diff --git a/README.md b/README.md
index 7dbbd61c71..38ddbce947 100644
--- a/README.md
+++ b/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
@@ -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
====================================================================
diff --git a/default.nix b/default.nix
index 9403fa8c9d..e59d76c363 100644
--- a/default.nix
+++ b/default.nix
@@ -16,7 +16,6 @@ in
let provers =
if withProvers then [
- alt-ergo-pin
cvc4-pin
cvc5-pin
z3-pin
diff --git a/dune-project b/dune-project
index 69b48bb937..a8bc5091e4 100644
--- a/dune-project
+++ b/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))
))
diff --git a/easycrypt.opam b/easycrypt.opam
index 9af04487d7..a1c17689c9 100644
--- a/easycrypt.opam
+++ b/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}
diff --git a/scripts/docker/Makefile b/scripts/docker/Makefile
index e9d4ec22e2..870f274290 100644
--- a/scripts/docker/Makefile
+++ b/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
diff --git a/scripts/docker/build-box/Dockerfile b/scripts/docker/build-box/Dockerfile
index 39accc5b65..ddb50c2889 100644
--- a/scripts/docker/build-box/Dockerfile
+++ b/scripts/docker/build-box/Dockerfile
@@ -5,31 +5,35 @@ MAINTAINER Pierre-Yves Strub
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
diff --git a/scripts/nix/alt-ergo/default.nix b/scripts/nix/alt-ergo/default.nix
index cd175f7f2f..f2d96550fd 100644
--- a/scripts/nix/alt-ergo/default.nix
+++ b/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";