-
Notifications
You must be signed in to change notification settings - Fork 233
The many Makefile targets
Kenji Maillard edited this page May 26, 2017
·
6 revisions
-
make -C src/ocaml-output
builds the ocaml snapshot providing you with a working F* compiler (fastest way to have latest F* provided that the snapshot is not corrupted) -
make -C src fstar-ocaml
extracts a new ocaml snapshot using current F* and rebuilds the extracted snapshot (usual command when working on the F* compiler) -
make -C src utest
: cleans, bootstraps the compiler and runs the full regression suite -
make -C src uregressions
: implied by the above; doesn't rebuild the compiler just runs the full regression suite. -
make -C examples
: implied by the above; does only the regressions inFStar/examples
. Each sub-directory in examples has its own, so this target just calls each of them. Some of the targets are currently broken (e.g. Wysteria build); trymake -C examples/unit-tests
for an extremely minimalistic test suite. -
make -C ulib
: implied bymake -C src regressions
; tests regressions inFStar/lib
, the standard library -
make -C src uregressions OTHERFLAGS=--lax
: If you've made a change that doesn't really impact the type-checker (e.g., maybe you just moved some files around), then this will run the regressions in lax mode, skipping SMT verification, which will be MUCH faster.