Fix cross-platform build: replace symlinks with copy_files

.docker/base/Dockerfile

@@ -1,4 +1,4 @@
-FROM ubuntu:18.04
+FROM ubuntu:22.04
 
 MAINTAINER Benjamin Beurdouche <benjamin.beurdouche@inria.fr>; Victor Dumitrescu <victor.dumitrescu@nomadic-labs.com>; Daniel Fabian <daniel.fabian@integral-it.ch>;
 
@@ -7,7 +7,7 @@ RUN apt-get -qq update
 RUN apt-get install -y software-properties-common
 RUN add-apt-repository -y ppa:avsm/ppa # for opam 2
 RUN apt-get -qq update
-RUN apt-get install -y sudo wget libssl-dev libsqlite3-dev g++ gcc m4 make opam pkg-config python libgmp3-dev unzip cmake
+RUN apt-get install -y sudo wget libssl-dev libsqlite3-dev g++ gcc m4 make opam pkg-config python3 libgmp-dev unzip cmake git
 
 # Create user
 RUN useradd -ms /bin/bash build
@@ -18,7 +18,7 @@ WORKDIR /home/build
 # Prepare and build OPAM and OCaml
 RUN opam init -y --disable-sandboxing
 RUN opam update
-RUN opam install -y ocamlbuild ocamlfind batteries stdint zarith yojson fileutils pprint menhir mtime sedlex ppx_deriving ppx_deriving_yojson process pprint visitors fix wasm ppxlib=0.22.0
+RUN opam install -y dune batteries stdint zarith yojson pprint menhir mtime sedlex ppx_deriving ppx_deriving_yojson process ppxlib memtrace
 
 # Prepare and build Z3
 ENV z3=z3-4.8.5-x64-debian-8.11

.docker/build/build_funs.sh

@@ -71,9 +71,33 @@ function fstar_default_build () {
         (fetch_karamel ; make_karamel_pre) &
     fi
 
-    # Build F*, along with fstarlib
-    if ! make -j $threads ci-pre; then
-        echo Warm-up failed
+    # Build F* using dune (replaces old make ci-pre)
+    echo "Building F* with dune..."
+
+    # Stage 0: Bootstrap compiler
+    dune build --root=stage0 -j $threads
+    dune install --root=stage0 --prefix=stage0/out
+    export FSTAR_EXE=$(pwd)/stage0/out/bin/fstar.exe
+
+    # Generate fstarc.dune.inc (dune needs it to parse src/extracted/dune)
+    $FSTAR_EXE --lax --MLish --MLish_effect FStarC.Effect --dep dune \
+      --include ulib --include src/basic --include src/class \
+      --include src/data --include src/extraction --include src/fstar \
+      --include src/interactive --include src/parser --include src/prettyprint \
+      --include src/reflection --include src/smtencoding --include src/syntax \
+      --include src/syntax/print --include src/tactics --include src/tosyntax \
+      --include src/typechecker --include src/tests \
+      --extract FStarC --extract +FStar.Pervasives \
+      --extract -FStar.Pervasives.Native --extract "krml:-*" \
+      src/fstar/FStarC.Main.fst > src/extracted/fstarc.dune.inc
+
+    # Extract, Stage 1, Stage 2
+    dune build @extract-stage1 -j $threads
+    dune build @stage1 -j $threads
+    dune build @stage2 -j $threads
+
+    if [ $? -ne 0 ]; then
+        echo Build failed
         echo Failure >$result_file
         return 1
     fi
@@ -82,25 +106,25 @@ function fstar_default_build () {
 
     wait # for fetches above
 
-    # Once F* is built, run its main regression suite. This also runs the karamel
-    # test (unless CI_NO_KARAMEL is set).
-    $gnutime make -j $threads -k ci-post && echo true >$status_file
+    # Run tests (replaces old make ci-post)
+    echo "Running tests with dune..."
+    $gnutime dune runtest -j $threads && echo true >$status_file
     echo Done building FStar
 
     if [ -z "${FSTAR_CI_NO_GITDIFF}" ]; then
         # Make it a hard failure if there's a git diff in the snapshot. First check for
         # extraneous files, then for a diff.
-        echo "Searching for a diff in ocaml/*/generated"
-        git status ocaml/*/generated # Print status for log
+        echo "Searching for a diff in src/extracted"
+        git status src/extracted # Print status for log
 
         # If there's any output, i.e. any file not in HEAD, fail
-        if git ls-files --others --exclude-standard -- ocaml/*/generated | grep -q . ; then
+        if git ls-files --others --exclude-standard -- src/extracted | grep -q . ; then
             echo " *** GIT DIFF: there are extraneous files in the snapshot"
             echo false >$status_file
         fi
 
         # If there's a diff in existing files, fail
-        if ! git diff --exit-code ocaml/*/generated ; then
+        if ! git diff --exit-code src/extracted ; then
             echo " *** GIT DIFF: the files in the list above have a git diff"
             echo false >$status_file
         fi

.docker/opam.Dockerfile

@@ -19,6 +19,6 @@ RUN rm -rf FStar
 # opam uninstall will balk at removing files created there during the test
 RUN cp -p -r $(opam config var fstar:share)/examples $HOME/examples
 RUN cp -p -r $(opam config var fstar:share)/doc $HOME/doc
-RUN eval $(opam env) && make -C $HOME/examples -j $opamthreads
-RUN eval $(opam env) && make -C $HOME/doc/old/tutorial -j $opamthreads regressions
+RUN eval $(opam env) && cd $HOME/examples && dune runtest
+RUN eval $(opam env) && cd $HOME/doc/old/tutorial && dune runtest
 RUN opam uninstall -v -v -v fstar

.github/workflows/build-ci.yml

@@ -36,6 +36,10 @@ jobs:
         run: |
           # Note: we don't package Z3 for the CI artifact as the images
           # already have the relevant Z3.
+          # verify-ulib creates .checked files needed by downstream projects like Pulse
+          # Run verify-ulib first (sequential) because it generates ulib.dune.inc
+          # which dune needs to parse before building package
+          make -skj$(nproc) verify-ulib
           make -skj$(nproc) package package-src FSTAR_TAG= FSTAR_PACKAGE_Z3=false
         working-directory: FStar
 

.github/workflows/build-linux.yml

@@ -84,6 +84,6 @@ jobs:
 
       - name: Smoke test
         run: |
-          ./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
+          ./fstar/bin/fstar fstar/lib/fstar/ulib/Prims.fst -f
           echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
-          ./fstar/bin/fstar.exe A.fst
+          ./fstar/bin/fstar A.fst

.github/workflows/build-macos.yml

@@ -70,6 +70,6 @@ jobs:
 
       - name: Smoke test
         run: |
-          ./fstar/bin/fstar.exe --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
+          ./fstar/bin/fstar --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
           echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
-          ./fstar/bin/fstar.exe --admit_smt_queries true A.fst
+          ./fstar/bin/fstar --admit_smt_queries true A.fst

.github/workflows/build-opam.yml

@@ -18,7 +18,7 @@ jobs:
       matrix:
         ocamlv:
           - 4.14.2
-          - 5.3
+          - 5.4
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@master
@@ -36,4 +36,4 @@ jobs:
       - name: Smoke test
         run: |
           echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
-          eval $(opam env) && fstar.exe A.fst
+          eval $(opam env) && fstar A.fst

.github/workflows/build-pulse.yml

@@ -26,7 +26,7 @@ jobs:
         with:
           name: fstar.tar.gz
       - run: tar -xzf fstar.tar.gz
-      - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar.exe" >> $GITHUB_ENV
+      - run: echo "FSTAR_EXE=$(pwd)/fstar/bin/fstar" >> $GITHUB_ENV
 
       - name: Checkout pulse
         uses: actions/checkout@master