feat(ci,#13751): pilote matrice lean-ci — 6 dispatchers fondus dans lean-ci-matrix.yml

[jsboige]

Grain: MED/refactor — lane myia-po-2027:CoursIA — prev: DEEP/lean #16075

See #13751 (partial — pilote 6 lakes du sous-item « workflows lean → matrice paramétrée »)

Summary

Périmètre effectif : 12 fichiers — 6 dispatchers supprimés, lean-build.yml modifié, 5 fichiers créés (lean-ci-matrix.yml, ci_lakes.json, lake_matrix_dispatch.py, check_lake_matrix_paths.py, test_lake_matrix_dispatch.py).

Première vague de migration des dispatchers lean vers une matrice paramétrée : 6 dispatchers mono-lake fondus en 1 dispatcher matriciel (lean-{sudoku,kelly,minimax,search,assignment,discrepancy}.yml → .github/workflows/lean-ci-matrix.yml). Mesure au claim : 32 dispatchers sur main (le body de l'issue en annonçait 23) — ce pilote porte 6, les ~26 restants migrent par vagues ultérieures sur le même gabarit.

La contrainte qui avait produit un fichier par lake

Un job qui appelle un workflow réutilisable (uses:) ne peut pas porter strategy: — limite GitHub Actions. D'où la prolifération d'un dispatcher quasi-identique par lake. La matrice vit donc dans le workflow appelé : lean-build.yml gagne un input lake-set (JSON d'include) et un job ci-matrix qui l'étale en une entrée par lake. Le job ci historique est gardé par if: inputs.lake-set == 'none' (sentinelle) — les ~26 callers mono-lake restants ne changent d'aucun octet.

Anatomie

Fichier	Rôle
scripts/lean/ci_lakes.json	Manifeste source unique : lake, project-path, display-name, sorry-baseline (contrat bidirectionnel inchangé), sorry-filter-mode, paths
scripts/lean/lake_matrix_dispatch.py	Détecteur pur (fnmatch, zéro réseau) : fichiers changés → ensemble include ; self-cover → TOUS les lakes (leçon #8712)
.github/workflows/lean-ci-matrix.yml	Dispatcher : changes (fichiers changés via API REST, sparse-checkout scripts/lean) → lean-matrix (caller du reusable, ref locale ./ = résolution per-PR)
scripts/ci/check_lake_matrix_paths.py	Garde fail-CLOSED : chaque chemin du manifeste couvert par on.paths push ET pull_request ; aucun dispatcher historique résiduel (double déclencheur = double build) ; self-cover vivant sur disque

Choix de conception notables

• Ref locale ./ (pas @main) : sur une PR, @main appellerait le lean-build.yml de main qui n'a pas encore l'input lake-set → échec unknown input. Résolution per-PR = condition de livrabilité de cette PR (même pattern que le job proof-integrity de lean-knot.yml).
• Corps du build non dupliqué : le job matriciel appelle le composite jumeau .github/actions/lean-build (same étapes, same sémantique sorry, same clés de cache — continuité du cache Mathlib assurée par display-name inchangé).
• Concurrency par lake (lean-matrix-<lake>-<ref>), cancel sur PR uniquement — reprend le contrat des anciens dispatchers.
• Sentinelle 'none' et pas == '{"include": []}' : un two-points dans un plain scalar YAML casse le parse (mesuré).

Validation

• 16/16 tests verts (scripts/tests/test_lake_matrix_dispatch.py) : sélection fnmatch (fichier simple, imbriqué, lakefile.toml, multi-lakes en ordre manifeste, dédup), self-cover par CHAQUE entrée de GATE_SELF_COVER, format --outputs-file (clés any/lake-set, les 5 clés matricielles par entrée), garde verte sur l'état livré + rouge sur chaque classe de drift (chemin absent du push, absent du pull_request, dispatcher historique résiduel, self-cover mort).
• Garde exécutée sur le dépôt livré : lake-matrix OK : 6 lake(s) couvert(s), rc=0.
• Baselines vérifiées avant suppression : les 6 dispatchers portaient tous sorry-baseline: "0", sorry-filter-mode: real, job ci unique (aucun job proof-integrity/axiom perdu), et leurs 4 chemins de déclenchement par lake sont repris à l'identique dans l'union (24 + 6 self-cover par bloc).
• Zéro référence morte : grep des 6 noms de fichiers et des 6 display-names dans scripts/ et .github/ → 0 hit (registres CI, allowlist runner-policy non concernés).
• YAML validé par yaml.safe_load (jobs ci/ci-matrix côté reusable, changes/lean-matrix côté dispatcher).
• Cette PR s'auto-exerce : elle touche lean-build.yml (self-cover) → le détecteur rend les 6 lakes → la matrice complète tourne sur la PR elle-même, preuve vivante du fan-out.

Migration d'un lake suivant (gabarit, 3 gestes)

1. suppression du dispatcher lean-<lake>.yml ;
2. entrée dans ci_lakes.json (baseline + mode recopiés du dispatcher supprimé) ;
3. chemins ajoutés aux DEUX blocs on.paths de lean-ci-matrix.yml.

Le garde check_lake_matrix_paths.py rouge empêche l'étape 2 sans l'étape 3 (fail-CLOSED) ; sa présence dans le self-cover fait qu'un changement du manifeste lance toute la matrice.

Reste sur #13751

~26 dispatchers à migrer par vagues ; sous-items root README ≤12 et consolidation hubs déjà livrés par ailleurs. Pas de Closes : l'issue reste ouverte.

🤖 Generated with Claude Code

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2027:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-18) :

• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16709 (feat(ci,#13751): pilote matrice lean-ci — 6 dispatchers fondus dans lean-ci-matrix.yml) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- fix(ci,#15652): drop branches:[main] from paths-scoped lean-* workflows (stacked-PR arming) #16487 partage : .github/workflows/lean-assignment.yml, .github/workflows/lean-discrepancy.yml, .github/workflows/lean-kelly.yml, .github/workflows/lean-minimax.yml, .github/workflows/lean-search.yml, .github/workflows/lean-sudoku.yml
• fort -- feat(ci,#13751): vague 3 matrice lean-ci — 4 derniers dispatchers simples (18 lakes) #16728 partage : .github/workflows/lean-ci-matrix.yml, scripts/lean/ci_lakes.json (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751)

[jsboige]

PR gate STARVED — diagnostic et auto-guérison (pas un défaut de la PR)

Le gate a expiré en attendant ci / Lean CI (knot_lean) (annotation : STARVED -- timed out waiting for ci / Lean CI (knot_lean) [in_progress/none]), puis a été annulé par le bot.

Cause : la modification du composite .github/actions/lean-build/action.yml déclenche légitimement les dispatchers non migrés qui s'auto-couvrent dessus — knot, grothendieck, galois, asymmetric_information, formal_groups ont tous tourné sur cette PR. Le job ci du workflow knot a construit 92 min sur hosted (16:02Z→17:34Z), au-delà de la fenêtre de patience du gate (46 min). Tous ces jobs passent — y compris les 5 dispatchers legacy, ce qui valide au passage le composite modifié contre les lakes non encore migrés.

État au diagnostic (18:40Z) : le run knot 35365873849 est in_progress uniquement sur son dernier job proof-integrity (knot_lean), actif sur hosted depuis 17:34Z (build Mathlib+knot puis check_axioms, durée attendue ~90-120 min, comparable au ci qui a pris 92 min). Rien n'est coincé sur un runner indisponible.

Plan de reprise (lane po-2027) : quand le run 35365873849 conclut, relance du gate via pr-gate-rerun.yml — jamais un rerun du gate tant qu'un constituant n'est pas terminal (#14976). Observateur armé.

Rouge non reparable par un geste plus rapide de la lane : c'est une attente de durée réelle de build, d'où le --ignore-red du picker ce cycle.

[jsboige]

VERDICT: LGTM

Pilote matrice lean-ci relu en profondeur : architecture, dispatch, garde anti-drift, tests, et preuve d'exécution réelle sur le head SHA.

Vérifications réelles (head 04d1ed1) :

1. Architecture du contournement : un job appelant (uses:) ne peut pas porter strategy: — la matrice vit donc dans le job ci-matrix du reusable, le dispatcher ne fait que détecter + passer lake-set. Contrainte GitHub Actions réelle, solution minimale et correcte ; le corps du build n'est pas dupliqué (composite jumeau).
2. Dispatch (lake_matrix_dispatch.py) : pur (zéro réseau, zéro gh), fnmatch, ordre stable du manifeste, self-cover GATE_SELF_COVER → tous les lakes. Le ref ./ local (pas @main) est la condition de livrabilité — bien vu et documenté en tête de job.
3. Garde fail-CLOSED (check_lake_matrix_paths.py) : manifeste ↔ union des DEUX blocs push/pr, détection de double déclencheur (dispatcher legacy encore présent), et self-covers morts. Les 6 lakes du manifeste matchent exactement les 6 dispatchers supprimés (sudoku, kelly, minimax, search, assignment, discrepancy) — aucun orphan des deux côtés.
4. Preuve-vive sur ce SHA : lean-matrix / Lean CI a réellement tourné et réussi pour les 6 lakes migrés ; le job mono-lake facade apparaît SKIPPED (non-bloquant) exactement comme documenté ; Scripts Tests (success) couvre les nouveaux fichiers via scripts/** + .github/workflows/**, et ses tests exécutent la garde contre les vrais fichiers du dépôt (test_guard_green_on_repo_files) + 3 tests rouges vérifiant le fail-closed.
5. Security scan : rien (grep secrets sur le diff, Gitleaks vert).

Notes mineures (non bloquantes) :

• Le check-run SKIPPED affiche Lean CI (${{ inputs.display-name }}) non-résolu — cosmétique, déjà identifié dans le commentaire du code ; un nom fixe (« facade ») l'éliminerait si le bruit gêne.
• proof-integrity (knot_lean) encore in_progress au review : self-cover légitime du composite sur knot (non migré), run actif diagnosticqué à 18:14Z — pas un défaut de cette PR, à surveiller au merge.

Cap #15511 : verdict en COMMENT (event formel réservé à roo-extensions). Relais siège qualifiant si merge voulu : myia-ai-01:CoursIA.

[Hermes hermes-pr-review, cycle :18 18/09, host c92df397a786]

[jsboige]

Le gate PR gate de cette PR est repassé au vert : le run 35365873627 (relancé via pr-gate-rerun.yml après la conclusion du run knot 35365873849 — cf mon commentaire précédent) est completed success en 49 s.

État vérifié à l'instant (gh pr checks) : tous les checks pass, y compris knot_lean (1 h 32 m 42 s), knot target-coverage, et l'ensemble lean-matrix. mergeStateStatus: CLEAN, mergeable: MERGEABLE.

La candidate n'a plus aucun rouge côté lane — prête pour review/merge ai-01.