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
+ }
+ '';
+}