From c365d59d61219ce0139fb7f1406c2048f1a38d07 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 15 Apr 2026 16:03:19 +0100 Subject: [PATCH 1/2] [docker] provers: bump alt-ergo to 2.6.3 --- scripts/docker/Dockerfile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/docker/Dockerfile.build b/scripts/docker/Dockerfile.build index 3966522d7..0a979ed2c 100644 --- a/scripts/docker/Dockerfile.build +++ b/scripts/docker/Dockerfile.build @@ -16,7 +16,7 @@ COPY --chmod=0755 --chown=1001:0 docker-parts/alt-ergo bin/run-alt-ergo ENV PATH="/home/charlie/bin:$PATH" RUN \ - version=2.6.2 && \ + version=2.6.3 && \ opam switch create --no-switch alt-ergo-${version} ocaml-system && \ opam pin --switch=alt-ergo-${version} add -n alt-ergo ${version} && \ opam install --switch=alt-ergo-${version} --deps-only --confirm-level=unsafe-yes alt-ergo && \ From 557a14dde0b7dbd4f224ece47df533dfe8069183 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Wed, 15 Apr 2026 16:03:29 +0100 Subject: [PATCH 2/2] REVERT ME --- .github/workflows/ci.yml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86a9f8b14..dca2147c5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -60,6 +60,17 @@ jobs: target: [unit, stdlib, examples] steps: - uses: actions/checkout@v4 + - name: Install latest alt-ergo + run: | + opam remove --switch=alt-ergo-2.6.2 alt-ergo + opam update + opam switch create --no-switch alt-ergo-2.6.3 ocaml-system + opam pin --switch=alt-ergo-2.6.3 add -n alt-ergo 2.6.3 + opam install --switch=alt-ergo-2.6.3 --deps-only --confirm-level=unsafe-yes alt-ergo + opam install --switch=alt-ergo-2.6.3 alt-ergo + opam clean --switch=alt-ergo-2.6.3 + ln -s run-alt-ergo ~/bin/alt-ergo-2.6.3 + opam exec -- why3 config detect - name: Install EasyCrypt dependencies run: | opam pin add -n easycrypt . @@ -135,6 +146,16 @@ jobs: opam install --deps-only easycrypt - name: Compile & Install EasyCrypt run: opam exec -- make -C easycrypt build install + - name: Install latest alt-ergo + run: | + opam remove --switch=alt-ergo-2.6.2 alt-ergo + opam update + opam switch create --no-switch alt-ergo-2.6.3 ocaml-system + opam pin --switch=alt-ergo-2.6.3 add -n alt-ergo 2.6.3 + opam install --switch=alt-ergo-2.6.3 --deps-only --confirm-level=unsafe-yes alt-ergo + opam install --switch=alt-ergo-2.6.3 alt-ergo + opam clean --switch=alt-ergo-2.6.3 + ln -s run-alt-ergo ~/bin/alt-ergo-2.6.3 - name: Detect SMT provers run: | rm -f ~/.why3.conf ~/.config/easycrypt/why3.conf