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 it to either OCaml or F#, using F*'s code extraction facility---this is invoked using the command line argument --codegen OCaml or --codegen FSharp.

The OCaml extractor will produce <ModuleName>.ml files for each F* module in the code; whereas the F# version will emit <ModuleName>.fs.

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 lib/fs (for F#) and lib/ml (for OCaml). To compile the code further and obtain an executable, you will need to link the extracted code with the support library.

Several examples of how this process works can be found in the repository.

• 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#.
• 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.

TODO: explain codegen and codegen lib flags https://github.com/FStarLang/FStar/issues/374

Note: make -C lib/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.