Build F* with dune instead of ocamlbuild

[tahina-pro]

tl;dr: What changes for the user

• fstarlib, fstar-tactics-lib and fstar-compiler-lib all become fstar.lib
• OCAMLPATH=$FSTAR_HOME/bin becomes OCAMLPATH=$FSTAR_HOME/lib
  • $FSTAR_HOME/bin/fstarlib.cmx* becomes $FSTAR_HOME/lib/fstar/lib/fstar_lib.cmx*
• the tactic library is now statically linked with fstar.exe
• in the binary package, the standard library is now in lib/fstar instead of ulib (this was already the case with the OPAM package or make install)
• compiling F* programs extracted to OCaml with the F* binary package is no longer supported, please install F* via opam instead (with opam pin fstar --dev-repo)

The problem

Currently, the OCaml port of F*, both for Windows and Linux, relies on ocamlbuild, which leads to the following issues:

• no parallelism
• poor incrementality
• ocamlbuild is explicitly dubbed as a "legacy" build system for OCaml, undergoing deprecation in favor of Dune (cf. https://github.com/ocaml/ocamlbuild)

The solution: this PR

This PR builds F* with dune instead of ocamlbuild. To this end:

• a whole snapshot of F*, including ulib, is now included, currently in the ocaml subdirectory. Now, to build F*, it is only necessary to build that snapshot and verify ulib. This is what the default make rule of the root Makefile now does. No extraction is needed as long as nothing in the F* sources or in ulib is changed, which is the case for most users. (In particular, lax-typechecking of ulib is no longer needed!) As of now, the snapshot includes FStar_Parser_Parse.ml file as generated by menhir/ocamlyacc, but no version of parse.mly file (so that we don't need to instruct dune to call menhir or ocamlyacc)
• fstar-lib, fstar-tactics-lib and fstar-compiler-lib are now all merged into a single package, fstar.lib, whose OCaml sources (including the generated and extracted files) are in ocaml/fstar-lib, which is now statically linked with the F* compiler. No need to dynamically load any "F* tactic library" anymore! No need to compute a list of "leftovers between fstarlib and fstartaclib" anymore! The library is now installed into lib/fstar, instead of a subdirectory of bin.
  (With this solution, every application built with F* needs to be linked with the whole F* compiler/typechecker, etc., which may cause bloating of the produced binary executable. As discussed with @nikswamy and @mtzguido , we may need to change the way --codegen Plugin works, by making sure it produces a library disjoint from --codegen OCaml, at least at the level of the module name.)
• all handwritten OCaml files are now in the ocaml subdirectory, instead of src/*/ml, ulib/ml or ulib/tactics_ml, with the exception of parse.mly. The entrypoint of fstar.exe is in ocaml/fstar, that of fstar_tests.exe is in ocaml/fstar-tests; everything else is in ocaml/fstar-lib. However, we distinguish them from the generated files, which are in ocaml/fstar-lib/generated (instead of src/ocaml-output). This is both to make sure there is only one copy of each file, and to satisfy dune's requirement that all OCaml files shall be in the same directory hierarchy.

How to test: 3 make rules

• To build F*, just do make
• With an existing F*, to update the snapshot in case of any change in src or ulib, just do make dune-bootstrap
  This rule now supports incrementality.
• If needed, the rule make dune-full-bootstrap removes all generated files from the snapshot before generating them again. This shouldn't be necessary, except maybe if a file is renamed and we want to make sure the old file is removed.

All those 3 rules support parallelism.

Remaining tasks before merging this PR

• Fix the remaining state-handling issues (behavior discrepancies between the executables compiled by dune and ocamlbuild) (see bc00724):
  • An "error 147" message disappeared from tests/ide/emacs/search.cons-snoc
  • uvar numbers shifted in Bug2010, Bug2021, OccursCheckOnArrows.
  • As part of this PR, I fixed a bug in the pretty-printer, where some internal state (unfold_tuples) was not properly restored, cf. 0b02e48 . This bug was causing a diff in tests/prettyprinting/Tuples, with extra parentheses in the dune build as opposed to the ocambuild build.
• Remove now-unused, useless attempts to dynamically load the old fstartaclib.cmxs (easy)
• Re-enable the snapshot diff check in the CI. To do that, we need to:
  • Fix the elaboration of static quotations, which are currently printing the full name of the file where the file is built, thus introducing a discrepancy between the committer's machine and the CI container
• Fix the make install rule (for binary packages and opam)
• Clarify the opam package: probably ocaml/fstar.opam is not needed, but we can benefit from the new snapshot to reduce the dependencies in the existing fstar.opam
• For make package, rebuild and include the F# snapshot of ulib
• Fix the release infra
• Fix the nix rules
• Check that everest still works (this should be fine)

What this pull request DOES NOT do

• Instruct dune to generate the F* parser using menhir and/or ocamlyacc
• Build each ocaml extraction example with dune instead of ocamlbuild (hello/multifile already does, but not sample_project) (tracked by Discontinue ocamlbuild in OCaml extraction examples #2838)
• Extract the F* sources without --lax, benefitting from the .checked files of ulib
• Move the standard library from ulib to lib/fstar in the F* sources
• Verify ulib with dune instead of make (this would replace make with dune as the build driver for F*)

[nikswamy]

I've been trying to build this branch from a clean state on Windows with cygwin, but it fails with the following log:

make[1]: Entering directory '/home/nswamy/workspace/clean/test/FStar/src/ocaml-output'
  MAKE      FStar_Version.ml
make[1]: Leaving directory '/home/nswamy/workspace/clean/test/FStar/src/ocaml-output'
cd /home/nswamy/workspace/clean/test/FStar/ocaml && dune build --profile release && dune install --prefix=/home/nswamy/workspace/clean/test/FStar
Installing "/home/nswamy/workspace/clean/test/FStar\\lib\\fstar\\META"
Installing "/home/nswamy/workspace/clean/test/FStar\\lib\\fstar\\dune-package"
Installing "/home/nswamy/workspace/clean/test/FStar\\lib\\fstar\\lib/FStar_Algebra_CommMonoid.ml"
Installing "/home/nswamy/workspace/clean/test/FStar\\lib\\fstar\\lib/FStar_Algebra_CommMonoid_Equiv.ml"
...
Installing "/home/nswamy/workspace/clean/test/FStar\\lib\\fstar\\lib/fstar_lib.cmxs"
Installing "/home/nswamy/workspace/clean/test/FStar\\bin\\fstar.exe"
Installing "/home/nswamy/workspace/clean/test/FStar\\bin\\fstar_tests.exe"
make verify-ulib
make[1]: Entering directory '/home/nswamy/workspace/clean/test/FStar'
make -C ulib
make[2]: Entering directory '/home/nswamy/workspace/clean/test/FStar/ulib'
make FSTAR_HOME=.. -f Makefile.verify verify-core
make[3]: Entering directory '/home/nswamy/workspace/clean/test/FStar/ulib'
../bin/fstar.exe --warn_error @271-330   --use_hints --cache_dir .cache --hint_dir .cache --silent --cache_checked_modules --odir _output @.depend.rsp > .depend
/bin/sh: ../bin/fstar.exe: No such file or directory
make[3]: *** [gmake/Makefile.tmpl:78: .depend] Error 127
make[3]: Leaving directory '/home/nswamy/workspace/clean/test/FStar/ulib'
make[2]: *** [Makefile:10: all] Error 2
make[2]: Leaving directory '/home/nswamy/workspace/clean/test/FStar/ulib'
make[1]: *** [Makefile:21: verify-ulib] Error 2
make[1]: Leaving directory '/home/nswamy/workspace/clean/test/FStar'
make: *** [Makefile:24: dune] Error 2

My bin directory is actually empty, aside from a couple static scripts

[nikswamy]

I pulled the latest and tried again ... here's what I got.

Internal error, please report upstream including the contents of _build/log.
Description:
  ("Fs_memo.Watcher.watch called on a build path",
  { path = In_build_dir "version.txt" })
Raised at Stdune__code_error.raise in file "otherlibs/stdune\\code_error.ml",
  line 11, characters 30-62
Called from Dune_engine__fs_memo.Watcher.watch in file
  "src/dune_engine\\fs_memo.ml", line 129, characters 6-108
Called from Dune_engine__fs_memo.file_digest in file
  "src/dune_engine\\fs_memo.ml", line 271, characters 12-60
Called from Dune_engine__load_rules.source_file_digest in file
  "src/dune_engine\\load_rules.ml", line 281, characters 2-26
Called from Dune_engine__load_rules.get_rule_or_source in file
  "src/dune_engine\\load_rules.ml", line 870, characters 13-36
Called from Dune_engine__build_system.Exported.build_file_impl in file
  "src/dune_engine\\build_system.ml", line 888, characters 4-38
Called from Fiber__scheduler.exec in file "src/fiber\\scheduler.ml", line 69,
  characters 8-11
-> required by ("build-file", In_build_dir "version.txt")
-> required by ("deps", ())
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
   { id = 4
   ; info =
       From_dune_file
         { pos_fname = "fstar-lib/dune"
         ; start = { pos_lnum = 22; pos_bol = 320; pos_cnum = 320 }
         ; stop = { pos_lnum = 31; pos_bol = 536; pos_cnum = 563 }
         }
   })
-> required by ("<unnamed>", ())
-> required by
   ("build-file", In_build_dir "default/fstar-lib/FStar_Version.ml")
-> required by ("Rule.make", ())
-> required by
   ("execute-rule",
   { id = 274
   ; info =
       From_dune_file
         { pos_fname = "fstar-lib/dune"
         ; start = { pos_lnum = 2; pos_bol = 30; pos_cnum = 30 }
         ; stop = { pos_lnum = 20; pos_bol = 317; pos_cnum = 318 }
         }
   })
-> required by ("<unnamed>", ())
-> required by
   ("build-file",
   In_build_dir "install/default/lib/fstar/lib/FStar_Version.ml")
-> required by ("Rule.make", ())
-> required by ("execute-rule", { id = 1208; info = Internal })
-> required by ("<unnamed>", ())
-> required by ("build-file", In_build_dir "default/fstar.install")
-> required by
   ("build-pred",
   { dir = In_build_dir "default"
   ; predicate = { id = exclude }
   ; only_generated_files = true
   })
-> required by ("<unnamed>", ())
-> required by ("build-alias", { dir = "default"; name = "all" })
-> required by ("<unnamed>", ())
-> required by ("build-alias", { dir = "default"; name = "default" })
-> required by ("toplevel", ())

I must not crash.  Uncertainty is the mind-killer. Exceptions are the
little-death that brings total obliteration.  I will fully express my cases.
Execution will pass over me and through me.  And when it has gone past, I
will unwind the stack along its path.  Where the cases are handled there will
be nothing.  Only I will remain.
****

[tahina-pro]

Thanks Nik for reporting. There is an issue on Cygwin with running the bash script to generate FStar_Version.ml from dune. I just pushed a fix, can you please try again?

[nikswamy]

Hi @tahina-pro ... I have the same dune exception even with your latest changes.

[mtzguido]

FYI @nikswamy @aseemr, this is a way to bootstrap the compiler without verifying/extracting ulib. It won't work if something in ulib that the compiler depends on changed significantly, but it can save you time otherwise

[nikswamy]

Upgrading to dune 3.5 solved my problem on cygwin

[tahina-pro]

Upgrading to dune 3.5 solved my problem on cygwin

Thanks Nik for reporting! I confirm F* successfully builds with dune 3.2.0 but not dune 3.1.x. I think this is related to ocaml/dune#5572, which was fixed in dune 3.2.0. So I updated the dependency requirements accordingly.

[tahina-pro]

For any F* maintainers who might still have outstanding branches with F* building with ocamlbuild, here is some process to merge master in your branches to convert to dune, adapted from my comment above (#2815 (comment)):

1. _taramana_dune_step_2 is the last step of the F*+dune PR that has both ocamlbuild and dune flavors, so you should merge that branch into yours:

git pull origin _taramana_dune_step_2

2. If you have conflicts in the ocamlbuild snapshot, you should solve them first,
   then extract an ocamlbuild snapshot with an ocamlbuild-compiled fstar.exe:

make -C src/ocaml-output
make -j -C src ocaml
make -C src/ocaml-output

3. Generate the dune snapshot from the ocamlbuild snapshot, and commit that snapshot:

make clean-full-dune-snapshot
make -j dune-staged-bootstrap
git add ocaml/fstar*/*.ml ocaml/fstar*/generated/*.ml
git commit

4. Remove the ocamlbuild snapshot:

rm -f src/ocaml-output/FStar_*
git add -u
git commit

5. Finally, merge master into your branch and regenerate a snapshot (implicitly using the fstar.exe created at step 3):

git pull origin master
make clean-dune-snapshot
make -j dune-bootstrap
git add ocaml/fstar*/generated/*.ml
git commit

[nikswamy]

Additionally, I've noticed that if you have changes to hand-written ML files in your branch, then you may need to copy those changes over to ocaml/fstar-lib manually.

In _nik_steel_dsl for instance, we had changes to FStar_Tactics_Builtins.ml and FStar_Parsing_LexFStar.ml ... and these were dropped initially, leading to a successful build, but with strange failures in behavior (particularly with the parser) that had me confused for a while.

[tahina-pro]

Additionally, I've noticed that if you have changes to hand-written ML files in your branch, then you may need to copy those changes over to ocaml/fstar-lib manually.

When converting a given branch, this case should be covered by the dune-staged-bootstrap rule, which copies those files. Was it not in your case?
However, if you have a branch A that "depends" on a branch B, then it is not enough to convert B and merge it into A, if A has additional changes in handwritten ML files. In that case, there should be modify-delete conflicts on those handwritten files when merging a converted B into A.