diff --git a/.github/actions/lean-ci-setup/action.yml b/.github/actions/lean-ci-setup/action.yml index 1627b831..b470811e 100644 --- a/.github/actions/lean-ci-setup/action.yml +++ b/.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') }}- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 029f0503..c6c45617 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index a66c81af..51dde5fb 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md index 4fab4f28..c4775feb 100644 --- a/docs/DEVELOPMENT.md +++ b/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` diff --git a/lakefile.lean b/lakefile.lean index 58235290..c513b879 100644 --- a/lakefile.lean +++ b/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"