build: enable Lake artifact caching

.github/actions/lean-ci-setup/action.yml

@@ -5,6 +5,12 @@
 name: Lean CI Setup
 description: Install system dependencies, elan, and restore Lean/Lake caches for CI jobs.
 
+inputs:
+  save-lake-artifact-cache:
+    description: Save the restored Lake artifact cache when the job succeeds.
+    required: false
+    default: "false"
+
 runs:
   using: composite
   steps:
@@ -27,6 +33,7 @@ runs:
         path: |
           ~/.elan/toolchains
           ~/.elan/settings.toml
+          !~/.elan/toolchains/*/lake/cache
         key: ${{ runner.os }}-elan-${{ hashFiles('lean-toolchain') }}
 
     - name: Restore Lake Package Cache
@@ -41,3 +48,35 @@ runs:
         elan --version
         lean --version
         lake --version
+
+    - name: Resolve Lake Artifact Cache
+      id: lake-artifact-cache
+      shell: bash
+      run: |
+        lake_bin="$(elan which lake)"
+        toolchain_root="${lake_bin%/bin/lake}"
+        if [[ "${toolchain_root}" == "${lake_bin}" ]]; then
+          echo "error: could not resolve the active Lake toolchain root" >&2
+          exit 1
+        fi
+        cache_dir="${toolchain_root}/lake/cache"
+        mkdir -p "${cache_dir}"
+        printf 'dir=%s\n' "${cache_dir}" >> "${GITHUB_OUTPUT}"
+
+    - name: Restore Lake Artifact Cache
+      if: inputs.save-lake-artifact-cache != 'true'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ steps.lake-artifact-cache.outputs.dir }}
+        key: ${{ runner.os }}-${{ runner.arch }}-lake-artifacts-v2-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ runner.os }}-${{ runner.arch }}-lake-artifacts-v2-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-
+
+    - name: Restore And Save Lake Artifact Cache
+      if: inputs.save-lake-artifact-cache == 'true'
+      uses: actions/cache@v5
+      with:
+        path: ${{ steps.lake-artifact-cache.outputs.dir }}
+        key: ${{ runner.os }}-${{ runner.arch }}-lake-artifacts-v2-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ runner.os }}-${{ runner.arch }}-lake-artifacts-v2-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-

.github/workflows/ci.yml

@@ -76,6 +76,8 @@ jobs:
       - uses: actions/checkout@v6
 
       - uses: ./.github/actions/lean-ci-setup
+        with:
+          save-lake-artifact-cache: "true"
 
       - name: Beam Fast Test
         run: bash tests/test-beam-fast.sh

CHANGELOG.md

@@ -33,6 +33,9 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY
 
 ### Changed
 
+- Local builds now write to Lake's toolchain-scoped artifact cache and restore cached outputs into
+  `.lake/build`, preserving the paths used by Beam's wrapper, installer, and tests. CI restores that
+  cache for Lean jobs and lets one job per OS publish each commit's updated cache.
 - Wrapper lifecycle commands now use the explicit `serve`, `status`, and `stop` vocabulary;
   `stop` and `recover` require `--root`, alternate selectors use `--session-dir`, and wrapper
   descriptors contain exactly one frozen workspace. Successful lifecycle commands use typed

docs/DEVELOPMENT.md

@@ -570,6 +570,24 @@ What this does not promise:
 
 ## Recommended Test Order
 
+Beam enables Lake's toolchain-scoped local artifact cache. Cached artifacts are restored into the
+ordinary `.lake/build` layout because the wrapper, installer, and test harnesses consume those
+paths directly. This lets task worktrees reuse unchanged compilation outputs without changing the
+repository's runtime layout contract. For a genuinely cold Beam rebuild, point `LAKE_CACHE_DIR` at
+a fresh temporary directory; Lake's `--no-cache` option controls remote package caches rather than
+this explicit local package cache. Restricted automation that cannot write to the default cache
+inside the elan toolchain must likewise point `LAKE_CACHE_DIR` at a writable directory; sharing
+that directory between task worktrees preserves the intended reuse. The save/checkpoint regression
+suite uses separate fixture packages and disables their artifact caches so a Lake replay cannot
+masquerade as a Beam-written artifact.
+
+CI restores the artifact cache for every Lean job, while `beam-fast` is the single writer for each
+OS and commit. Keeping one writer avoids concurrent immutable GitHub cache entries and bounds cache
+growth. CI archives the active root toolchain's exact Lake cache directory separately from the elan
+toolchain cache. It does not override `LAKE_CACHE_DIR`, so compatibility tests that select another
+toolchain continue using Lake's toolchain-isolated default instead of replaying incompatible native
+artifacts.
+
 - LSP request / handle / scenario changes: `bash tests/test-lsp.sh`
 - Beam broker protocol / stream / barrier changes: `bash tests/test-beam-fast.sh`
 - Beam save replay changes: `bash tests/test-beam-save-olean.sh`

lakefile.lean

@@ -10,6 +10,8 @@ open Lake DSL
 open System
 
 package "beam" where
+  enableArtifactCache := true
+  restoreAllArtifacts := true
 
 target beamControlDirObj (pkg) : FilePath := do
   let srcFile := pkg.dir / "Beam" / "Native" / "control_dir.c"