Unexpected error when missing all files

[briangmilnes]

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.

[kant2002]

I try to build FStar locally in WSL. I run

make

and go to bed. In the morning, I wake up and check if there ulib.dll which was nowhere to be found. So I run make again and decide to run make -C ulib ulib-in-fsharp and have similar error.

:/mnt/d/d/github/fstar/FStar$ make -C ulib ulib-in-fsharp
make: Entering directory '/mnt/d/d/github/fstar/FStar/ulib'
make FSTAR_HOME=.. -f Makefile.verify verify-core
make[1]: Entering directory '/mnt/d/d/github/fstar/FStar/ulib'
make[1]: Circular .cache/FStar.Real.fsti.checked <- .cache/FStar.Real.fsti.checked dependency dropped.
make[1]: Nothing to be done for 'verify-core'.
make[1]: Leaving directory '/mnt/d/d/github/fstar/FStar/ulib'
make -f Makefile.extract.fsharp dll
make[1]: Entering directory '/mnt/d/d/github/fstar/FStar/ulib'
true

/mnt/d/fstar/bin/fstar.exe   --use_hints   --warn_error @241 --cache_checked_modules --odir fs/extracted --cache_dir .cache --extract 'FSharp:*;OCaml:None;krml:None' --dep full --extract '* '  @.depend.extract.fsharp.rsp --output_deps_to .depend.extract.fsharp
unrecognized option '--output_deps_to'
Makefile.extract.fsharp:45: .depend.extract.fsharp: No such file or directory
make[1]: *** [Makefile.extract.fsharp:41: .depend.extract.fsharp] Error 1
make[1]: Leaving directory '/mnt/d/d/github/fstar/FStar/ulib'
make: *** [Makefile:35: ulib-in-fsharp-dll] Error 2
make: Leaving directory '/mnt/d/d/github/fstar/FStar/ulib'

I did try to reproduce and following command lines produce same error for me

/mnt/d/fstar/bin/fstar.exe --output_deps_to .depend.extract.fsharp
/mnt/d/fstar/bin/fstar.exe --output_deps_to
/mnt/d/fstar/bin/fstar.exe -output_deps_to
touch test
/mnt/d/fstar/bin/fstar.exe --output_deps_to test

All of that produce unrecognized option '--output_deps_to' for me.

$ git log
commit 7400bdd28f55b526726cf56d4041f9d925c839db (HEAD -> master)
Merge: 4015a6c463 5a43dd01e0
Author: Guido Martínez <mtzguido@gmail.com>
Date:   Tue Sep 3 13:50:23 2024 -0700

    Merge pull request #3432 from mtzguido/inline

    Parser.Dep: interpret inline_for_extraction on *any* decl, not just Vals

[mtzguido]

All of that produce unrecognized option '--output_deps_to' for me.

Hi Andrii. If you're getting this error your fstar.exe must be very old. What does fstar.exe --version say?

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 export FSTAR_HOME=$(pwd) from the root of the repo and try again?

This needing to set FSTAR_HOME is a very annoying problem which we should also fix.

[kant2002]

Ooh, you are right. I miss that. I definitely have older FStar on that PC. Thanks.