Pass proof state using references. #921
Annotations
3 errors and 10 warnings
|
Run tests, without forcing a build
Process completed with exit code 2.
|
|
Run tests, without forcing a build
Diff failed for files /tests/error-messages/_output/Bug2899.fst.output and /tests/error-messages/Bug2899.fst.output.expected:
--- Bug2899.fst.output.expected 2025-09-11 03:23:12.785599573 +0000
+++ _output/Bug2899.fst.output 2025-09-11 03:29:22.658858937 +0000
@@ -2,10 +2,9 @@
- Expected failure:
- Tactic failed
- Tactic got stuck!
- - Reduction stopped at:
- FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))"
+ - Reduction stopped at: Prims.admit ()
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
- - See also FStar.Tactics.Effect.fsti(200,48-200,58)
+ - See also FStar.Tactics.Effect.fsti(198,48-198,58)
* Info at Bug2899.fst(10,12-10,18):
- Expected failure:
@@ -13,21 +12,22 @@
- Tactic got stuck!
- Reduction stopped at: Prims.admit ()
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
- - See also FStar.Tactics.Effect.fsti(200,48-200,58)
+ - See also FStar.Tactics.Effect.fsti(198,48-198,58)
* Info at Bug2899.fst(13,12-13,18):
- Expected failure:
- Tactic failed
- Tactic got stuck!
- Reduction stopped at:
- FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))"
+ FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())
+ "(((ref proofstate)))"
- The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?
- - See also FStar.Tactics.Effect.fsti(200,48-200,58)
+ - See also FStar.Tactics.Effect.fsti(198,48-198,58)
* Info at Bug2899.fst(17,50-17,66):
- Expected failure:
- Tactic failed
- Tactic got stuck!
- - Reduction stopped at: reify (tac ()) "(((proofstate)))"
- - See also FStar.Tactics.Effect.fsti(200,48-200,58)
+ - Reduction stopped at: reify (tac ()) "(((ref proofstate)))"
+ - See also FStar.Tactics.Effect.fsti(198,48-198,58)
|
|
Run tests, without forcing a build
Diff failed for files /tests/error-messages/_output/Bug2899.fst.json_output and /tests/error-messages/Bug2899.fst.json_output.expected:
--- Bug2899.fst.json_output.expected 2025-09-11 03:23:12.785599573 +0000
+++ _output/Bug2899.fst.json_output 2025-09-11 03:29:21.887854041 +0000
@@ -1,4 +1,4 @@
-{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
-{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
-{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]}
-{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":200,"col":48},"end_pos":{"line":200,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}
+{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]}
+{"msg":["Expected failure:","Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Info","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":198,"col":48},"end_pos":{"line":198,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses'
in file "Typeclasses.fst".
- Rename "Typeclasses.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file
"Pure.fst".
- Rename "Pure.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(361) * Warning 361 at AlexOpaque.fst(103,0-125,5):
- Some #push-options have not been popped. Current depth is 2.
|
|
Run tests, without forcing a build:
Test.fst#L21
(272) * Warning 272 at Test.fst(21,0-21,31):
- Top-level let-bindings must be total; this term may have effects
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
Hello.fst#L5
(272) * Warning 272 at Hello.fst(5,0-5,34):
- Top-level let-bindings must be total; this term may have effects
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses'
in file "Typeclasses.fst".
- Rename "Typeclasses.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file
"Pure.fst".
- Rename "Pure.fst" to avoid conflicts.
|
|
Run tests, without forcing a build:
dummy#L0
(274) * Warning 274:
- Implicitly opening namespace 'fstar.' shadows module 'uint32' in file
"UInt32.fsti, UInt32.fst".
- Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.
|
Loading