Classifying the F* test suite

Here's some information about various classes of programs in the F* source tree.

To benchmark F* performance alone, you should run with --admit_smt_queries true. This will prevent F* from calling Z3.

Each example sub-directory should have its own Makefile

Extraction tests

The main test for extraction in the source tree is bootstrapping the F* compiler

To bootstrap, see INSTALL.md, specifically this part: https://github.com/FStarLang/FStar/blob/master/INSTALL.md#step-2-extracting-the-sources-of-f-itself-to-ocaml

Unifier-heavy tests

• examples/micro-benchmarks/ChrisCheck.fst
• examples/tactics/Bane.Lib.fst

Normalizer-heavy tests

• examples/micro-benchmarks/Normalization.fst
• examples/tactics/Canon.fst