Merge branch 'master' of github.com:FStarLang/FStar into gebner_ocaml5

.ci/fsdoc.sh

@@ -24,7 +24,7 @@ pushd ulib
 FST_FILES=(FStar.*.fst FStar.*.fsti)
 
 # In case some files needs to be removed use this:
-# FST_FILES=( ${FST_FILES[@]/"prims.fst"} )
+# FST_FILES=( ${FST_FILES[@]/"Prims.fst"} )
 
 ../bin/fstar-any.sh --odir "../$FSDOC_ODIR" --doc ${FST_FILES[*]} 
 popd

.devcontainer/minimal.Dockerfile

@@ -1,4 +1,5 @@
-FROM ubuntu:23.10
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:22.04
 
 SHELL ["/bin/bash", "-c"]
 
@@ -42,11 +43,11 @@ RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a
     rm -f dotnet-sdk*.tar.gz
 
 # Install OCaml
-ARG OCAML_VERSION=4.12.0
+ARG OCAML_VERSION=4.14.0
 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
 RUN opam option depext-run-installs=true
 ENV OPAMYES=1
-RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
+RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib mtime pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
 
 # Get compiled Z3
 RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \

.docker/base.Dockerfile

@@ -8,9 +8,8 @@
 # and it is copied into the home directory on the image. CI jobs
 # will NOT use this file.
 
-# We always try to build against the most current ubuntu image.
-# FIXME: Broken with 24.04, fixing it to 23.10 so we can keep working
-FROM ubuntu:23.10
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:22.04
 
 RUN apt-get update
 

.docker/base/Dockerfile

@@ -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 sedlex ppx_deriving ppx_deriving_yojson process pprint visitors fix wasm ppxlib=0.22.0
+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
 
 # Prepare and build Z3
 ENV z3=z3-4.8.5-x64-debian-8.11

.docker/build/build_funs.sh

@@ -19,21 +19,26 @@ function export_home() {
 
 # By default, karamel master works against F* stable. Can also be overridden.
 function fetch_karamel() {
-    if [ ! -d karamel ]; then
-        git clone --depth 1 https://github.com/FStarLang/karamel karamel
-    fi
-
-    cd karamel
-    git fetch origin
     local ref=$(jq -c -r '.RepoVersions["karamel_version"]' "$rootPath/.docker/build/config.json" )
     if [[ $ref == "null" ]]; then
         echo "Unable to find RepoVersions.karamel_version on $rootPath/.docker/build/config.json"
         return -1
     fi
 
+    if [ ! -d karamel ]; then
+        # If we just want origin/master, we can shallow clone. Otherwise no,
+        # as we'll need to switch to some other branch/commit.
+        if [ x"$ref" = x"origin/master" ]; then
+            SHALLOW="--depth 1"
+        else
+            SHALLOW=""
+        fi
+        git clone ${SHALLOW} https://github.com/FStarLang/karamel karamel
+    fi
+
     echo Switching to KaRaMeL $ref
-    git reset --hard $ref
-    cd ..
+    git -C karamel reset --hard $ref
+
     export_home KRML "$(pwd)/karamel"
 
     # Install the Karamel dependencies
@@ -73,10 +78,6 @@ function fstar_default_build () {
         return 1
     fi
 
-    # Clean temporary build files, not needed and saves
-    # several hundred MB
-    make clean-buildfiles || true
-
     export_home FSTAR "$(pwd)"
 
     wait # for fetches above

.docker/nu_base.Dockerfile

@@ -0,0 +1,88 @@
+# For check-world workflow, should be coallesced to the other base.
+# This could definitely use a big cleanup too.
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:22.04
+
+RUN apt-get update
+
+# Base dependencies: opam
+# python3 (for interactive tests)
+RUN apt-get install -y --no-install-recommends \
+      git \
+      sudo \
+      python3 \
+      python-is-python3 \
+      opam \
+      rustc \
+      && apt-get clean -y
+
+# Create a new user and give them sudo rights
+# NOTE: we give them the name "opam" to keep compatibility with
+# derived hierarchical CI
+RUN useradd -d /home/opam opam
+RUN echo 'opam ALL=NOPASSWD: ALL' >> /etc/sudoers
+RUN mkdir /home/opam
+RUN chown opam:opam /home/opam
+USER opam
+ENV HOME /home/opam
+WORKDIR $HOME
+SHELL ["/bin/bash", "--login", "-c"]
+
+# Install GitHub CLI
+# From https://github.com/cli/cli/blob/trunk/docs/install_linux.md#debian-ubuntu-linux-raspberry-pi-os-apt
+# This is only used by the workflow that makes a release and publishes
+# it, but no harm in having it in the base.
+RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \
+    && curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg | sudo dd of=/usr/share/keyrings/githubcli-archive-keyring.gpg \
+    && sudo chmod go+r /usr/share/keyrings/githubcli-archive-keyring.gpg \
+    && echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" | sudo tee /etc/apt/sources.list.d/github-cli.list > /dev/null \
+    && sudo apt-get update \
+    && sudo apt-get install gh -y \
+    && sudo apt-get clean
+
+# Install OCaml
+ARG OCAML_VERSION=4.14.2
+RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
+RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+RUN opam option depext-run-installs=true
+ENV OPAMYES=1
+
+# F* dependencies. This is the only place where we read a file from
+# the F* repo.
+ADD fstar.opam $HOME/fstar.opam
+RUN opam install --confirm-level=unsafe-yes --deps-only $HOME/fstar.opam && opam clean
+
+# Some karamel dependencies
+RUN opam install --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex uucp ctypes ctypes-foreign && opam clean
+
+# Set up $HOME/bin. Note, binaries here take precedence over OPAM
+RUN mkdir $HOME/bin
+RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+
+WORKDIR $HOME
+
+RUN sudo apt-get install -y npm && sudo apt-get clean
+
+RUN sudo apt-get install -y --no-install-recommends \
+      time \
+      && sudo apt-get clean -y
+
+# To run Vale
+# RUN sudo apt-get install -y dotnet-runtime-6.0 dotnet-sdk-6.0
+
+RUN opam install --confirm-level=unsafe-yes mtime && opam clean
+
+# everparse (hex for quackyducky)
+RUN opam install --confirm-level=unsafe-yes hex sexplib re sha && opam clean
+
+# 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 wget -nv 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 && \
+    rm -f dotnet-sdk*.tar.gz
+    # echo 'export PATH=$PATH:$DOTNET_ROOT:$DOTNET_ROOT/tools' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile && \
+
+RUN sudo ln -s $DOTNET_ROOT/dotnet /usr/local/bin/dotnet

.docker/opam.Dockerfile

@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root FStar directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-ocaml-$ocaml_version
 
 # FIXME: the `opam depext` command should be unnecessary with opam 2.1

.docker/package.Dockerfile

@@ -1,7 +1,7 @@
 # This Dockerfile should be run from the root FStar directory
 
 # Build the package
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 ARG CI_THREADS=24
 
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild

.docker/release.Dockerfile

@@ -1,7 +1,7 @@
 # This Dockerfile should be run from the root FStar directory
 
 # Build the package
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 ARG CI_THREADS=24
 
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild

.github/setup-macos.sh

@@ -4,7 +4,7 @@
 # coreutils: for the `install` command used in install-ulib.sh
 export OPAMYES=1
 brew install opam bash gnu-getopt coreutils gnu-sed
-opam init --compiler=4.12.0
+opam init --compiler=4.14.0
 eval $(opam env)
 
 # Install Z3 and the opam package dependencies