Now need to set FSTAR_HOME to verify examples

[catalin-hritcu]

Without that I'm getting a new error:

$ make -C examples
make: Entering directory '/home/hritcu/Projects/fstar/pub/examples'
Makefile.include:11: /home/hritcu/Projects/fstar/pub/bin//../lib/fstar/gmake/fstar.mk: No such file or directory
make: *** No rule to make target '/home/hritcu/Projects/fstar/pub/bin//../lib/fstar/gmake/fstar.mk'.  Stop.
make: Leaving directory '/home/hritcu/Projects/fstar/pub/examples'

[catalin-hritcu]

On second thought, a better fix would probably be to fix the following code instead of documenting the problem: https://github.com/FStarLang/FStar/blob/master/examples/Makefile.common#L6

[tahina-pro]

Thanks Catalin for reporting. I think we should at least better document how to use the examples directory. The main goal of https://github.com/FStarLang/FStar/commit/b7c98ea199e9794264b4019f71c58bad1964cee1 is to allow using examples outside of the F* repository structure. In other words, paths in examples Makefiles should work even if not relative to the F* directory. However, that commit only foresees two scenarios:

• either FSTAR_HOME is defined
• or, we assume that F* is installed by opam or make install, and reachable from the PATH.

Otherwise, in the scenario where F* is being run from the repository, we are silently assuming that such users should set FSTAR_HOME by hand. So, a better fix could be that if FSTAR_HOME is not defined and F* is not in the PATH, then this Makefile should assume that we are in the F* repository and set FSTAR_HOME=$(realpath ..) What do you all think? @nikswamy @aseemr

[aseemr]

Your suggestion sounds good to me @tahina-pro. I would also be fine saying that our makefiles/scripts take care of the scenarios where F* is being used from binary packages or opam, whereas if you are running from the repository, then you have to set FSTAR_HOME explicitly (and our makefiles/scripts could error out with a message).