From 9b0b21c0ff364f1d50c261d0d6b7eaf9966cb481 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 10 Oct 2024 17:59:46 -0700 Subject: [PATCH] output changed!?!? --- tests/error-messages/Bug2899.fst.expected | 8 ++++---- tests/error-messages/Bug2899.fst.json_expected | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/error-messages/Bug2899.fst.expected b/tests/error-messages/Bug2899.fst.expected index c98faed40a6..9bad2e4edb9 100644 --- a/tests/error-messages/Bug2899.fst.expected +++ b/tests/error-messages/Bug2899.fst.expected @@ -2,8 +2,8 @@ * Error 170 at Bug2899.fst(7,12-7,18): - Tactic failed - Tactic got stuck! - - Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ()) - "(((proofstate)))" + - Reduction stopped at: + FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))" - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`? - See also FStar.Tactics.Effect.fsti(212,48-212,58) @@ -21,8 +21,8 @@ * Error 170 at Bug2899.fst(13,12-13,18): - Tactic failed - Tactic got stuck! - - Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) - "(((proofstate)))" + - Reduction stopped at: + FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))" - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`? - See also FStar.Tactics.Effect.fsti(212,48-212,58) diff --git a/tests/error-messages/Bug2899.fst.json_expected b/tests/error-messages/Bug2899.fst.json_expected index 740eddb1cc0..1f64a5aee7c 100644 --- a/tests/error-messages/Bug2899.fst.json_expected +++ b/tests/error-messages/Bug2899.fst.json_expected @@ -1,11 +1,11 @@ >> Got issues: [ -{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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":["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":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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`"]} >>] >> Got issues: [ {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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`"]} >>] >> Got issues: [ -{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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":["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":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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`"]} >>] >> Got issues: [ {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"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`"]}