From a6cebb7a4eec539e6822aa26654dc06c09f42740 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 5 Oct 2024 09:44:17 -0700 Subject: [PATCH 1/4] Errors: making sure to bound all issues with the error_bound --- src/basic/FStarC.Errors.fst | 31 +++++++++++++++++-------------- src/basic/FStarC.Errors.fsti | 3 +++ 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/basic/FStarC.Errors.fst b/src/basic/FStarC.Errors.fst index c920afaef98..15ab8ea43a1 100644 --- a/src/basic/FStarC.Errors.fst +++ b/src/basic/FStarC.Errors.fst @@ -44,6 +44,11 @@ let with_error_bound (r:range) (f : unit -> 'a) : 'a = error_range_bound := old; res +let maybe_bound_range (r : Range.range) : Range.range = + match !error_range_bound with + | Some r' -> Range.bound_range r r' + | None -> r + (** This exception is raised in FStar.Error when a warn_error string could not be processed; The exception is handled in FStarC.Options as part of @@ -287,16 +292,11 @@ let compare_issues i1 i2 = let dummy_ide_rng : Range.rng = mk_rng "" (mk_pos 1 0) (mk_pos 1 0) -let maybe_bound_rng (r : Range.range) : Range.range = - match !error_range_bound with - | Some r' -> Range.bound_range r r' - | None -> r - (* Attempts to set a decent range (no dummy, no dummy ide) relying on the fallback_range reference. *) -let fixup_issue_range (i:issue) : issue = +let fixup_issue_range (rng:option Range.range) : option Range.range = let rng = - match i.issue_range with + match rng with | None -> (* No range given, just rely on the fallback. NB: the fallback could also be set to None if it's too early. *) @@ -316,7 +316,7 @@ let fixup_issue_range (i:issue) : issue = in Some (set_use_range range use_rng') in - { i with issue_range = map_opt rng maybe_bound_rng } + map_opt rng maybe_bound_range let mk_default_handler print = let issues : ref (list issue) = BU.mk_ref [] in @@ -368,7 +368,6 @@ let get_err_count () = (!current_handler).eh_count_errors () let wrapped_eh_add_one (h : error_handler) (issue : issue) : unit = (* Try to set a good use range if we got an empty/dummy one *) - let issue = fixup_issue_range issue in h.eh_add_one issue; if issue.issue_level <> EInfo then begin Options.abort_counter := !Options.abort_counter - 1; @@ -533,16 +532,17 @@ let lookup err = let log_issue_ctx r (e, msg) ctx = let msg = maybe_add_backtrace msg in + let r = fixup_issue_range (Some r) in match lookup e with | (_, CAlwaysError, errno) | (_, CError, errno) -> - add_one (mk_issue EError (Some r) msg (Some errno) ctx) + add_one (mk_issue EError r msg (Some errno) ctx) | (_, CWarning, errno) -> - add_one (mk_issue EWarning (Some r) msg (Some errno) ctx) + add_one (mk_issue EWarning r msg (Some errno) ctx) | (_, CSilent, _) -> () // We allow using log_issue to report a Fatal error in interactive mode | (_, CFatal, errno) -> - let i = mk_issue EError (Some r) msg (Some errno) ctx in + let i = mk_issue EError r msg (Some errno) ctx in if Options.ide() then add_one i else failwith ("don't use log_issue to report fatal error, should use raise_error: " ^ format_issue i) @@ -550,10 +550,11 @@ let log_issue_ctx r (e, msg) ctx = let info r msg = let open FStarC.Class.HasRange in let rng = pos r in + let rng = fixup_issue_range (Some rng) in let msg = to_doc_list msg in let msg = maybe_add_backtrace msg in let ctx = get_ctx () in - add_one (mk_issue EInfo (Some rng) msg None ctx) + add_one (mk_issue EInfo rng msg None ctx) let diag r msg = if Debug.any() then @@ -562,6 +563,7 @@ let diag r msg = let raise_error r e msg = let open FStarC.Class.HasRange in let rng = pos r in + let Some rng = fixup_issue_range (Some rng) in let msg = to_doc_list msg in raise (Error (e, maybe_add_backtrace msg, rng, error_context.get ())) @@ -583,7 +585,8 @@ let issue_of_exn (e:exn) : option issue = match e with | Error(e, msg, r, ctx) -> let errno = error_number (lookup e) in - Some (mk_issue EError (Some r) msg (Some errno) ctx) + let r = fixup_issue_range (Some r) in + Some (mk_issue EError r msg (Some errno) ctx) | _ -> None let err_exn exn = diff --git a/src/basic/FStarC.Errors.fsti b/src/basic/FStarC.Errors.fsti index 6cb0935ce84..bb8f482961f 100644 --- a/src/basic/FStarC.Errors.fsti +++ b/src/basic/FStarC.Errors.fsti @@ -37,6 +37,9 @@ val error_range_bound : FStarC.Effect.ref (option Range.range) val with_error_bound (r:Range.range) (f : unit -> 'a) : 'a +(* Intersect a range by the current bound (if any). *) +val maybe_bound_range (rng:Range.range) : Range.range + (* Get the error number for a particular code. Useful for creating error messages mentioning --warn_error. *) val errno : error_code -> int From 44000020c810b94e5fa1ded3bd4ff1f0bde9901e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 5 Oct 2024 09:47:58 -0700 Subject: [PATCH 2/4] Tactics.Effect: a read-only, total version This is useful for primitives that cannot possibly fail, and have no effect, but need to be in TAC due to reading some part of the proofstate. For example, the state of the current error range bound. --- ulib/FStar.Tactics.Effect.fsti | 3 +++ 1 file changed, 3 insertions(+) diff --git a/ulib/FStar.Tactics.Effect.fsti b/ulib/FStar.Tactics.Effect.fsti index d104d531ef3..63eb25d4d7c 100644 --- a/ulib/FStar.Tactics.Effect.fsti +++ b/ulib/FStar.Tactics.Effect.fsti @@ -164,6 +164,9 @@ effect Tac (a:Type) = TacH a (requires (fun _ -> True)) (ensures (fun _ _ -> Tru (* Metaprograms that succeed *) effect TacS (a:Type) = TacH a (requires (fun _ -> True)) (ensures (fun _ps r -> Success? r)) +(* Always succeed, no effect *) +effect TacRO (a:Type) = TAC a (fun ps post -> forall r. post (Success r ps)) + (* A variant that doesn't prove totality (nor type safety!) *) effect TacF (a:Type) = TacH a (requires (fun _ -> False)) (ensures (fun _ _ -> True)) From 394ebea1a404da1a5aeb720daeb538bfda95af40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sat, 5 Oct 2024 09:48:49 -0700 Subject: [PATCH 3/4] Tactics: exposing a way to read the error range bound, use it in `fail`s When a tactic fails, it raises an exception, which does not read the current error bound. The interpreter module running the tactic will then bound the range by reading the current error bound, but it is too late as it could have been popped away. This moves the bounding logic into the `fail`s in the tactic module, to read the bound immediately before raising the exception. This is mostly useful for Pulse, as there is no way for normal userspace clients to set the bound, so it wouldn't make a difference. Hence I'm unsure about this patch. --- src/ml/full/FStarC_Tactics_V2_Builtins.ml | 1 + src/tactics/FStarC.Tactics.V2.Basic.fst | 3 +++ src/tactics/FStarC.Tactics.V2.Basic.fsti | 1 + src/tactics/FStarC.Tactics.V2.Primops.fst | 2 ++ ulib/FStar.Stubs.Tactics.V2.Builtins.fsti | 2 ++ ulib/FStar.Tactics.V2.Derived.fst | 19 +++++++++++++------ 6 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/ml/full/FStarC_Tactics_V2_Builtins.ml b/src/ml/full/FStarC_Tactics_V2_Builtins.ml index 9829fffd4b7..7d1bf2ef51f 100644 --- a/src/ml/full/FStarC_Tactics_V2_Builtins.ml +++ b/src/ml/full/FStarC_Tactics_V2_Builtins.ml @@ -61,6 +61,7 @@ let from_tac_5 s (t: 'a -> 'b -> 'c -> 'd -> 'e -> 'r TM.tac): 'a -> 'b -> 'c - (* Pointing to the internal primitives *) +let fixup_range = from_tac_1 "B.fixup_range" B.fixup_range let compress = from_tac_1 "B.compress" B.compress let set_goals = from_tac_1 "TM.set_goals" TM.set_goals let set_smt_goals = from_tac_1 "TM.set_smt_goals" TM.set_smt_goals diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index f22d8dd8207..01909d49aff 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -73,6 +73,9 @@ open FStarC.Class.Monad open FStarC.Class.PP open FStarC.Class.Setlike +let fixup_range (r : FStarC.Range.range) : tac (FStarC.Range.range) = + return (Errors.maybe_bound_range r) + let compress (t:term) : tac term = return ();! return (SS.compress t) diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fsti b/src/tactics/FStarC.Tactics.V2.Basic.fsti index 9a36b5126a4..fa02b229630 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V2.Basic.fsti @@ -47,6 +47,7 @@ val proofstate_of_all_implicits: Range.range -> env -> implicits -> proofstate & (* Metaprogramming primitives (not all of them). * Documented in `ulib/FStarC.Tactics.Builtins.fst` *) +val fixup_range (r : Range.range) : tac (Range.range) val compress : term -> tac term val top_env : unit -> tac env val fresh : unit -> tac Z.t diff --git a/src/tactics/FStarC.Tactics.V2.Primops.fst b/src/tactics/FStarC.Tactics.V2.Primops.fst index 6251c6cbff3..49d2f64e234 100644 --- a/src/tactics/FStarC.Tactics.V2.Primops.fst +++ b/src/tactics/FStarC.Tactics.V2.Primops.fst @@ -100,6 +100,8 @@ let ops = [ unseal_step; + mk_tac_step_1 0 "fixup_range" fixup_range fixup_range; + mk_tac_step_1 0 "compress" compress compress; mk_tac_step_1 0 "set_goals" set_goals set_goals; mk_tac_step_1 0 "set_smt_goals" set_smt_goals set_smt_goals; diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index a277a35e88d..9e145dc2e67 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -29,6 +29,8 @@ open FStar.Tactics.Effect open FStar.Stubs.Tactics.Types include FStar.Stubs.Tactics.Unseal +val fixup_range : Range.range -> TacRO Range.range + (** Resolve unification variable indirections at the top of the term. *) val compress : term -> Tac term diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst index 06f6a002612..5dd819eae9e 100644 --- a/ulib/FStar.Tactics.V2.Derived.fst +++ b/ulib/FStar.Tactics.V2.Derived.fst @@ -63,29 +63,36 @@ exception Goal_not_trivial let goals () : Tac (list goal) = goals_of (get ()) let smt_goals () : Tac (list goal) = smt_goals_of (get ()) +private +let map_optRO (f:'a -> TacRO 'b) (x:option 'a) : TacRO (option 'b) = + match x with + | None -> None + | Some x -> Some (f x) + let fail_doc_at (#a:Type) (m:error_message) (r:option range) - : TAC a (fun ps post -> post (Failed (TacticFailure (m, r)) ps)) - = raise #a (TacticFailure (m, r)) + : TAC a (fun ps post -> forall r. post (Failed (TacticFailure (m, r)) ps)) + = let r = map_optRO fixup_range r in + raise #a (TacticFailure (m, r)) let fail_doc (#a:Type) (m:error_message) : TAC a (fun ps post -> post (Failed (TacticFailure (m, None)) ps)) = raise #a (TacticFailure (m, None)) let fail_at (#a:Type) (m:string) (r:option range) - : TAC a (fun ps post -> post (Failed (TacticFailure (mkmsg m, r)) ps)) + : TAC a (fun ps post -> forall r. post (Failed (TacticFailure (mkmsg m, r)) ps)) = fail_doc_at (mkmsg m) r let fail (#a:Type) (m:string) - : TAC a (fun ps post -> post (Failed (TacticFailure (mkmsg m, None)) ps)) + : TAC a (fun ps post -> forall r. post (Failed (TacticFailure (mkmsg m, r)) ps)) = fail_at m None let fail_silently_doc (#a:Type) (m:error_message) - : TAC a (fun _ post -> forall ps. post (Failed (TacticFailure (m, None)) ps)) + : TAC a (fun _ post -> forall r ps. post (Failed (TacticFailure (m, r)) ps)) = set_urgency 0; raise #a (TacticFailure (m, None)) let fail_silently (#a:Type) (m:string) - : TAC a (fun _ post -> forall ps. post (Failed (TacticFailure (mkmsg m, None)) ps)) + : TAC a (fun _ post -> forall r ps. post (Failed (TacticFailure (mkmsg m, r)) ps)) = fail_silently_doc (mkmsg m) (** Return the current *goal*, not its type. (Ignores SMT goals) *) From 5ab7deaed54cfd527c3f6ff73aa28101b9cb62f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 17 Jan 2025 23:47:52 -0800 Subject: [PATCH 4/4] Update expected output, mostly line number changes --- .../Bug2899.fst.json_output.expected | 8 ++++---- tests/error-messages/Bug2899.fst.output.expected | 8 ++++---- tests/ide/emacs/FStarMode_GH73.ideout.expected | 4 ++-- tests/ide/emacs/FailRange.ideout.expected | 16 ++++++++-------- 4 files changed, 18 insertions(+), 18 deletions(-) diff --git a/tests/error-messages/Bug2899.fst.json_output.expected b/tests/error-messages/Bug2899.fst.json_output.expected index a2f3914f38b..be9beacbd7b 100644 --- a/tests/error-messages/Bug2899.fst.json_output.expected +++ b/tests/error-messages/Bug2899.fst.json_output.expected @@ -1,12 +1,12 @@ >> Got issues: [ -{"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`"]} +{"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":215,"col":48},"end_pos":{"line":215,"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`"]} +{"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":215,"col":48},"end_pos":{"line":215,"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:\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`"]} +{"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":215,"col":48},"end_pos":{"line":215,"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`"]} +{"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":215,"col":48},"end_pos":{"line":215,"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`"]} >>] diff --git a/tests/error-messages/Bug2899.fst.output.expected b/tests/error-messages/Bug2899.fst.output.expected index 95b036ea5bc..a06dd4c2183 100644 --- a/tests/error-messages/Bug2899.fst.output.expected +++ b/tests/error-messages/Bug2899.fst.output.expected @@ -5,7 +5,7 @@ - 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) + - See also FStar.Tactics.Effect.fsti(215,48-215,58) >>] >> Got issues: [ @@ -14,7 +14,7 @@ - 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(212,48-212,58) + - See also FStar.Tactics.Effect.fsti(215,48-215,58) >>] >> Got issues: [ @@ -24,7 +24,7 @@ - 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) + - See also FStar.Tactics.Effect.fsti(215,48-215,58) >>] >> Got issues: [ @@ -32,6 +32,6 @@ - Tactic failed - Tactic got stuck! - Reduction stopped at: reify (tac ()) "(((proofstate)))" - - See also FStar.Tactics.Effect.fsti(212,48-212,58) + - See also FStar.Tactics.Effect.fsti(215,48-215,58) >>] diff --git a/tests/ide/emacs/FStarMode_GH73.ideout.expected b/tests/ide/emacs/FStarMode_GH73.ideout.expected index ee934ccefff..7a3248d351d 100644 --- a/tests/ide/emacs/FStarMode_GH73.ideout.expected +++ b/tests/ide/emacs/FStarMode_GH73.ideout.expected @@ -3,5 +3,5 @@ {"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": ""}]}], "status": "failure"} {"kind": "response", "query-id": "4", "response": [], "status": "success"} -{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [121, 12], "end": [121, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"} -{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- 'exact' failed\n- Term 1 of type int does not exactly solve the goal bool\n- See also FStar.Tactics.V2.Derived.fst(121,12-121,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": ""}, {"beg": [121, 12], "end": [121, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} +{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [128, 12], "end": [128, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"} +{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- 'exact' failed\n- Term 1 of type int does not exactly solve the goal bool\n- See also FStar.Tactics.V2.Derived.fst(128,12-128,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": ""}, {"beg": [128, 12], "end": [128, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} diff --git a/tests/ide/emacs/FailRange.ideout.expected b/tests/ide/emacs/FailRange.ideout.expected index be84020522c..22141684072 100644 --- a/tests/ide/emacs/FailRange.ideout.expected +++ b/tests/ide/emacs/FailRange.ideout.expected @@ -1,14 +1,14 @@ {"kind": "protocol-info", "rest": "[...]"} {"kind": "response", "query-id": "1", "response": [], "status": "success"} -{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [6, 25], "end": [6, 33], "fname": ""}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "2"} -{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Tactic failed\n- A\n- See also (6,25-6,33)\n", "number": 228, "ranges": [{"beg": [5, 2], "end": [5, 18], "fname": ""}, {"beg": [6, 25], "end": [6, 33], "fname": ""}]}], "status": "failure"} +{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "2"} +{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Tactic failed\n- A\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [5, 2], "end": [5, 18], "fname": ""}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "3", "response": [], "status": "success"} -{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [10, 25], "end": [10, 33], "fname": ""}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "4"} -{"kind": "response", "query-id": "4", "response": [{"level": "error", "message": "- Tactic failed\n- B\n- See also (10,25-10,33)\n", "number": 228, "ranges": [{"beg": [9, 2], "end": [9, 18], "fname": ""}, {"beg": [10, 25], "end": [10, 33], "fname": ""}]}], "status": "failure"} +{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}, {"goal": {"label": "", "type": "squash l_True", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "4"} +{"kind": "response", "query-id": "4", "response": [{"level": "error", "message": "- Tactic failed\n- B\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [9, 2], "end": [9, 18], "fname": ""}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "5", "response": [], "status": "success"} -{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [13, 2], "end": [13, 18], "fname": ""}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "6"} -{"kind": "response", "query-id": "6", "response": [{"level": "error", "message": "- Tactic failed\n- C\n", "number": 228, "ranges": [{"beg": [13, 2], "end": [13, 18], "fname": ""}]}], "status": "failure"} +{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "6"} +{"kind": "response", "query-id": "6", "response": [{"level": "error", "message": "- Tactic failed\n- C\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [13, 2], "end": [13, 18], "fname": ""}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "7", "response": [], "status": "success"} -{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [17, 2], "end": [17, 18], "fname": ""}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "8"} -{"kind": "response", "query-id": "8", "response": [{"level": "error", "message": "- Tactic failed\n- D\n", "number": 228, "ranges": [{"beg": [17, 2], "end": [17, 18], "fname": ""}]}], "status": "failure"} +{"contents": {"depth": 0, "goals": [{"goal": {"label": "", "type": "squash (l_True /\\ l_True)", "witness": "(*?u[...]*) _"}, "hyps": [{"name": "uu___", "type": "unit"}]}], "label": "at the time of failure", "location": {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "8"} +{"kind": "response", "query-id": "8", "response": [{"level": "error", "message": "- Tactic failed\n- D\n- See also FStar.Tactics.V2.Derived.fst(75,4-75,35)\n", "number": 228, "ranges": [{"beg": [17, 2], "end": [17, 18], "fname": ""}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "9", "response": [], "status": "success"}