Merge pull request #2815 from FStarLang/_taramana_dune

Build F* with `dune` instead of `ocamlbuild`

.common.mk

@@ -4,7 +4,7 @@
 # follows (taken from src/Makefile.boot):
 #
 # ocaml-output/%.ml:
-# 	@echo "[EXTRACT   $(notdir $@)]"
+# 	$(call msg, "EXTRACT", $(notdir $@))
 # 	$(Q)$(BENCHMARK_PRE) $(FSTAR_C) $(SIL) $(notdir $(subst .checked.lax,,$<)) \
 #                   --codegen OCaml \
 #                   --extract_module $(basename $(notdir $(subst .checked.lax,,$<)))
@@ -17,10 +17,6 @@
 #
 # Besides that, when not using V=1, F* receives the --silent flag to
 # reduce non-critical output.
-#
-# It would be nice to define a function to print messages instead of
-# copying the same echo invocation everywhere, but AFAIK that would mean
-# we require GNU make.
 
 Q?=@
 SIL?=--silent
@@ -37,6 +33,10 @@ runlim not found:
   You can get it from: [https://github.com/arminbiere/runlim]
 endef
 
+define msg =
+@printf "  %-8s  %s\n" $(1) $(2)
+endef
+
 # Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
 # information about the time and space taken by each F* invocation.
 ifneq ($(RESOURCEMONITOR),)

.completion/fish/fstar.exe.fish

@@ -49,7 +49,6 @@ complete -c fstar.exe -l max_ifuel --description "non-negative integer  Number o
 complete -c fstar.exe -l MLish --description "Trigger various specializations for compiling the F* compiler itself (not meant for user code)"
 complete -c fstar.exe -l no_default_includes --description "Ignore the default module search paths"
 complete -c fstar.exe -l no_extract --description "module name  Deprecated: use --extract instead; Do not extract code from this module"
-complete -c fstar.exe -l no_load_fstartaclib --description "Do not attempt to load fstartaclib by default"
 complete -c fstar.exe -l no_location_info --description "Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)"
 complete -c fstar.exe -l no_smt --description "Do not send any queries to the SMT solver, and fail on them instead"
 complete -c fstar.exe -l normalize_pure_terms_for_extraction --description "Extract top-level pure terms after normalizing them. This can lead to very large code, but can result in more partial evaluation and compile-time specialization."

.docker/build/build_funs.sh

@@ -103,9 +103,15 @@ function update_version_number () {
     git commit -m "[CI] bump version number to $version_number"
 }
 
+function git_add_fstar_snapshot () {
+    if ! git diff-index --quiet --cached HEAD -- ocaml/*/generated ; then
+        git ls-files ocaml/*/generated | xargs git add
+    fi
+}
+
 function refresh_fstar_hints() {
     [[ -n "$DZOMO_GITHUB_TOKEN" ]] &&
-    refresh_hints "https://$DZOMO_GITHUB_TOKEN@github.com/FStarLang/FStar.git" "git ls-files src/ocaml-output/ | xargs git add" "regenerate hints + ocaml snapshot" "."
+    refresh_hints "https://$DZOMO_GITHUB_TOKEN@github.com/FStarLang/FStar.git" "git_add_fstar_snapshot" "regenerate hints + ocaml snapshot" "."
 }
 
 # Note: this performs an _approximate_ refresh of the hints, in the sense that
@@ -194,8 +200,7 @@ function fstar_binary_build () {
 function fstar_docs_build () {
     # First - get fstar built
     # Second - run fstar with the --doc flag
-    make -C src/ocaml-output clean && \
-        make -C src/ocaml-output -j $threads && \
+    OTHERFLAGS='--admit_smt_queries true' make -j $threads && \
         .ci/fsdoc.sh && \
         echo true >$status_file
 }
@@ -213,7 +218,7 @@ function fstar_default_build () {
     fi &
 
     # Build F*, along with fstarlib
-    if ! make -C src -j $threads utest-prelude; then
+    if ! make -j $threads ci-utest-prelude; then
         echo Warm-up failed
         echo Failure >$result_file
         return 1
@@ -232,13 +237,13 @@ function fstar_default_build () {
     fi
 
     # Once F* is built, run its main regression suite.
-    $gnutime make -C src -j $threads -k $localTarget && echo true >$status_file
+    $gnutime make -j $threads -k ci-$localTarget && echo true >$status_file
     echo Done building FStar
 
     # Make it a hard failure if there's a git diff. Note: FStar_Version.ml is in the
     # .gitignore.
-    echo "Searching for a diff in src/ocaml-output"
-    if ! git diff --exit-code src/ocaml-output; then
+    echo "Searching for a diff in ocaml/*/generated"
+    if ! git diff --exit-code ocaml/*/generated ; then
         echo "GIT DIFF: the files in the list above have a git diff"
         echo false >$status_file
     fi

.docker/opam.Dockerfile

@@ -6,12 +6,19 @@ FROM ocaml/opam:ubuntu-ocaml-$ocaml_version
 # FIXME: the `opam depext` command should be unnecessary with opam 2.1
 RUN opam depext conf-gmp z3.4.8.5 conf-m4
 
+ADD --chown=opam:opam ./fstar.opam fstar.opam
+RUN opam install --deps-only ./fstar.opam
+RUN rm fstar.opam
+
 ADD --chown=opam:opam ./ FStar/
-RUN rm -rf FStar/.git
 
-RUN opam install --deps-only FStar/fstar.opam
 ARG opamthreads=24
 RUN opam install -j $opamthreads -v -v -v FStar/fstar.opam
-RUN eval $(opam env) && make -C $(opam config var fstar:share)/examples -j $opamthreads
-RUN eval $(opam env) && make -C $(opam config var fstar:share)/tutorial -j $opamthreads regressions
+RUN rm -rf FStar
+# NOTE: I need to copy examples and tutorial from share/ because
+# 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/tutorial -j $opamthreads regressions
 RUN opam uninstall -v -v -v fstar

.docker/package.Dockerfile

@@ -4,54 +4,45 @@
 
 # Build the package
 ARG ocaml_version=4.12
-FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstardep
+ARG opamthreads=24
+
+FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild
 
 # FIXME: the `opam depext` command should be unnecessary with opam 2.1
 RUN opam depext conf-gmp z3.4.8.5 conf-m4
 
-ADD --chown=opam:opam ./ FStar/
+ADD --chown=opam:opam ./fstar.opam fstar.opam
 
 # Install opam dependencies only
-RUN opam install --deps-only FStar/fstar.opam
+RUN opam install --deps-only ./fstar.opam
 
-ARG opamthreads=24
+# Install .NET
+RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
+  libicu66
 
-FROM fstardep AS fstarbuild
+# (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
+# CI dependencies: .NET Core
+# Repository install may incur some (transient?) failures (see for instance https://github.com/dotnet/sdk/issues/27082 )
+# So, we use manual install instead, from https://docs.microsoft.com/en-us/dotnet/core/install/linux-scripted-manual#manual-install
+ENV DOTNET_ROOT /home/opam/dotnet
+RUN sudo apt-get install --yes --no-install-recommends \
+    wget
 
-# Build the package, 
-RUN eval $(opam env) && env Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" OTHERFLAGS='--admit_smt_queries true' make -C FStar -j $opamthreads package_unknown_platform
+RUN wget https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
+    mkdir -p $DOTNET_ROOT && \
+    tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT
 
-# Create a separate image to test the package
-FROM fstardep AS fstarbin
+ENV PATH=${PATH}:$DOTNET_ROOT:$DOTNET_ROOT/tools
 
-# Remove F* sources (keep deps)
-RUN mv FStar FStar.todelete && rm -rf FStar.todelete
+ADD --chown=opam:opam ./ FStar/
 
-# Copy the F* binary package
-COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/fstar.tar.gz /home/opam/fstar.tar.gz
-RUN tar xzf fstar.tar.gz
-ENV FSTAR_HOME /home/opam/fstar
-ENV PATH="${FSTAR_HOME}/bin:${PATH}"
+# Build the package, 
+RUN eval $(opam env) && env Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" OTHERFLAGS='--admit_smt_queries true' make -C FStar -j $opamthreads package_unknown_platform
 
-# Copy examples and docs
-ADD --chown=opam:opam examples/ fstar_examples/
-ADD --chown=opam:opam doc/ fstar_doc/
+# Create a separate image to test the package
 
 # Test the F* binary package
 
-# Case 1: test the fresh package
-FROM fstarbin
-RUN eval $(opam env) && make -C fstar_examples -j $opamthreads
-RUN eval $(opam env) && make -C fstar_doc/tutorial -j $opamthreads regressions
-
-# Case 2: rebuild ulib and test again
-FROM fstarbin
-RUN eval $(opam env) && make -C $FSTAR_HOME/ulib rebuild -j $opamthreads
-RUN eval $(opam env) && make -C fstar_examples/hello -j $opamthreads
-RUN eval $(opam env) && make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
-RUN eval $(opam env) && make -C fstar_examples -j $opamthreads
-RUN eval $(opam env) && make -C fstar_doc/tutorial -j $opamthreads regressions
-
 # Test the fresh package without OCaml
 FROM ubuntu:20.04 AS fstarnoocaml
 ENV DEBIAN_FRONTEND=noninteractive
@@ -71,24 +62,29 @@ SHELL ["/bin/bash", "--login", "-c"]
 # Copy the package
 COPY --from=fstarbuild /home/opam/FStar/src/ocaml-output/fstar.tar.gz /home/test/fstar.tar.gz
 RUN tar xzf fstar.tar.gz
-ENV FSTAR_HOME /home/test/fstar
-ENV PATH="${FSTAR_HOME}/bin:${PATH}"
 
 # Copy tests, examples and docs
 ADD --chown=test:test examples/ fstar_examples/
 ADD --chown=test:test doc/ fstar_doc/
 
 # Case 3: test F* package without OCaml
-FROM fstarnoocaml
-RUN make -C fstar_examples -j $opamthreads
-RUN make -C fstar_doc/tutorial -j $opamthreads regressions
 
-# Case 4: test F* package without OCaml, but recheck ulib
+# Test the package with FSTAR_HOME defined
+# Move z3 elsewhere
+# FROM fstarnoocaml
+# ENV FSTAR_HOME=$HOME/fstar
+# RUN mkdir -p $HOME/bin && ln -s $FSTAR_HOME/bin/z3 $HOME/bin/
+# ENV PATH="${HOME}/bin:${PATH}"
+# RUN make -C fstar_examples -j $opamthreads
+# RUN make -C fstar_doc/tutorial -j $opamthreads regressions
+
+# Test the package with F* in the PATH instead
 FROM fstarnoocaml
-RUN make -C $FSTAR_HOME/ulib clean_checked && make -C $FSTAR_HOME/ulib -j $opamthreads
+ENV PATH="/home/test/fstar/bin:${PATH}"
 RUN make -C fstar_examples -j $opamthreads
 RUN make -C fstar_doc/tutorial -j $opamthreads regressions
 
+FROM fstarnoocaml
 # This is the last image. So we can also copy the file that contains
 # the desired filename for the package, to be extracted via
 # `docker cp`

.gitattributes

@@ -4,6 +4,7 @@
 *.fsti linguist-language=FStar
 *.fsti linguist-documentation=false
 /src/ocaml-output/FStar_*.ml linguist-vendored
+/ocaml/fstar-lib/generated/FStar_*.ml linguist-vendored
 
 # Line endings
 *.fs* eol=lf
@@ -24,6 +25,8 @@ karamel_ref eol=lf
 # does not show diffs in the CLI nor GitHub.
 /src/ocaml-output/FStar_*.ml -diff -merge
 /src/ocaml-output/FStar_*.ml linguist-generated=true
+/ocaml/fstar-lib/generated/FStar_*.ml -diff -merge
+/ocaml/fstar-lib/generated/FStar_*.ml linguist-generated=true
 *.hints -diff -merge
 *.hints linguist-generated=true
 

.gitignore

@@ -31,6 +31,8 @@ cache/
 /bin/z3-x64.exe
 /src/*/obj
 
+/lib
+
 examples/*/*.ml
 examples/crypto/CntProtocol.exe
 examples/wysteria/ocaml-output/*
@@ -43,6 +45,8 @@ _build/
 /ulib/fs/obj
 /ulib/fs/bin
 
+/release
+
 *.native
 *.byte
 
@@ -60,6 +64,7 @@ dump
 *.cmxs
 *.cmxa
 *.o
+fstar.install
 
 .depend
 .depend.rsp

.nix/README.md

@@ -43,11 +43,6 @@ To build/run/install/... `fstar-bootsrap`, just use
 `github:FStarLang/FStar#fstar-bootsrap` instead of
 `github:FStarLang/FStar`.
 
-## Building custom version of F\*
-
-The file `.nix/lib.nix` provides a fined grained Nix API to build
-custom F\*.
-
 ## Hacking on F\*
 
 Just run `nix develop` in your local clone of F\*, you will be dropped

.nix/bootstrap.nix

@@ -0,0 +1,25 @@
+{ fstar, fstar-dune, fstar-ocaml-snapshot, fstar-ulib, stdenv }:
+
+let
+  ocaml-src = stdenv.mkDerivation {
+    name = "src";
+    src = fstar-ocaml-snapshot;
+    dontBuild = true;
+    installPhase = ''
+      mkdir -p $out/ocaml
+      mv ./* $out/ocaml
+      cp ${../version.txt} $out/version.txt
+    '';
+  };
+  fstar-dune-bootstrap = fstar-dune.overrideAttrs (_: {
+    pname = "fstar-bootstrap-dune";
+    src = ocaml-src;
+  });
+  fstar-ulib-bootstrap = (fstar-ulib.override
+    (_: { fstar-dune = fstar-dune-bootstrap; })).overrideAttrs
+    (_: { pname = "fstar-bootstrap-ulib"; });
+
+in (fstar.override (_: {
+  fstar-dune = fstar-dune-bootstrap;
+  fstar-ulib = fstar-ulib-bootstrap;
+})).overrideAttrs (_: { pname = "fstar-bootstrap"; })

.nix/fstar.nix

@@ -0,0 +1,42 @@
+{ callPackage, fstar-dune, fstar-ulib, installShellFiles, lib, makeWrapper
+, stdenv, version, z3 }:
+
+stdenv.mkDerivation {
+  pname = "fstar";
+  inherit version;
+
+  buildInputs = [ installShellFiles makeWrapper ];
+
+  src = lib.sourceByRegex ./.. [
+    ".common.mk"
+    "doc.*"
+    "examples.*"
+    "src(/ocaml-output(/Makefile)?)?"
+    "ucontrib.*"
+  ];
+
+  dontBuild = true;
+
+  installPhase = ''
+    mkdir $out
+
+    CP="cp -r --no-preserve=mode"
+    $CP ${fstar-dune}/* $out
+    $CP ${fstar-ulib}/* $out
+
+    PREFIX=$out make -C src/ocaml-output install-sides
+
+    for binary in $out/bin/*
+    do
+      chmod +x $binary
+      wrapProgram $binary --prefix PATH ":" ${z3}/bin
+    done
+
+    cd $out
+    installShellCompletion --bash ${../.completion/bash/fstar.exe.bash}
+    installShellCompletion --fish ${../.completion/fish/fstar.exe.fish}
+    installShellCompletion --zsh --name _fstar.exe ${
+      ../.completion/zsh/__fstar.exe
+    }
+  '';
+}