diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b95d2e542..a5157c6ac 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -15,7 +15,8 @@ env: # - Dockerfile # - cryptol-remote-api/Dockerfile # - README.md - SOLVER_PKG_VERSION: "snapshot-20240212" + # - dev/dev_setup.sh + SOLVER_PKG_VERSION: "snapshot-20241119" # 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 @@ -78,12 +79,12 @@ jobs: run-tests: false # Windows and macOS CI runners are more expensive than Linux runners, # so we only build one particular GHC version to test them on. We - # include both an x86-64 macOS runner (macos-12) as well as an AArch64 + # include both an x86-64 macOS runner (macos-13) as well as an AArch64 # macOS runner (macos-14). - os: windows-2019 ghc-version: 9.4.8 run-tests: true - - os: macos-12 + - os: macos-13 ghc-version: 9.4.8 run-tests: true - os: macos-14 @@ -276,7 +277,7 @@ jobs: continue-on-error: false #- suite: rpc # target: '' - # os: macos-12 + # os: macos-13 # continue-on-error: false #- suite: rpc # target: '' diff --git a/Dockerfile b/Dockerfile index 3804254dd..d2b8cfa22 100644 --- a/Dockerfile +++ b/Dockerfile @@ -18,7 +18,7 @@ RUN mkdir -p rootfs/usr/local/bin WORKDIR /cryptol/rootfs/usr/local/bin # The URL here is based on the same logic used to specify BIN_ZIP_FILE in # `.github/workflow/ci.yml`, but specialized to x86-64 Ubuntu. -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20241119/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 096d2519a..cbee1f192 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-20240212). +of Z3, but you can see the specific version tested in CI by looking [here](https://github.com/GaloisInc/what4-solvers/releases/tag/snapshot-20241119). You can download Z3 binaries for a variety of platforms from their [releases page](https://github.com/Z3Prover/z3/releases). If you @@ -74,10 +74,11 @@ on [GitHub](https://github.com/GaloisInc/cryptol). Cryptol builds and runs on various flavors of Linux, Mac OS X, and Windows. We regularly build and test it in the following environments: -- macOS 12, 64-bit -- Ubuntu 20.04, 64-bit -- Ubuntu 22.04, 64-bit -- Windows Server 2019, 64-bit +- macOS 13 (x86-64) +- macOS 14 (ARM64) +- Ubuntu 20.04 (x86-64) +- Ubuntu 22.04 (x86-64) +- Windows Server 2019 (x86-64) ## Prerequisites diff --git a/cryptol-remote-api/Dockerfile b/cryptol-remote-api/Dockerfile index 4c93b8979..72179184c 100644 --- a/cryptol-remote-api/Dockerfile +++ b/cryptol-remote-api/Dockerfile @@ -82,7 +82,7 @@ RUN mkdir -p rootfs/"${CRYPTOLPATH}" \ WORKDIR /cryptol/rootfs/usr/local/bin # The URL here is based on the same logic used to specify BIN_ZIP_FILE in # `.github/workflow/ci.yml`, but specialized to x86-64 Ubuntu. -RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip" && \ +RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20241119/ubuntu-22.04-X64-bin.zip" && \ unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /cryptol/rootfs diff --git a/dev/dev_setup.sh b/dev/dev_setup.sh index db072cc2a..dec1bac89 100755 --- a/dev/dev_setup.sh +++ b/dev/dev_setup.sh @@ -17,7 +17,7 @@ # - In Ubuntu, we assume that the system has already run `apt-get update` # - In macOS, we assume the system has `brew` installed and on the path # -# There is some half-baked support for macOS 12 (x86_64), +# There is some half-baked support for macOS 13 (x86_64), # but it hasn't been tested. # @@ -37,9 +37,9 @@ GHCUP_URL="https://downloads.haskell.org/~ghcup" GHC_VERSION="9.4.8" CABAL_VERSION="3.10.3.0" -WHAT4_SOLVERS_SNAPSHOT="snapshot-20240212" +WHAT4_SOLVERS_SNAPSHOT="snapshot-20241119" WHAT4_SOLVERS_URL="https://github.com/GaloisInc/what4-solvers/releases/download/$WHAT4_SOLVERS_SNAPSHOT" -WHAT4_SOLVERS_MACOS_12="macos-12-X64-bin.zip" +WHAT4_SOLVERS_MACOS_13="macos-13-X64-bin.zip" WHAT4_SOLVERS_MACOS_14="macos-14-ARM64-bin.zip" WHAT4_SOLVERS_UBUNTU_20="ubuntu-20.04-X64-bin.zip" WHAT4_SOLVERS_UBUNTU_22="ubuntu-22.04-X64-bin.zip" @@ -49,7 +49,7 @@ WHAT4_Z3_VERSION="version 4.8.14" # Set of supported platforms: MACOS14="macos14" -MACOS12="macos12" # actually, this isn't supported yet +MACOS13="macos13" # actually, this isn't supported yet UBUNTU20="ubuntu-20.04" UBUNTU22="ubuntu-22.04" @@ -62,9 +62,9 @@ supported_platform() { Darwin) if [ $(uname -m) = "arm64" ]; then echo $MACOS14 - # This is how we'd support macOS 12. Since this hasn't been tested yet, + # This is how we'd support macOS 13. Since this hasn't been tested yet, # we withhold official support. - # This might bork on something running macOS <12, since we're basing + # This might bork on something running macOS <13, since we're basing # the it on the hardware, not the specific version. elif [ $(uname -m) = "x86_64" ]; then echo "" @@ -208,7 +208,7 @@ install_solvers() { notice "Installing cvc4, cvc5, and/or z3 solvers via direct download" case $CRYPTOL_PLATFORM in - $MACOS12) solvers_version=$WHAT4_SOLVERS_MACOS_12;; + $MACOS13) solvers_version=$WHAT4_SOLVERS_MACOS_13;; $MACOS14) solvers_version=$WHAT4_SOLVERS_MACOS_14;; $UBUNTU20) solvers_version=$WHAT4_SOLVERS_UBUNTU_20;; $UBUNTU22) solvers_version=$WHAT4_SOLVERS_UBUNTU_22;; @@ -278,7 +278,7 @@ check_version() { # be available on the user's path. This is particularly needed for GMP. put_brew_packages_in_path() { if $USED_BREW; then - # `brew --prefix` is different on macOS 12 and macOS 14 + # `brew --prefix` is different on macOS 13 and macOS 14 echo "export CPATH=$(brew --prefix)/include" >> $VAR_FILE echo "export LIBRARY_PATH=$(brew --prefix)/lib" >> $VAR_FILE fi