Bump the minimal version of Why to 1.7

This allows us to use more recent versions of the provers.

The docker images have been updated accordingly.

This commit disables alt-ergo in nix-shell that currently
does not compile on Apple silicon.

README.md

@@ -34,7 +34,7 @@ EasyCrypt uses the following third-party tools/libraries:
 
  * OCamlbuild
 
- * Why3 (= 1.6.x)
+ * Why3 (>= 1.7.x, < 1.8)
 
      Available at <http://why3.lri.fr/>
 
@@ -202,20 +202,16 @@ Why3 and SMT solvers are independent pieces of software with their
 own version-specific interactions. Obtaining a working SMT setup may
 require installing specific versions of some of the provers.
 
-At the time of writing, we depend on Why3 1.6.x, which supports the
+At the time of writing, we depend on Why3 1.7.x, which supports the
 following prover versions:
 
- * Alt-Ergo 2.4.2
+ * Alt-Ergo 2.5.2
  * CVC4 1.8
- * Z3 4.12.1
+ * CVC5 1.0.5
+ * Z3 4.12.x
 
 `alt-ergo` can be installed using opam, if you do you can use pins to
-select a specific version (e.g, `opam pin alt-ergo 2.4.1`).
-
-Development branches use `dune-3.x` and which is incompatible with
-`alt-ergo-2.4.1`. In this case, you can use `alt-ergo-2.4.2`. The
-warning "Prover Alt-Ergo version 2.4.2 is not recognized." upon
-configuration (see below) can be [safely ignored](https://gitlab.inria.fr/why3/why3/-/commit/f2863d84f65824f21afd75546117becbf453efcc).
+select a specific version (e.g, `opam pin alt-ergo 2.5.2`).
 
 Installing/Compiling EasyCrypt
 ====================================================================

default.nix

@@ -16,7 +16,6 @@ in
 
 let provers =
   if withProvers then [
-    alt-ergo-pin
     cvc4-pin
     cvc5-pin
     z3-pin

dune-project

@@ -21,7 +21,7 @@
   dune-site
   (ocaml-inifiles (>= 1.2))
   (pcre (>= 7))
-  (why3 (and (>= 1.6.0) (< 1.8)))
+  (why3 (and (>= 1.7.0) (< 1.8)))
   yojson
   (zarith (>= 1.10))
 ))

easycrypt.opam

@@ -9,7 +9,7 @@ depends: [
   "dune-site"
   "ocaml-inifiles" {>= "1.2"}
   "pcre" {>= "7"}
-  "why3" {>= "1.6.0" & < "1.8"}
+  "why3" {>= "1.7.0" & < "1.8"}
   "yojson"
   "zarith" {>= "1.10"}
   "odoc" {with-doc}

scripts/docker/Makefile

@@ -20,7 +20,7 @@ all:
 	cd $*-test-box && docker build -t $(DNAME)/ec-$*-test-box .
 
 %-build: __force__
-	cd $* && docker build -t $(DNAME)/ec-$* .
+	cd $* && docker build --platform linux/amd64 -t $(DNAME)/ec-$* .
 
 %-publish: __force__
 	cd $* && docker push $(DNAME)/ec-$*:latest

scripts/docker/build-box/Dockerfile

@@ -5,31 +5,35 @@ MAINTAINER Pierre-Yves Strub <[email protected]>
 ENV DEBIAN_FRONTEND noninteractive
 
 RUN \
-	sudo apt-get -q -y install wget curl python3 python3-pip && \
-	sudo apt-get -q -y clean && \
-	sudo pip3 install --no-cache-dir pyyaml
+	sudo apt-get -q -y install wget curl python3 python3-pip python3-yaml && \
+	sudo apt-get -q -y clean
 
 RUN \
 	opam pin add -n easycrypt https://github.com/EasyCrypt/easycrypt.git && \
-	opam install depext && opam depext easycrypt && \
-	opam install --deps-only easycrypt && \
+	opam install --deps-only --confirm-level=unsafe-yes easycrypt && \
 	opam clean
 
-ENV ALTERGO=2.4.2 CVC4V=1.8 Z3V=4.8.10 Z3SV= Z3A=ubuntu-18.04
+ENV ALTERGO=2.5.2 CVC4=1.8 CVC5=1.0.6 Z3=4.12.2 Z3GLIBC=2.35
 
 RUN \
-	opam pin add -n alt-ergo ${ALTERGO} && \
-        opam depext alt-ergo && opam install alt-ergo && opam clean
+	wget -O z3.zip https://github.com/Z3Prover/z3/releases/download/z3-${Z3}/z3-${Z3}-x64-glibc-${Z3GLIBC}.zip && \
+        unzip -j z3.zip z3-${Z3}-x64-glibc-${Z3GLIBC}/bin/z3 && \
+        sudo cp z3 /usr/local/bin/ && sudo chmod 755 /usr/local/bin/z3 && \
+	rm -rf z3 z3.zip
 
 RUN \
-        wget -O cvc4 https://github.com/cvc5/cvc5/releases/download/${CVC4V}/cvc4-${CVC4V}-x86_64-linux-opt && \
+        wget -O cvc4 https://github.com/cvc5/cvc5/releases/download/${CVC4}/cvc4-${CVC4}-x86_64-linux-opt && \
         sudo mv cvc4 /usr/local/bin/ && sudo chmod 755 /usr/local/bin/cvc4
 
 RUN \
-        wget https://github.com/Z3Prover/z3/releases/download/z3-${Z3V}/z3-${Z3V}${Z3SV}-x64-${Z3A}.zip && \
-        unzip -j z3-${Z3V}${Z3SV}-x64-${Z3A}.zip z3-${Z3V}${Z3SV}-x64-${Z3A}/bin/z3 && \
-        sudo cp z3 /usr/local/bin/ && sudo chmod 755 /usr/local/bin/z3 && \
-	rm -rf z3 z3-${Z3V}${Z3SV}-x64-${Z3A}.zip
+        wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5}/cvc5-Linux && \
+        sudo mv cvc5 /usr/local/bin/ && sudo chmod 755 /usr/local/bin/cvc5
+
+RUN \
+	opam pin add -n alt-ergo ${ALTERGO} && \
+	opam install --deps-only --confirm-level=unsafe-yes alt-ergo && \
+        opam install alt-ergo && \
+	opam clean
 
 RUN \
-	opam config exec -- why3 config detect
+	opam exec -- why3 config detect

scripts/nix/alt-ergo/default.nix

@@ -4,46 +4,34 @@ with import nixpkgs { };
 
 let
   pname = "alt-ergo";
-  version = "2.4.2";
+  version = "2.5.2";
 
-  configureScript = "ocaml unix.cma configure.ml";
-
-  src = fetchFromGitHub {
-    owner = "OCamlPro";
-    repo = pname;
-    rev = version;
-    hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc=";
+  src = fetchurl {
+    url = "https://github.com/OCamlPro/alt-ergo/releases/download/v${version}/alt-ergo-${version}.tbz";
+    hash = "sha256-9GDBcBH49sheO5AjmDsznMEbw0JSrnSOcIIRN40/aJU=";
   };
 in
 
 let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
   pname = "alt-ergo-lib";
-  inherit version src configureScript;
-  configureFlags = [ pname ];
-  nativeBuildInputs = [ which ];
-  buildInputs = with ocamlPackages; [ dune-configurator ];
-  propagatedBuildInputs = with ocamlPackages; [ dune-build-info num ocplib-simplex seq stdlib-shims zarith ];
-  preBuild = ''
-    substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
-  '';
+  inherit version src;
+  buildInputs = with ocamlPackages; [ ppx_blob ];
+  propagatedBuildInputs = with ocamlPackages; [ camlzip dolmen_loop dune-build-info fmt ocplib-simplex seq stdlib-shims zarith ];
 }; in
 
 let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
   pname = "alt-ergo-parsers";
-  inherit version src configureScript;
-  configureFlags = [ pname ];
-  nativeBuildInputs = [ which ocamlPackages.menhir ];
-  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+  inherit version src;
+  nativeBuildInputs = [ ocamlPackages.menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ psmt2-frontend ]);
 }; in
 
 ocamlPackages.buildDunePackage {
 
-  inherit pname version src configureScript;
-
-  configureFlags = [ pname ];
+  inherit pname version src;
 
-  nativeBuildInputs = [ which ocamlPackages.menhir ];
-  buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ];
+  nativeBuildInputs = [ ocamlPackages.menhir ];
+  buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [ cmdliner dune-site ]);
 
   meta = {
     description = "High-performance theorem prover and SMT solver";