FStar icon indicating copy to clipboard operation
FStar copied to clipboard

minor adjustment to `new_z3proc_with_id`

Open smoothdeveloper opened this issue 3 years ago • 1 comments

This function was failing in my environment and it seems to fix it.

This is checking just the prefix of the output rather than the whole of it.

Context: I was running Verify current file in the command line in emacs

before:

"C:/dev/src/github.com/FStar/FStar/bin/fstar.exe" "c:/dev/src/github.com/mateuszbujalski/jsonstar/jsonstar/JsonStar.Json.fst" "--smt" "C:/dev/bin/z3-4.8.5-x64-win/bin/z3.exe" Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. Failed to start and test Z3 process, expected output "Test" got "Test Done! "

after:

"C:/dev/src/github.com/FStar/FStar/bin/fstar.exe" "c:/dev/src/github.com/mateuszbujalski/jsonstar/jsonstar/JsonStar.Json.fst" "--smt" "C:/dev/bin/z3-4.8.5-x64-win/bin/z3.exe" C:\dev\src\github.com\FStar\FStar\ulib\prims.fst(0,0-0,0): (Warning 241) Unable to load C:\dev\src\github.com\FStar\FStar\ulib\prims.fst.checked since checked file C:\dev\src\github.com\FStar\FStar\ulib\prims.fst.checked does not exist; will recheck C:\dev\src\github.com\FStar\FStar\ulib\prims.fst (suppressing this warning for further modules) Verified module: JsonStar.Json All verification conditions discharged successfully

Please let me know any of the adjustments you'd like, or if there is an approach you'd like me to take to add a test.

smoothdeveloper avatar May 27 '21 17:05 smoothdeveloper

Hi @smoothdeveloper, thanks for submitting this PR. I looked into it a little. I am curious to know why is there an error on your configuration, while all of us use it without any problems. In particular, the "Done!" part should not be returned to this function that you are modifying.

Do you have any insights on this?

aseemr avatar Apr 05 '22 08:04 aseemr