Skip to content

fix(ci,#19658): les caches lake ne s'ecrivent plus sur les refs de PR (8 copies de la meme cle -> 1 sur main) #19668

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 4 commits into from
Oct 10, 2026
Merged

fix(ci,#19658): les caches lake ne s'ecrivent plus sur les refs de PR (8 copies de la meme cle -> 1 sur main) #19668

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e7c4f25
fix(ci,#19658): les caches lake ne s'ecrivent plus sur les refs de PR
jsboige Oct 7, 2026
1fe02d4
fix(ci,#19658): declarer actions/cache/restore et /save dans l'amorca…
jsboige Oct 7, 2026
7e4f5b0
fix(ci,#19668): cache matriciel -- la cle de sauvegarde passe par une…
jsboige Oct 9, 2026
8760eba
Merge branch 'main' into fix/19658-lake-cache-main-only
jsboige Oct 9, 2026
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
30 changes: 28 additions & 2 deletions .github/actions/lean-build/action.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,25 @@ inputs:
required: false
default: ''

outputs:
lake-cache-hit:
description: >
'true' quand l'archive `.lake` a ete restauree depuis le cache Actions.
La restauration seule vit dans le composite (#19658) ; le SAVE est un pas
explicite du job appelant, apres son `Drop Mathlib oleans` -- un post-step
interne au composite capturerait les oleans Mathlib (2,4 Go).
value: ${{ steps.lake-cache.outputs.cache-hit }}
lake-cache-key:
description: >
Cle primaire du cache d'archives `.lake`, telle que calculee par la
restauration du composite. Exposee pour que le SAVE d'un job appelant qui
ne porte PAS lui-meme d'etape `id: lake-cache` (le job matriciel
`ci-matrix`, #13751) puisse nommer la cle : y ecrire directement
`steps.lake-cache.outputs.cache-primary-key` rend la chaine vide, puisque
l'id n'existe que dans le job `ci` et dans ce composite (revue ai-01 sur
#19668).
value: ${{ steps.lake-cache.outputs.cache-primary-key }}

runs:
using: composite
steps:
Expand Down Expand Up @@ -134,8 +153,15 @@ runs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH

- name: Cache Lake build artifacts
uses: actions/cache@v4
# RESTORE SEUL (restore-only, #19658) : le SAVE est un pas explicite du job
# appelant, place APRES son etape `Drop Mathlib oleans` et conditionne a
# `github.ref == refs/heads/main`. Avant, `actions/cache@v4` sauvegardait en
# post-step sur TOUTE ref qui manquait la cle : mesure du 2026-10-07, la
# famille `lake-*` comptait 8 entrees de ~650 Mo, 8/8 sur `refs/pull/*`
# et 0 sur `main` -- la meme cle dupliquee par PR, 5,2 Go du quota de 10 Go.
- name: Restore Lake build artifacts
id: lake-cache
uses: actions/cache/restore@v4
with:
path: ${{ inputs.project-path }}/.lake
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)) }}
Expand Down
21 changes: 17 additions & 4 deletions .github/workflows/lean-axiom.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,18 +128,21 @@ jobs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH

- name: Cache Lake build artifacts
uses: actions/cache@v4
- name: Restore Lake build artifacts
id: lake-cache
uses: actions/cache/restore@v4
with:
path: ${{ inputs.project-path }}/.lake
# 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
# Key is IDENTICAL to lean-build's (workflows/lean-build.yml and
# actions/lean-build/action.yml, etape `Restore Lake build artifacts`): 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.
# RESTORE SEUL (#19658) : le SAVE appartient au job `ci` du meme run
# (et, hors run, a `main` seul) -- cette jambe ne fait que consommer.
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 }}-

Expand Down Expand Up @@ -301,3 +304,13 @@ jobs:
run: |
rm -rf .lake/packages/mathlib/.lake/build
du -sh .lake 2>/dev/null || true

# SAVE EXPLICITE, main only (#19658). Les refs de PR restaurent mais
# n'ecrivent plus : une PR qui manque la cle repart du cache de main via
# `restore-keys` (prefixe), au lieu d'ajouter sa propre copie de ~650 Mo.
- name: Save Lake build artifacts (main only)
if: github.ref == 'refs/heads/main' && steps.lake-cache.outputs.cache-hit != 'true'
uses: actions/cache/save@v4
with:
path: ${{ inputs.project-path }}/.lake
key: ${{ steps.lake-cache.outputs.cache-primary-key }}
34 changes: 32 additions & 2 deletions .github/workflows/lean-build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,8 +206,15 @@ jobs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> $GITHUB_PATH

- name: Cache Lake build artifacts
uses: actions/cache@v4
# RESTORE SEUL (restore-only, #19658) : le SAVE est un pas explicite du job,
# place APRES son etape `Drop Mathlib oleans` et conditionne a
# `github.ref == refs/heads/main`. Avant, `actions/cache@v4` sauvegardait en
# post-step sur TOUTE ref qui manquait la cle : mesure du 2026-10-07, la
# famille `lake-*` comptait 8 entrees de ~650 Mo, 8/8 sur `refs/pull/*` et
# 0 sur `main` -- la meme cle dupliquee par PR, 5,2 Go du quota de 10 Go.
- name: Restore Lake build artifacts
id: lake-cache
uses: actions/cache/restore@v4
with:
path: ${{ inputs.project-path }}/.lake
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)) }}
Expand Down Expand Up @@ -321,6 +328,17 @@ jobs:
rm -rf .lake/packages/mathlib/.lake/build
du -sh .lake 2>/dev/null || true

# SAVE EXPLICITE, main only (#19658). Les refs de PR restaurent mais
# n'ecrivent plus : une PR qui manque la cle repart du cache de main via
# `restore-keys` (prefixe), au lieu d'ajouter sa propre copie de ~650 Mo.
# Place APRES `Drop Mathlib oleans` : c'est l'etat allege qui doit partir.
- name: Save Lake build artifacts (main only)
if: github.ref == 'refs/heads/main' && steps.lake-cache.outputs.cache-hit != 'true'
uses: actions/cache/save@v4
with:
path: ${{ inputs.project-path }}/.lake
key: ${{ steps.lake-cache.outputs.cache-primary-key }}

# Mode matrice #13751 : fan-out par lake, pilote par lean-ci-matrix.yml.
# Un job appelant (`uses:`) ne peut PAS porter `strategy:` (limite GitHub
# Actions) -- c'est la contrainte qui a produit les 32 dispatchers un
Expand Down Expand Up @@ -350,6 +368,7 @@ jobs:
steps:
- uses: actions/checkout@v4
- name: Build + sorry gate (${{ matrix.display-name }})
id: build
uses: ./.github/actions/lean-build
with:
project-path: ${{ matrix.project-path }}
Expand Down Expand Up @@ -411,3 +430,14 @@ jobs:
run: |
rm -rf .lake/packages/mathlib/.lake/build
du -sh .lake 2>/dev/null || true

# SAVE EXPLICITE, main only (#19658). Les refs de PR restaurent mais
# n'ecrivent plus : une PR qui manque la cle repart du cache de main via
# `restore-keys` (prefixe), au lieu d'ajouter sa propre copie de ~650 Mo.
# Place APRES `Drop Mathlib oleans` : c'est l'etat allege qui doit partir.
- name: Save Lake build artifacts (main only)
if: github.ref == 'refs/heads/main' && steps.build.outputs.lake-cache-hit != 'true'
uses: actions/cache/save@v4
with:
path: ${{ matrix.project-path }}/.lake
key: ${{ steps.build.outputs.lake-cache-key }}
7 changes: 7 additions & 0 deletions scripts/ci/docker/linux-runner/seed_action_cache.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,13 @@
# (`jsboige/CoursIA/.github/workflows/*@main`).
ACTIONS = (
"actions/cache@v4",
# #19658 : la bascule restore/save scinde l'action en deux sous-chemins.
# Le depot cache est le meme (`parse_uses` s'arrete a `actions/cache`),
# mais le scanner de `test_action_cache_seed_guard.py` compare les formes
# `uses:` brutes : les deux sous-chemins doivent donc etre declares, comme
# les trois `github/codeql-action/*` ci-dessous.
"actions/cache/restore@v4",
"actions/cache/save@v4",
"actions/checkout@v4",
"actions/deploy-pages@v4",
"actions/github-script@v7",
Expand Down
4 changes: 3 additions & 1 deletion scripts/tests/test_action_cache_seed_guard.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,9 @@
la compte ;
- **la meme action sous un sous-chemin** : `github/codeql-action/init@v4` et
`.../analyze@v4` sont deux entrees `uses:` mais **un seul** depot a cacher.
Le compte brut (13 entrees) n'est pas le compte des archives (11 depots).
Le compte brut (15 entrees) n'est pas le compte des archives (11 depots).
Meme forme depuis #19658 : `actions/cache/restore@v4` et
`actions/cache/save@v4` partagent l'archive de `actions/cache`.
"""

import os
Expand Down
Loading
Loading