-
Notifications
You must be signed in to change notification settings - Fork 232
Building F* with dune? (and esy?)
This page is about building the OCaml (not F#) version of F*.
Currently, the OCaml port of F*, both for Windows and Linux, relies on opam and ocamlbuild, which leads to the following issues:
-
ocamlbuildis explicitly dubbed as a "legacy" build system for OCaml, undergoing deprecation in favor of Dune (cf. https://github.com/ocaml/ocamlbuild) - Windows users need to explicitly install Cygwin to use OCaml and compile F*
- The current Windows port of opam 2.0 is slated to be discontinued in August 2021 (cf. https://fdopen.github.io/opam-repository-mingw/ )
To solve each issue above, I propose to use:
- Dune: https://dune.readthedocs.io/en/stable/
- esy (https://esy.sh/docs/en/getting-started.html) hides all Cygwin details away from the user on Windows. Most packages rely on dune, although it could be possible to still use ocamlbuild.
- esy hides all uses of opam away from the user on Windows (and seems to use a different Windows port than fdopen), although "full support for Windows is planned for opam 2.2", alas yet unannounced to this day (cf. https://opam.ocaml.org/doc/Install.html#Windows)
Given that situation, I decided to experiment on both using dune and esy to rebuild F* on both Linux and Windows. On Linux, I managed to use dune;
then I tried to use esy on Windows based on that dune setup.
See: https://github.com/tahina-pro/FStar/tree/taramana_dune_20210519
To simplify things, I first filled in the few gaps in the OCaml snapshot of F*, by adding to the parse tree:
- the parser generated by menhir
- the
FStar_*Int*.mlimplementations of machine integers
Then, at this point, all OCaml modules are in the F* tree, ready to be compiled (rationale: on Windows, I no longer want to assume that users who want to recompile F* have make, Cygwin, MinGW or anything like that.)
And now starts the hard thing. Reading through src/ocaml-output/Makefile, the OCaml implementation of F* is scattered around src and some of ulib/ml.
- It is very hard, if at all possible, to build a single project whose source is scattered across a list of some (but not all) directories at different depths. The only way I found was to write a
dunefile at the root directory of F*, telling dune to include all directories undersrcandulib.
So I did that, and finally, on Linux, I managed to have a working fstar.exe.
On Windows, I couldn't reach that step, because:
- Building zarith is not based on dune, and esy cannot build zarith on Windows, failing because zarith's
configurescript fails to detect the C compiler used byesy. Porting zarith to dune is an open issue, with Xavier Leroy not very keen on solving it in the short term (cf. https://github.com/ocaml/Zarith/pull/73#issuecomment-768478489)
But then, I couldn't know how to build F* libraries with dune, either on Linux or on Windows, because:
- It is impossible to write a
dunefile to build executables and/or libraries from non-disjoint sets of modules.
To solve Problems 4 and 6, we should clarify the build of F*. For the compiler itself, we might need to follow an approach similar to the F# build of F*, saying that each directory is actually a library of its own. But the situation worsens (in particular problem 6) once we consider ulib. We might need to explicitly list modules that should go into F* ulib, vs. F* taclib vs. F* compiler lib, and/or split the ulib/ml directory into corresponding subdirectories (or totally revise this way of splitting ulib.) This somehow defeats the purpose of a build system (namely automatic dependency discovery.)
To solve Problem 5, we need to consider alternatives to zarith. Granted, zarith gives us high performance, but, in addition to build issues on Windows:
- zarith makes F* depend on a LGPL-licensed library, namely libgmp (the GNU multi-precision arithmetic library, https://gmplib.org/).