Skip to content

Commit

Permalink
Update expected output (line numbers)
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtzguido
mtzguido committed Feb 17, 2025
1 parent 5be4f66 commit 9811fc2
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 10 deletions.
4 changes: 2 additions & 2 deletions tests/ide/emacs/FStarMode_GH73.ideout.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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": "<input>"}]}], "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": "<input>"}]}], "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": [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": "<input>"}, {"beg": [128, 12], "end": [128, 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": [127, 12], "end": [127, 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(127,12-127,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [127, 12], "end": [127, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
16 changes: 8 additions & 8 deletions tests/ide/emacs/FailRange.ideout.expected
View file
Original file line number Diff line number Diff line change
@@ -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": [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": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "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": [74, 4], "end": [74, 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(74,4-74,35)\n", "number": 228, "ranges": [{"beg": [5, 2], "end": [5, 18], "fname": "<input>"}, {"beg": [74, 4], "end": [74, 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": [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": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "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": [74, 4], "end": [74, 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(74,4-74,35)\n", "number": 228, "ranges": [{"beg": [9, 2], "end": [9, 18], "fname": "<input>"}, {"beg": [74, 4], "end": [74, 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": [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": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "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": [74, 4], "end": [74, 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(74,4-74,35)\n", "number": 228, "ranges": [{"beg": [13, 2], "end": [13, 18], "fname": "<input>"}, {"beg": [74, 4], "end": [74, 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": [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": "<input>"}, {"beg": [75, 4], "end": [75, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "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": [74, 4], "end": [74, 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(74,4-74,35)\n", "number": 228, "ranges": [{"beg": [17, 2], "end": [17, 18], "fname": "<input>"}, {"beg": [74, 4], "end": [74, 35], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "9", "response": [], "status": "success"}

0 comments on commit 9811fc2

Please sign in to comment.