Merge with main

.github/actions/install-cvc5/action.yml

@@ -0,0 +1,52 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install cvc5
+description: >
+  Download a static cvc5 build and put it on the PATH. Supports both
+  x86_64 and aarch64 Linux runners. Consolidates the cvc5 install logic
+  previously duplicated across ci.yml and cbmc.yml; intended to also be
+  adopted by the python-fuzz workflow once that lands (see
+  https://github.com/strata-org/Strata/pull/984).
+
+inputs:
+  version:
+    description: cvc5 release tag (e.g. "1.2.1").
+    required: false
+    default: "1.2.1"
+  install-to:
+    description: >
+      Where to make the cvc5 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the cvc5 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download cvc5
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)         ARCH_NAME="x86_64" ;;
+          aarch64|arm64)  ARCH_NAME="arm64" ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        URL="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/cvc5-Linux-${ARCH_NAME}-static.zip"
+        wget -q "$URL"
+        unzip -q "cvc5-Linux-${ARCH_NAME}-static.zip"
+        chmod +x "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac

.github/actions/install-z3/action.yml

@@ -0,0 +1,55 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install z3
+description: >
+  Download a z3 release and put it on the PATH. Supports x86_64 and
+  aarch64 Linux runners. Consolidates the z3 install logic previously
+  duplicated across ci.yml and cbmc.yml.
+
+inputs:
+  version:
+    description: z3 release tag (e.g. "4.15.2").
+    required: false
+    default: "4.15.2"
+  install-to:
+    description: >
+      Where to make the z3 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the z3 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download z3
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-x64-glibc-2.39.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-x64-glibc-2.39"
+            ;;
+          aarch64|arm64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-arm64-glibc-2.34.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-arm64-glibc-2.34"
+            ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        wget -q "$URL"
+        unzip -q "${ARCHIVE_NAME}.zip"
+        chmod +x "${ARCHIVE_NAME}/bin/z3"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "${ARCHIVE_NAME}/bin/z3" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac

.github/actions/restore-lake-cache/action.yml

@@ -0,0 +1,82 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Restore lake cache
+description: >
+  Thin wrapper around actions/cache/restore@v5 that uses the standard
+  Strata cache-key pattern:
+    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<all .st files>-<sha>
+  with three fallback keys dropping each trailing component in turn.
+  Consolidates the ~15-line cache block previously duplicated across
+  ci.yml's build_and_test_lean, check_pending_python, build_python and
+  cbmc.yml; intended to also be adopted by the python-fuzz workflow once
+  that lands (see https://github.com/strata-org/Strata/pull/984).
+
+inputs:
+  fail-on-cache-miss:
+    description: >
+      If 'true', the step fails when no cache entry matches. Use this in
+      jobs that depend on a cache saved by an upstream job for the same
+      SHA (see https://github.com/strata-org/Strata/issues/952).
+    required: false
+    default: "false"
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Prefix used in the cache key. The action also hashes the
+      repo-root `lean-toolchain` and `lake-manifest.json`, so changing
+      only this prefix is appropriate for caches keyed on the same
+      root-level Lean build (e.g. distinguishing different artifact
+      names with the same source set). Sub-projects with their own
+      toolchain/manifest do not currently fit this action and should
+      not reuse it as-is.
+    required: false
+    default: "lake"
+  use-restore-keys:
+    description: >
+      Must be the string `'true'` or `'false'`.
+
+      If `'true'` (default), include three fallback `restore-keys` so
+      that a near match (same toolchain/manifest/.st files but different
+      SHA) is used when no exact-SHA cache exists.
+
+      Set to `'false'` for downstream jobs that depend on a cache saved
+      by an upstream job for the *same* SHA (typically together with
+      `fail-on-cache-miss: 'true'`); see
+      https://github.com/strata-org/Strata/issues/952. With fallback
+      keys present, `fail-on-cache-miss` only triggers when every
+      fallback also misses, which silently allows stale cross-SHA cache
+      matches and defeats the safety net.
+    required: false
+    default: "true"
+
+outputs:
+  cache-hit:
+    description: Whether a cache entry was restored (see actions/cache/restore@v5).
+    value: ${{ steps.restore-with-fallback.outputs.cache-hit || steps.restore-exact.outputs.cache-hit }}
+
+runs:
+  using: composite
+  steps:
+    - name: Restore lake cache (with fallback keys)
+      id: restore-with-fallback
+      if: inputs.use-restore-keys != 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}
+    - name: Restore lake cache (exact SHA only)
+      id: restore-exact
+      if: inputs.use-restore-keys == 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}

.github/actions/save-lake-cache/action.yml

@@ -0,0 +1,35 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Save lake cache
+description: >
+  Save the lake build cache using the canonical Strata cache-key pattern.
+  Companion to `restore-lake-cache`: the two actions share the same key
+  construction so downstream jobs that consume the saved cache via
+  `restore-lake-cache` with `use-restore-keys: "false"` will hit it
+  reliably.
+
+  Use this in workflows that produce a fresh build (typically the
+  `build_and_test_lean` job in ci.yml) to share the result with
+  downstream jobs at the same SHA.
+
+inputs:
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Cache-key prefix; must match the `key-prefix` passed to the
+      companion `restore-lake-cache` action so that the exact-SHA
+      restore keys line up.
+    required: false
+    default: "lake"
+
+runs:
+  using: composite
+  steps:
+    - name: Save lake cache
+      uses: actions/cache/save@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}

.github/scripts/testStrataCommand.sh

@@ -81,6 +81,15 @@ $strata print --include Examples/dialects Examples/dialects/Arith.dialect.st > "
 # Print Ion file and compare with previous run
 $strata print --include Examples/dialects "$temp_dir/Arith.dialect.st.ion" | cmp - "$temp_dir/Arith.dialect.st"
 
+# --- pyResolveOverloads error handling ---
+set +e
+
+expect_error "pyResolveOverloads missing dispatch file" \
+  "nonexistent_dispatch.ion" \
+  $strata pyResolveOverloads Examples/SimpleProc.core.st nonexistent_dispatch.ion
+
+set -e
+
 if [ $failed -ne 0 ]; then
   echo "Some tests failed."
   exit 1

.github/workflows/cbmc.yml

@@ -13,38 +13,9 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v6
       - name: Install cvc5
-        shell: bash
-        run: |
-              ARCH=$(uname -m)
-              if [ "$ARCH" = "x86_64" ]; then
-                ARCH_NAME="x86_64"
-              elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then
-                ARCH_NAME="arm64"
-              else
-                echo "Unsupported architecture: $ARCH"
-                exit 1
-              fi
-              wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip
-              unzip -q cvc5-Linux-${ARCH_NAME}-static.zip
-              chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5
-              echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH
+        uses: ./.github/actions/install-cvc5
       - name: Install z3
-        shell: bash
-        run: |
-              ARCH=$(uname -m)
-              if [ "$ARCH" = "x86_64" ]; then
-                wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip
-                ARCHIVE_NAME="z3-4.15.2-x64-glibc-2.39"
-              elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then
-                wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip
-                ARCHIVE_NAME="z3-4.15.2-arm64-glibc-2.34"
-              else
-                echo "Unsupported architecture: $ARCH"
-                exit 1
-              fi
-              unzip -q "${ARCHIVE_NAME}.zip"
-              chmod +x "${ARCHIVE_NAME}/bin/z3"
-              echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> $GITHUB_PATH
+        uses: ./.github/actions/install-z3
       - name: Prepare ccache
         uses: actions/cache@v5
         with:
@@ -77,11 +48,10 @@ jobs:
         # The cache is safe to use here because we just saved it for this exact SHA
         # in the build_and_test_lean job from ci.yml
         # https://github.com/strata-org/Strata/issues/952
-        uses: actions/cache/restore@v5
+        uses: ./.github/actions/restore-lake-cache
         with:
-          path: .lake
-          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
-          fail-on-cache-miss: true
+          fail-on-cache-miss: "true"
+          use-restore-keys: "false"
       - name: Build Strata
         uses: leanprover/lean-action@v1
         with: