Bootstrap process of F★ (the gory details)

These are notes for developers who are interested in understanding the bootstrap process of F★. If you're a user and just want to refresh your copy of F★, then make -C src -j 15 fstar-ocaml is probably what you want, assuming you have an already-working F★ (see https://github.com/FStarLang/FStar/blob/master/INSTALL.md for all the details).

For developers: details of the bootstrapping process.

The main constraint is that the src/ directory has to remain a valid F# "solution" (in Visual Studio lingo), so that we can edit and debug the F★ compiler itself within Visual Studio.

However, the F★ compiler cannot deal with the .fsi files that F# wants. Therefore, a "preprocessing" phase now occurs, to translate the .fsi + .fs files into valid .fst files. This preprocessing phase is fairly simple:

• the .fs file contains a special marker // VALS_HACK_HERE
• all the lines that start with val in the .fsi are inserted where the marker is found
• the resulting file is written to a module with the proper naming convention (e.g. FStar.Syntax.Print.fst) into src/boot_fsts
• the F★ compiler compiles and extracts everything in boot_fsts.