CI: Build and test both x86-64 and AArch64 macOS

.github/ci.sh

@@ -121,14 +121,14 @@ sign() {
 
 zip_dist() {
   : "${VERSION?VERSION is required as an environment variable}"
-  name="${name:-"cryptol-$VERSION-$OS_TAG-x86_64"}"
+  name="${name:-"cryptol-$VERSION-$OS_TAG-$ARCH_TAG"}"
   cp -r dist "$name"
   tar -cvzf "$name".tar.gz "$name"
 }
 
 zip_dist_with_solvers() {
   : "${VERSION?VERSION is required as an environment variable}"
-  name="${name:-"cryptol-$VERSION-$OS_TAG-x86_64"}"
+  name="${name:-"cryptol-$VERSION-$OS_TAG-$ARCH_TAG"}"
   sname="${name}-with-solvers"
   cp "$(which abc)"        dist/bin/
   cp "$(which cvc4)"       dist/bin/

.github/workflows/ci.yml

@@ -15,7 +15,7 @@ env:
   # - Dockerfile
   # - cryptol-remote-api/Dockerfile
   # - README.md
-  SOLVER_PKG_VERSION: "snapshot-20230711"
+  SOLVER_PKG_VERSION: "snapshot-20240212"
   # 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
@@ -64,24 +64,30 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-22.04, macos-12, windows-2019]
+        os: [ubuntu-22.04]
         ghc-version: ["9.2.8", "9.4.7", "9.6.2"]
         cabal: [ '3.10.1.0' ]
         run-tests: [true]
-        exclude:
-          - os: windows-2019
-            ghc-version: 9.4.7
-            run-tests: true
-          - os: windows-2019
-            ghc-version: 9.6.2
-            run-tests: true
         include:
           # We include one job from an older Ubuntu LTS release to increase our
           # coverage of possible Linux configurations. Since we already run the
           # tests with the newest LTS release, we won't bother testing this one.
           - os: ubuntu-20.04
             ghc-version: 9.2.8
             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
+          # macOS runner (macos-14).
+          - os: windows-2019
+            ghc-version: 9.2.8
+            run-tests: true
+          - os: macos-12
+            ghc-version: 9.2.8
+            run-tests: true
+          - os: macos-14
+            ghc-version: 9.2.8
+            run-tests: true
     outputs:
       test-lib-json: ${{ steps.test-lib.outputs.targets-json }}
     env:
@@ -181,19 +187,21 @@ jobs:
 
       - shell: bash
         run: |
-          NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64"
+          NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}"
           echo "NAME=$NAME" >> $GITHUB_ENV
           .github/ci.sh zip_dist $NAME
         env:
           OS_TAG: ${{ matrix.os }}
+          ARCH_TAG: ${{ runner.arch }}
 
       - shell: bash
         run: |
-          NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64"
+          NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-${{ runner.arch }}"
           echo "NAME=$NAME" >> $GITHUB_ENV
           .github/ci.sh zip_dist_with_solvers $NAME
         env:
           OS_TAG: ${{ matrix.os }}
+          ARCH_TAG: ${{ runner.arch }}
 
       - if: github.event.pull_request.head.repo.fork == false
         shell: bash
@@ -222,13 +230,13 @@ jobs:
         uses: actions/upload-artifact@v2
         with:
           path: dist/bin
-          name: ${{ runner.os }}-dist-bin
+          name: ${{ matrix.os }}-dist-bin
 
       - if: matrix.ghc-version == '9.2.8' && matrix.run-tests
         uses: actions/upload-artifact@v2
         with:
           path: bin
-          name: ${{ runner.os }}-bin
+          name: ${{ matrix.os }}-bin
 
       - uses: actions/upload-artifact@v2
         if: runner.os == 'Windows'
@@ -256,7 +264,7 @@ jobs:
       matrix:
         suite: [test-lib]
         target: ${{ fromJson(needs.build.outputs.test-lib-json) }}
-        os: [ubuntu-22.04, macos-12, windows-2019]
+        os: [ubuntu-22.04, macos-14, windows-2019]
         continue-on-error: [false]
         include:
           - suite: rpc
@@ -280,6 +288,24 @@ jobs:
         with:
           ghc-version: '9.2.8'
 
+      # Homebrew installs packages in different directories depending on which
+      # macOS architecture you are using:
+      #
+      # * /usr/local (X64)
+      # * /opt/homebrew (ARM64)
+      #
+      # Clang automatically searches in /usr/local without any additional setup,
+      # but it doesn't know about /opt/homebrew. As such, we have to teach Clang
+      # to do so by setting the appropriate environment variables.
+      #
+      # This step is important for the FFI unit tests, which rely on a
+      # Homebrew-provided version of gmp.
+      - name: Teach Clang about Homebrew paths (macOS ARM64)
+        run: |
+          echo "CPATH=/opt/homebrew/include" >> $GITHUB_ENV
+          echo "LIBRARY_PATH=/opt/homebrew/lib" >> $GITHUB_ENV
+        if: matrix.suite == 'test-lib' && runner.os == 'macOS' && runner.arch == 'ARM64'
+
       - name: Install dependencies (Windows)
         uses: msys2/setup-msys2@v2
         with:
@@ -305,12 +331,12 @@ jobs:
 
       - uses: actions/download-artifact@v2
         with:
-          name: "${{ runner.os }}-dist-bin"
+          name: "${{ matrix.os }}-dist-bin"
           path: dist/bin
 
       - uses: actions/download-artifact@v2
         with:
-          name: "${{ runner.os }}-bin"
+          name: "${{ matrix.os }}-bin"
           path: bin
 
       - shell: bash

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-20230711/ubuntu-22.04-X64-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/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

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-20230711).
+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).
 
 You can download Z3 binaries for a variety of platforms from their
 [releases page](https://github.com/Z3Prover/z3/releases). If you

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-20230711/ubuntu-22.04-X64-bin.zip" && \
+RUN curl -sL -o solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip" && \
     unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /cryptol/rootfs

src/Cryptol/Backend/Arch.hs

@@ -17,9 +17,9 @@ module Cryptol.Backend.Arch where
 -- experiments show that it's somewhere under 2^37 at least on 64-bit
 -- Mac OS X.
 maxBigIntWidth :: Integer
-#if i386_HOST_ARCH
+#if defined(i386_HOST_ARCH)
 maxBigIntWidth = 2^(32 :: Integer) - 0x1
-#elif x86_64_HOST_ARCH
+#elif defined(x86_64_HOST_ARCH) || defined(aarch64_HOST_ARCH)
 maxBigIntWidth = 2^(37 :: Integer) - 0x100
 #else
 -- Because GHC doesn't seem to define a CPP macro that will portably