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. Code written in a C-like shalowly embedded DSL can be extracted to C or WASM by the KreMLin tool, and code written in an ASM-like deeply embedded DSL can be extracted to ASM by the Vale tool, but none of that is not discussed on this page. Also since F# extraction is plagued by some bugs (eg. #1096, #1087 and more), the rest of this page is really only about OCaml extraction.

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/ml (for OCaml) and ulib/fs (for F#). 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 F* 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 any of the OCaml extraction examples.

• examples/hello provides hello.fst and a Makefile that compiles and executes a hello world program in OCaml. You can try that out via:

  $ make -C examples/hello ocaml
  

  (There is also an attempt to extract this to F# and run it, but it doesn't currently work.)

• doc/tutorial/code/exercises provides a simplistic example of access control on files in Ex1a.fst The make target Ex01a-ocaml illustrates how to extract this to OCaml and run it:

  $ make -C doc/tutorial/code/exercises Ex01a-ocaml
  

• examples/crypto provides RPC.fst and CntProtocol.fst and a Makefile with the rpc-test and cnt-test targets providing a way to run a small, verified example of remote procedure calls in OCaml (while linking with OpenSSL).

  $ make -C examples/crypto rpc-test
  $ make -C examples/crypto cnt-test
  

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

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.