Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Executing F* code
Clone this wiki locally
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
--codegen OCaml or
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 compile the code
further and obtain an executable, you will need to link the extracted
code with the support library.
This 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.
Makefilethat compiles and executes a hello world program in both F# and OCaml.
ex1a-safe-read-write.fst(a simplistic example of access control on files) and
Makefile. The build target
acls-fs.execompiles and runs the code using F#;
acls-ocaml.exeillustrates a simple way to compile and run in OCaml; while
hard-aclillustrates a harder, but more general way to run in OCaml.
rpc-mltarget providing a way to run a small, verified example of remote procedure calls in OCaml (while linking with OpenSSL).
Makefilewhich we use to bootstrap the F* compiler in OCaml.
src/Makefileprovides a make target
boot-fsharpwhich we use to bootstrap the F* compiler in F#. See Bootstrap-process-of-F★-(the-gory-details).
examples/wysteria/Makefilecontains make targets for extracting and compiling Wysteria code. Target
codegengenerates code with some admitted interfaces (
ffi.fsi) and target
ocamlcompiles the extracted code providing concrete implementations of those interfaces.
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.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.Baz are extracted as references to
Foo.Bar (instead of
Foo.Baz (instead of
Foo_Baz), so that you can use OCaml's module system to encapsulate your realized modules.