Skip to content

Bootstrap process of F★ (the gory details)

Jonathan Protzenko edited this page Feb 12, 2016 · 3 revisions

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 + .fsfiles 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.
Clone this wiki locally