Compiler hacking: Calling an OCaml or F# library from the F* sources

First, recall that the compiler is programmed in the shared subset of F* and F#. So, the filename extensions we use in the compiler sources are .fs and fsi, for compatibility with F#. However, these files are also valid F* files, when parsed with the --MLish flag.

We routinely call library functions from OCaml or F# from the F* sources. It's pretty straightforward, but involves a few steps.

A good example of this is the use of string buffers. See:

• Interface file, valid both in F* and F#: src/basic/boot/FStar.StringBuffer.fsi
• F# implementation src/basic/boot/FStar.StringBuffer.fs
• OCaml implementation src/basic/ml/FStar_StringBuffer.ml

1. Create an interface file for the functionality you wish to call.

For instance, in FStar.StringBuffer.fsi is a pretty straightforward interface.

2. Implement the interface in F# and OCaml

Note, the OCaml implementation has to anticipate the name-mangling the F* introduces on extraction. See FStar_StringBuffer.ml.

3. Building it:

• For the F# build, you need to add the .fsi and .fs to the suitable .fsproj file for the Visual Studio build
• For the OCaml build, add your new .fsi file to the ALL_BOOT variable in src/Makefile (around line 46). This is not always necessary, but it's a reasonable rule to follow. Depending on the way you named your file, you may need to add your module to the NOEXTRACT variable in src/Makefile.boot. Most common cases should not require this.

4. Now you should be able to just build as usual, make -C src fstar-ocaml for the OCaml build and make boot for the bootstrapping build.

Sometimes, the extraction works fine, but you get an error further along in the build when attempting to use the extracted ML file — this could indicate one of two things, generally speaking: (1) the generated ML sources on your disk are broken, and you need a working F* compiler do build your project. To resolve this, simply make FSTAR_BOOT=... 2 with FSTAR_BOOT pointing to a working F* compiler. (2) there is a genuine bug that the extraction mechanism failed to catch. In this case, roll up your sleeves, read the generated OCaml, and work your way backwards.

5. Now, elsewhere in the F* sources, you should just be able to call your newly added library as normal.

Note, if it's just a single small primitive it may be easier to add it to src/basic/boot/FStar.Util.fsi, to src/basic/boot/NotFStar.Util.fs (The F# implementation of this module) and to src/basic/ml/FStar_Util.ml (the OCaml implementation). These modules already aggregate many library functions and the build system is already aware of them. So, for small additions, extending FStar.Util is the way to go.