-
Notifications
You must be signed in to change notification settings - Fork 231
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unexpected error when missing all files #3450
Comments
I try to build FStar locally in WSL.
and go to bed. In the morning, I wake up and check if there
I did try to reproduce and following command lines produce same error for me
All of that produce
|
Hi Andrii. If you're getting this error your fstar.exe must be very old. What does On a higher level, I think it's picking up the fstar.exe in your PATH instead of the one in your current directory. Could you do This needing to set FSTAR_HOME is a very annoying problem which we should also fix. |
Ooh, you are right. I miss that. I definitely have older FStar on that PC. Thanks. |
F* 2024.08.14~dev
platform=Linux_x86_64
compiler=OCaml 4.14.2
date=2024-09-02 15:23:16 -0700
commit=445f713ad8b276864ba7e205e028813e19324b66
I was goofing around with fstar arguments (in Forge makefiles) and darn Make did not evaluate things at the expected time,
so I missed all the file arguments and put a bad library in it and wham:
/home/milnes/.opam/default/bin/fstar.exe --warn_error "-321-333-331" --use_hints --use_hint_hashes --record_hints --hint_dir _build/fstar/fst/hints --print_universes --print_implicits --cache_checked_modules --dep full --output_deps_to depend --cache_dir _build/fstar/fst/cached --include /home/milnes/.opam/default/lib/fstar/ucontrib/Platform/fst --include /home/milnes/.opam/default/lib/fstar/ucontrib/Platform/fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Sys_error("/home/milnes/.opam/default/lib/fstar/ucontrib/Platform/fst: No such file or directory")
Probably should just be converted to a command line error.
The text was updated successfully, but these errors were encountered: