Bump the minimal version of Why to 1.7

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

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,15 @@ 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
- * CVC4 1.8
- * Z3 4.12.1
+ * Alt-Ergo 2.4.3
+ * 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.4.3`).
 
 Installing/Compiling EasyCrypt
 ====================================================================

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

@@ -2,8 +2,8 @@
 
 # --------------------------------------------------------------------
 # docker.com account name
-DNAME ?= ghcr.io/easycrypt
-BBOX  := build-box test-box
+DNAME  ?= ghcr.io/easycrypt
+BBOX   := build-box test-box
 
 # --------------------------------------------------------------------
 .PHONY: all __force__
@@ -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.4.3 CVC4=1.8 CVC5=1.0.5 Z3=4.12.1 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