Classifying the F* test suite

Jump to bottom Edit New page

nikswamy edited this page Jun 3, 2019 · 2 revisions

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.

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