"Executing F* code" needs an update: instructions for building examples/hello don't work?

[btj]

I cloned the FStar repo and built F* from source on my Mac x86. I'm trying to build examples/hello using the instructions from Executing F* code, but this fails:

~/fstar/FStar/examples/hello % make hello
../Makefile.include:11: /../lib/fstar/gmake/z3.mk: No such file or directory
../Makefile.include:12: /../lib/fstar/gmake/fstar.mk: No such file or directory
Makefile:3: /../lib/fstar/ml/Makefile.include: No such file or directory
make: *** No rule to make target `/../lib/fstar/ml/Makefile.include'.  Stop.

The following does work:

~/fstar/FStar/examples/hello % ../../bin/fstar.exe --odir out --codegen OCaml --extract 'Hello' Hello/Hello.fst
Extracted module Hello
* Warning 272 at Hello/Hello.fst(20,0-20,37):
  - Top-level let-bindings must be total; this term may have effects

Verified module: Hello
All verification conditions discharged successfully
~/fstar/FStar/examples/hello % ocamlfind ocamlopt -I ../../ocaml/_build/install/default/lib/fstar/lib ../../ocaml/_build/install/default/lib/fstar/lib/fstar_lib.cmxa out/Hello.ml -package ZArith,Stdint,Yojson,ppx_deriving_yojson -linkpkg -o hello.exe
ld: warning: search path '/opt/local/lib' not found
~/fstar/FStar/examples/hello % ./hello.exe 
Hello F*!

[btj]

This also works:

../../bin/fstar.exe --odir out --codegen OCaml --extract 'Hello' Hello/Hello.fst
OCAMLPATH=../../lib ocamlfind ocamlopt out/hello.ml -package fstar.lib -linkpkg -thread -o hello.exe

[btj]

I found out I could make make -C examples/hello hello work by defining FSTAR_HOME to point to the FStar repo. (Neither "Executing F* code" nor the repo's README.md instructed me to do so.)

[mtzguido]

Hi Bart, sorry for this issue. Indeed this need to set FSTAR_HOME is not properly documented, and it's a common footgun. There is some discussion here about why it's needed.

I think most of this whole mess comes from the makefiles trying to find the location of F*'s library depending on these variables. Maybe we can just add an F* option to print the location of the library, and have the makefiles use that, and hopefully that's it. I'll take a look soon.

Thanks for the report!