The many Makefile targets

• 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 in FStar/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); try make -C examples/unit-tests for an extremely minimalistic test suite.
• make -C ulib: implied by make -C src regressions; tests regressions in FStar/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.