Merge pull request #3631 from FStarLang/nik_z3_4.13.3

Upgrade F* to use Z3 4.13.3

.devcontainer/devcontainer.json

@@ -1,6 +1,7 @@
 {
   "name": "F* minimal devcontainer",
   "build": {
+    "context": "..",
     "dockerfile": "minimal.Dockerfile"
   },
   "customizations": {

.devcontainer/minimal.Dockerfile

@@ -17,6 +17,7 @@ RUN apt-get update \
       python3 \
       python-is-python3 \
       libgmp-dev \
+      pkg-config \
       opam \
     && apt-get clean -y
 # FIXME: libgmp-dev should be installed automatically by opam,
@@ -34,6 +35,10 @@ RUN mkdir -p $HOME/bin
 # Make sure ~/bin is in the PATH
 RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
 
+# Install Z3
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh ~/bin
+
 # Install dotnet
 ENV DOTNET_ROOT /home/$USER/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 && \
@@ -43,17 +48,12 @@ RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a
     rm -f dotnet-sdk*.tar.gz
 
 # Install OCaml
-ARG OCAML_VERSION=4.14.0
+ARG OCAML_VERSION=4.14.2
 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 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 \
- && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
- && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \
- && rm -r z3-4.8.5-*
+COPY ./fstar.opam .
+RUN opam install --deps-only . && rm fstar.opam
 
 WORKDIR $HOME
 

.docker/base.Dockerfile

@@ -33,22 +33,13 @@ RUN apt-get install -y --no-install-recommends \
       sudo \
       python3 \
       python-is-python3 \
+      pkg-config \
       opam \
       && apt-get clean -y
 
-# Install the Z3 versions we want to use in CI (4.8.5, 4.13.3). Note: we
-# currently also have 4.8.5 in the opam switch, as it is a dependency of
-# in fstar.opam, but that should be removed.
-
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
- && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
- && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 /usr/local/bin/z3-4.8.5 \
- && rm -r z3-4.8.5-*
-
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip \
- && unzip z3-4.13.3-x64-glibc-2.35 \
- && cp z3-4.13.3-x64-glibc-2.35/bin/z3 /usr/local/bin/z3-4.13.3 \
- && rm -r z3-4.13.3-*
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
 
 # Create a new user and give them sudo rights
 # NOTE: we give them the name "opam" to keep compatibility with

.docker/nu_base.Dockerfile

@@ -1,7 +1,7 @@
 # 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
+FROM ubuntu:24.04
 
 RUN apt-get update
 
@@ -10,12 +10,17 @@ RUN apt-get update
 RUN apt-get install -y --no-install-recommends \
       git \
       sudo \
+      ca-certificates \
       python3 \
       python-is-python3 \
       opam \
       rustc \
       && apt-get clean -y
 
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
+
 # Create a new user and give them sudo rights
 # NOTE: we give them the name "opam" to keep compatibility with
 # derived hierarchical CI
@@ -28,18 +33,6 @@ 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
@@ -50,6 +43,7 @@ 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

.nix/z3.nix

@@ -1,11 +1,18 @@
-{ fetchFromGitHub, z3 }:
+{ pkgs, stdenv, callPackage }:
 
-z3.overrideAttrs (old: rec {
-  version = "4.8.5";
-  src = fetchFromGitHub {
-    owner = "z3prover";
-    repo = "z3";
-    rev = "Z3-${version}";
-    sha256 = "ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
-  };
-})
+let
+  z3_4_8_5 = callPackage (import ./z3_4_8_5.nix) {};
+  z3_4_13_3 = callPackage (import ./z3_4_13_3.nix) {};
+in
+stdenv.mkDerivation {
+  pname = "fstar-z3";
+  version = "1";
+
+  dontUnpack = true;
+
+  buildPhase = ''
+    mkdir -p $out/bin
+    ln -s ${z3_4_8_5}/bin/z3 $out/bin/z3-4.8.5
+    ln -s ${z3_4_13_3}/bin/z3 $out/bin/z3-4.13.3
+  '';
+}

.nix/z3_4_13_3.nix

@@ -0,0 +1,11 @@
+{ fetchFromGitHub, z3 }:
+
+z3.overrideAttrs (old: rec {
+  version = "4.13.3";
+  src = fetchFromGitHub {
+    owner = "z3prover";
+    repo = "z3";
+    rev = "z3-${version}";
+    sha256 = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA=";
+  };
+})

.nix/z3_4_8_5.nix

@@ -0,0 +1,11 @@
+{ fetchFromGitHub, z3 }:
+
+z3.overrideAttrs (old: rec {
+  version = "4.8.5";
+  src = fetchFromGitHub {
+    owner = "z3prover";
+    repo = "z3";
+    rev = "Z3-${version}";
+    sha256 = "ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
+  };
+})