File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -103,7 +103,7 @@ jobs:
103103 - name : Smoke test
104104 run : |
105105 ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
106- echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
106+ echo -e "module A\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
107107 ./fstar/bin/fstar.exe A.fst
108108 echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
109109 ./fstar/bin/fstar.exe --admit_smt_queries true B.fst
Original file line number Diff line number Diff line change 8888 - name : Smoke test
8989 run : |
9090 ./fstar/bin/fstar.exe --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
91- echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
91+ echo -e "module A\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
9292 ./fstar/bin/fstar.exe --admit_smt_queries true A.fst
9393 echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
9494 ./fstar/bin/fstar.exe --admit_smt_queries true B.fst
Original file line number Diff line number Diff line change 3737
3838 - name : Smoke test
3939 run : |
40- echo -e "module A\let _ = assert (forall x. 1 + x*x > 0)" > A.fst
40+ echo -e "module A\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
4141 eval $(opam env) && fstar.exe A.fst
4242 echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
4343 eval $(opam env) && fstar.exe B.fst
You can’t perform that action at this time.
0 commit comments