Skip to content

fix(ci,#14921): lean-axiom partage la cle de cache de lean-build (footprint /2 par lake) #17986

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Sep 27, 2026
Merged

fix(ci,#14921): lean-axiom partage la cle de cache de lean-build (footprint /2 par lake) #17986

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 18 additions & 6 deletions .github/workflows/lean-axiom.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ name: Lean Axiom Check (reusable)
#
# The check is NOT a build run — we assume `lean-build.yml` already ran
# successfully upstream. We just need the lake project cached and the
# toolchain present, so we run the same setup steps. If `lake build`
# toolchain present, so we run the same setup steps — and since #14921
# option 1 the cache key is the SAME as lean-build's, so `needs: ci`
# hands us the ci job's own build artifacts (exact HIT, no rebuild).
# If `lake build`
# fails, the `#print axioms` step will too, and the job will exit 1 with
# the lake error in the logs.
#
Expand Down Expand Up @@ -110,16 +113,25 @@ jobs:
uses: actions/cache@v4
with:
path: ${{ inputs.project-path }}/.lake
key: lake-${{ inputs.display-name }}-axiom-${{ runner.os }}-${{ hashFiles(format('{0}/lakefile.lean', inputs.project-path), format('{0}/lakefile.toml', inputs.project-path), format('{0}/lean-toolchain', inputs.project-path)) }}
restore-keys: lake-${{ inputs.display-name }}-axiom-${{ runner.os }}-
# Key is IDENTICAL to lean-build's (workflows/lean-build.yml l.213 and
# actions/lean-build/action.yml l.141): same path, same hashed file set
# {lakefile.lean|toml, lean-toolchain}. Callers run `needs: ci`, so the
# ci job of the SAME run has already saved this exact key — here it is
# an exact HIT and the `lake -R build` below is a no-op trace, not a
# rebuild. One cache entry per lake instead of two (footprint /2,
# See #14921 option 1). Legacy `-axiom-` keys do not prefix-match the
# new restore-keys, so they expire by LRU without ever being served.
key: lake-${{ inputs.display-name }}-${{ runner.os }}-${{ hashFiles(format('{0}/lakefile.lean', inputs.project-path), format('{0}/lakefile.toml', inputs.project-path), format('{0}/lean-toolchain', inputs.project-path)) }}
restore-keys: lake-${{ inputs.display-name }}-${{ runner.os }}-

- name: Add swap space
# Same OOM guard as lean-build.yml (see the comment there): a cache-miss
# build of a large local module (conway_lean HashlifeCorrectness.lean)
# exceeds the 16 GB of hosted runners and the VM is torn down with exit 143.
# This workflow rebuilds the lake too (its cache key differs from
# lean-build's, so it can miss independently) — observed on PR #9798 where
# BOTH proof-integrity jobs died at exit 143 alongside the build job.
# With the shared key the steady state is a HIT, but the swap stays: on
# cache eviction (or a first run of a new lake) this job still builds
# cold — the observed failure mode of PR #9798, where both jobs died at
# exit 143 with two independently-missed caches.
# 16 G -> 32 G (2026-08-07, PR #9840): teardown recurred with the swap step
# green, and the peak is inside a SINGLE module — see the long note in
# lean-build.yml for the measurements.
Expand Down
Loading