"Executing F* code" needs an update: instructions for building examples/hello don't work?
- Dominant language
- F*
- Stars
- 3.1k
- Forks
- 266
- Avg merge
- 21h 1m
- Merged PRs (30d)
- 54
Description
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](https://github.com/FStarLang/FStar/wiki/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*!
```
Contributor guide
Research direction
Start with the “Executing F* code” wiki page and the commands in examples/hello. Compare its make instructions with the reported missing paths and the working F* and OCaml commands; done means the documented example steps build and run successfully on the described setup.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- ocaml
- Domain
- build-system, documentation
- Issue type
- Documentation
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100