Fix: authenticate lake git clones under concurrent CI runs (#14886)

[jsboige]

Grain: MED/lean — lane myia-po-2027:CoursIA-2 — prev: MED/slides #15049

Closes #14886.

Symptôme

Run 34027638170, PR #14821, knot_lean. Les deux jobs Lean (build + axiom) cold-cache clonent mathlib4 + 8 deps publics en parallèle depuis la même IP de sortie. Sur la fenêtre 10:35:54 → 10:36:18 (~24 s), GitHub répond aux requêtes anonymes par un prompt credentials ; git sans terminal meurt code 128. Quatre échecs mesurés, signature identique :

fatal: could not read Username for 'https://github.com': No such device or address
fatal: the remote end hung up unexpectedly
error: external command 'git' exited with code 128

Le discriminant est l'heure, pas le paquet. LeanSearchClient réussit à 10:34:20 sur le job build et échoue à 10:36:07 sur le job axiom ; Qq et batteries tombent dans la même fenêtre sur le job build. Les trois dépôts sont publics (curl -o /dev/null -w '%{http_code}' .../info/refs?service=git-upload-pack → 200), ce n'est ni une dépendance disparue, ni un passage privé.

Cause (3 mesures)

1. Aucun git config --get-regexp 'url\..*\.insteadof' dans les deux jobs (grep -c extraheader → 0 dans les logs). Les ~9 clones partent en anonyme.
2. lake exe cache get ne couvre que les oleans ; les sources sont clonées de toute façon.
3. Les deux jobs ont des clés de cache distinctes (.github/actions/lean-axiom/action.yml:56). Sur miss, chacun re-clone les 9 deps indépendamment et en parallèle, mathlib4 compris (3 min 30 à 4 min chacun).

Correctif

Une étape Authenticate lake's git clones insérée avant le premier appel lake dans chacun des 4 fichiers :

• .github/workflows/lean-build.yml (réutilisable hosted)
• .github/workflows/lean-axiom.yml (réutilisable hosted)
• .github/actions/lean-build/action.yml (composite self-hosted)
• .github/actions/lean-axiom/action.yml (composite self-hosted)

L'étape pose l'insteadOf avec le job token GHA :

git config --global url."https://x-access-token:${{ github.token }}@github.com/".insteadOf "https://github.com/"
git config --get-regexp '^url\..*\.insteadof$' | sed -E 's#://[^@/]+@#://***@#g'

• Le token reste dans le store de secrets GHA (jamais commité, jamais loggé).
• La seconde ligne sed masque tout ://user:pass@ → ://***@ avant d'écho, donc le token n'atteint pas stdout.

Acceptance (cf #14886 §Acceptance)

1. git config --get-regexp rend une ligne insteadOf dans chaque job (affichée redacted dans le log). Vérifiable par inspection de run.
2. Contrôle positif : un run de knot_lean avec les caches des deux jobs vidés (la condition qui a produit l'échec) — les 18 clones aboutissent, zéro code 128. Un run qui tape le cache ne prouve rien : il ne clone pas.
3. Aucun jeton en clair dans le log ni dans l'arbre. Vérifié par git grep -E "(secrets\.|TOKEN|ghp_)" .github/ → vide.

Diff

.github/actions/lean-axiom/action.yml | 12 ++++++++++++
.github/actions/lean-build/action.yml | 12 ++++++++++++
.github/workflows/lean-axiom.yml      | 12 ++++++++++++
.github/workflows/lean-build.yml      | 12 ++++++++++++
4 files changed, 48 insertions(+)

Strict minimum, isolé à 4 fichiers (les 2 workflows réutilisables + les 2 composite actions qui les twinnent pour le pool self-hosted Lean #14337 tranche 2a).

Pré-requis pour le merge

• Le contrôle positif Genetic sharp playground #2 (cache vidé sur les deux jobs) demande une exécution CI : c'est ce que le run sur la PR donnera.
• Si un run séparé est nécessaire (workflow_dispatch + paramètre cache-disabled: true), le demander ; sinon le run mergé sur la PR suffit.

Notes

• Ne ferme pas le second axe de [Lean][CI] Clones lake anonymes : GitHub exige une identite sous rafale, le paquet qui tombe est aleatoire #14886 (mutualiser les 9 deps entre les deux jobs, périmètre [EPIC] Lean — harmoniser Mathlib, mutualiser les checkouts, regrouper les lakes (anti-proliferation) #4362). Cette PR traite uniquement l'authentification, qui est la cause immédiate et suffisante.
• Le sorry gate de knot_lean reste à baseline (10/10) — l'échec n'a jamais touché la logique de preuve, seulement le clone des deps.

[jsboige]

Fermeture — doublon strict de PR #15025 (et non redélivrance intentionnelle).

Cette PR fait la même chose, sur les mêmes 4 fichiers, avec le même mécanisme insteadOf, que PR #15025 ouverte antérieurement par la même lane (myia-po-2027:CoursIA-2) à 2026-09-07T11:20:26Z (SHA ded6a1ec49f1, branche feature/14886-lean-clone-auth). Le claim [CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: ... que j'avais posé sur #14886 le 2026-09-07T11:18:19Z avait conduit à la rédaction de PR #15025 avant compaction. La compaction de session a effacé la trace ; je n'ai pas vérifié l'existence de #15025 via gh pr list --search "14886" (L1356, L898 — leçon notée).

PR #15025 couvre déjà l'acceptance #14886 :

• 39/40 checks SUCCESS (1 CANCELLED sur PR gate, rollup reroll en attente)
• mergeable: MERGEABLE
• Review Hermes COMMENTED (comment only, pas CHANGES_REQUESTED)
• Périmètre identique : 4 fichiers CI Lean, step Authenticate lake's git clones avec ${{ github.token }} masqué en log par sed

Décision : fermer #15148 sans merger. La branche feature/14886-lake-clones-auth reste supprimable après merge de #15025.

Action vers ai-01 : si PR #15025 reste BLOQUÉE sur le PR gate, un simple re-run du check rollup suffit — l'acceptance #2 (cache vidé sur les deux jobs, 18 clones aboutissent, zéro code 128) sera obtenue sur le run mergé.

Leçon MEMORY à noter : compaction efface les claims récents ; check_lane_claim.py N seul ne suffit pas — un gh pr list --search "head:<branche>" + gh pr list --state all --search "<N>" AVANT tout gh pr create est nécessaire pour détecter un doublon de PR déjà livrée par la même lane.

[github-actions]

prev: genre mots-clé fermant -- bloquant (#10093).

prev: reference(s) fail invariant(s) (prev-not-merged -> [15049]) -> point prev: at a MERGED PR of the same lane, distinct from the current PR. See #13475.

Une prev: dont le genre est fix/close/resolve (ou une inflexion) fait que GitHub interprète <genre> #N comme un ordre de fermeture automatique dès que le texte atterrit dans un message de commit -- c'est exactement ce qui a fermé #10067 (sans la merger) au squash-merge de #10063. Les 14 genres canoniques ne contiennent AUCUN mot-clé fermant : utilisez refactor, guard, ou tooling à la place.

Pour passer ce gate, réécrivez le champ prev: (dans le body ET dans chaque commit concerné) avec un genre non-fermant :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<refactor|guard|tooling|...> #<PR>