Executing F* code

By default F* only verifies the input code, it does not compile or execute it. To execute F* code one needs to translate for instance to OCaml or F#, using F*'s code extraction facility---this is invoked using the command line argument --codegen OCaml or --codegen FSharp. F* can also generate C, WASM, or even ASM code, but that is not discussed here.

The OCaml extractor will produce <ModuleName>.ml files for each F* module in the code; whereas the F# version will emit <ModuleName>.fs. These files will be located in the directory specified with --out; if no output directory is specified, the files are written out in the current directory.

The extracted code often relies on a support library, providing, for example, implementations of various primitive functions provided by F*'s standard library. The sources for this support library are in ulib/fs (for F#) and ulib/ml (for OCaml). To build the support library for OCaml, run make -C ulib/ml in the F* directory. To compile the extracted code further and obtain an executable, you will need to link it with the support library.

This also means that some modules (e.g. FStar.List) should not be extracted (because we provide an optimized implementation written in ML that uses, say, Batteries). For that purpose, a --no-codegen FStar.List flag should be passed when extracting.

To simplify things, a generic Makefile is provided in ulib/ml/Makefile.include; it provides a pre-set invocation of fstar where all the --no-codegen flags have been added. Furthermore, to speed up build times, make -C ulib/ml now builds a .cmxa file in addition to the individual .cmx files. You may want to link against that to simplify your build scripts, rather than copying ml files. The examples/hello directory provides an example.

Several examples of how this process works can be found in the repository. Reminder: run make -C ulib/ml before proceeding to the following examples.

• examples/hello provides hello.fst and a Makefile that compiles and executes a hello world program in both F# and OCaml.
• doc/tutorial/code/exercises provides ex1a-safe-read-write.fst (a simplistic example of access control on files) and Makefile. The build target acls-fs.exe compiles and runs the code using F#; acls-ocaml.exe illustrates a simple way to compile and run in OCaml; while hard-acl illustrates a harder, but more general way to run in OCaml.
• examples/crypto provides rpc.fst and a Makefile with the rpc-ml target providing a way to run a small, verified example of remote procedure calls in OCaml (while linking with OpenSSL).
• src/ocaml-output provides a Makefile which we use to bootstrap the F* compiler in OCaml.
• src/Makefile provides a make target boot-fsharp which we use to bootstrap the F* compiler in F#. See Bootstrap-process-of-F★-(the-gory-details).
• examples/wysteria/Makefile contains make targets for extracting and compiling Wysteria code. Target codegen generates code with some admitted interfaces (lib/ordset.fsi, lib/ordmap.fsi, and ffi.fsi) and target ocaml compiles the extracted code providing concrete implementations of those interfaces.

Advanced:

By default, Foo.Bar.fst gets extracted as a module Foo_Bar.ml; references to Foo.Bar become ML references to Foo_Bar. If you provide an F* model for Foo.Bar (via an .fsti only), then there will be no Foo_Bar.ml generated, you're expected to provide your own realization. So far, so good.

It may be the case that you have both Foo.Bar.fsti and Foo.Baz.fsti, both of which are related to each other. In order to simplify your life, --codegen-lib Foo will ensure that references to Foo.Bar and Foo.Baz are extracted as references to Foo.Bar (instead of Foo_Bar) and Foo.Baz (instead of Foo_Baz), so that you can use OCaml's module system to encapsulate your realized modules.