From 693f82f1b12259413c6774652f41693c2a395822 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 11 Jul 2023 12:53:13 -0400 Subject: [PATCH] CI: Bump what4-solvers snapshot to 20230711 This includes the following changes: * The bindist URLs now include the OS architecture, I have tweaked the parts of CI that downloads bindists accordingly. * This snapshot includes `cvc5-1.0.5`, which has fixed a bug that was responsible for #1548. As such, this fixes #1548. --- .github/workflows/ci.yml | 6 +++--- Dockerfile | 2 +- README.md | 2 +- cryptol-remote-api/Dockerfile | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 20af5512..d70b5ab3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,7 +9,7 @@ on: workflow_dispatch: env: - SOLVER_PKG_VERSION: "snapshot-20221212" + SOLVER_PKG_VERSION: "snapshot-20230711" # The CACHE_VERSION can be updated to force the use of a new cache if # the current cache contents become corrupted/invalid. This can # sometimes happen when (for example) the OS version is changed but @@ -121,7 +121,7 @@ jobs: - shell: bash run: .github/ci.sh install_system_deps env: - BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip + BIN_ZIP_FILE: ${{ matrix.os }}-${{ runner.arch }}-bin.zip - shell: bash env: @@ -293,7 +293,7 @@ jobs: - shell: bash env: - BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip + BIN_ZIP_FILE: ${{ matrix.os }}-${{ runner.arch }}-bin.zip run: | set -x chmod +x dist/bin/cryptol diff --git a/Dockerfile b/Dockerfile index 21492e0d..d3bce2d0 100644 --- a/Dockerfile +++ b/Dockerfile @@ -14,7 +14,7 @@ USER cryptol WORKDIR /cryptol RUN mkdir -p rootfs/usr/local/bin WORKDIR /cryptol/rootfs/usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20230711/ubuntu-22.04-X64-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * WORKDIR /cryptol ENV PATH=/cryptol/rootfs/usr/local/bin:/home/cryptol/.local/bin:/home/cryptol/.ghcup/bin:$PATH diff --git a/README.md b/README.md index 20ddd570..ecaf569c 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,7 @@ Cryptol currently uses Microsoft Research's [Z3 SMT solver](https://github.com/Z3Prover/z3) by default to solve constraints during type checking, and as the default solver for the `:sat` and `:prove` commands. Cryptol generally requires the most recent version -of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20221212). +of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20230711). You can download Z3 binaries for a variety of platforms from their [releases page](https://github.com/Z3Prover/z3/releases). If you diff --git a/cryptol-remote-api/Dockerfile b/cryptol-remote-api/Dockerfile index 08dc2159..8f88d1f5 100644 --- a/cryptol-remote-api/Dockerfile +++ b/cryptol-remote-api/Dockerfile @@ -64,7 +64,7 @@ ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ && cp -r lib/* rootfs/"${CRYPTOLPATH}" WORKDIR /cryptol/rootfs/usr/local/bin -RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip" && \ +RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20230711/ubuntu-22.04-X64-bin.zip" && \ unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /cryptol/rootfs