From db38793cf079654880707af7747dd8f255ffc8f9 Mon Sep 17 00:00:00 2001
From: jsboige <jsboige@gmail.com>
Date: Sat, 26 Sep 2026 21:05:05 +0200
Subject: [PATCH] fix(ci,#14921): lean-axiom partage la cle de cache de
 lean-build -- footprint /2 par lake

Le discriminant -axiom- donnait a proof-integrity sa propre entree de
cache pour le meme .lake, meme hash de lakefile/toolchain : double
empreinte quota (defaut 1) et rebuild froid independant (incident
#9798, exit 143 sur les deux jobs). La cle harmonisee rend le restore
exact-HIT sur la sauvegarde du job ci du MEME run (needs: ci), le
lake -R build du job d'axiomes devient une trace no-op, et les cles
legacy -axiom- n'entrent pas dans le prefixe restore (LRU seul).

Option 1 du residuel mesure au 2026-09-20 (c.5848602768) sur #14921.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
---
 .github/workflows/lean-axiom.yml | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/lean-axiom.yml b/.github/workflows/lean-axiom.yml
index 64f4d9c2ea..2c6c071a11 100644
--- a/.github/workflows/lean-axiom.yml
+++ b/.github/workflows/lean-axiom.yml
@@ -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.
 #
@@ -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.