tests: ide: use --ext fstar:no_absolute_paths, update output

FStarLang · Aug 28, 2023 · 82066fd · 82066fd
1 parent 87ab9d3
commit 82066fd
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 5 deletions.
diff --git a/tests/ide/cleanup.py b/tests/ide/cleanup.py
@@ -18,8 +18,9 @@ def cleanup_json(js):
     if isinstance(js, dict):
         if "fname" in js:
             js["fname"] = os.path.basename(js["fname"].replace('\\', '/'))
-        if "location" in js:
-            js["location"] = "<location removed>"
+        # We do currently care about locations, do not remove them
+        #  if "location" in js:
+        #      js["location"] = "<location removed>"
         for v in js.values():
             cleanup_json(v)
     elif isinstance(js, list):

diff --git a/tests/ide/emacs/Makefile b/tests/ide/emacs/Makefile
@@ -1,6 +1,6 @@
 include ../Makefile.common
 
-FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --ide --warn_error -282
+FSTAR:=${FSTAR_HOME}/bin/fstar.exe $(SMT) --ide --warn_error -282 --ext fstar:no_absolute_paths
 
 # Feed .in to F* and record output as .out.  Output is passed through cleanup.py
 # to ensure that the output is deterministic by pretty-printing JSON messages

diff --git a/tests/ide/emacs/fstarmode_gh73.out.expected b/tests/ide/emacs/fstarmode_gh73.out.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\"", "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\"", "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": "<location removed>", "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
+{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [101, 12], "end": [101, 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": "user tactic failed: `exact: 1 : int does not exactly solve the goal bool (witness = (*?u[...]*) _)`", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [101, 12], "end": [101, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
diff --git a/tests/ide/emacs/search.cons-snoc.out.expected b/tests/ide/emacs/search.cons-snoc.out.expected
@@ -1,4 +1,4 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [], "status": "success"}
-{"contents": "<input>(1,0-1,0): (Error 147) Effect template STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position\n", "kind": "message", "level": "error", "query-id": "2"}
+{"contents": "FStar.Seq.Properties.fsti(774,0-776,62): (Error 147) Effect template STATE_h should be applied to arguments for its binders ((heap: Type)) before it can be used at an effect position (see also <input>(1,0-1,0))\n", "kind": "message", "level": "error", "query-id": "2"}
 {"contents": "1 error was reported (see above)\n", "kind": "message", "level": "error", "query-id": "2"}