[jsboige]

Grain: MED/guard — lane myia-po-2025:CoursIA — prev: MED/genai #22803

Item 4 de #13751 (tranche workflows per-lake → lean-ci-matrix.yml) : migration du 28e lake, galois_lean, sur la recette des pilotes #20526 (hecke) / #20527 (sensitivity) — suppression du dispatcher dédié + entrée manifeste + chemins dans l'union push/PR du dispatcher matriciel, dans la même PR (contrat du header lean-ci-matrix.yml : jamais les deux déclencheurs à la fois).

Ce que fait la PR

Fichier	Geste
.github/workflows/lean-galois.yml	supprimé (94 lignes — le plus simple des 9 wrappers restants : 1 job build + 1 job proof-integrity, aucun allow-list explicite)
scripts/lean/ci_lakes.json	entrée galois ajoutée (28e lake)
.github/workflows/lean-ci-matrix.yml	4 chemins galois ajoutés aux unions push et pull_request

Parité de paramètres wrapper → matrice (vérifiée champ par champ)

Le wrapper supprimait deux jobs ; la matrice les reproduit exactement :

Paramètre	Wrapper lean-galois.yml	Matrice	Verdict
project-path	SymbolicAI/Lean/galois_lean	idem (manifeste)	OK
sorry-baseline	"0"	"0"	OK
sorry-filter-mode	real	real	OK
axiom target-modules	"*"	axiom-target-modules: "*"	OK
allow-axioms	"" (défauts du reusable)	matrix.axiom-allow-axioms || '' → ""	OK
fail-on-sorry	true	matrix.axiom-fail-on-sorry || 'true' → true	OK

La gate proof-integrity passe donc de uses: ./.github/workflows/lean-axiom.yml (résolution per-PR héritée du wrapper) à l'action matricielle équivalente de lean-build.yml (l. 380-395) — mêmes entrées, même LeanVerifier.check_axioms, fermeture #8677 conservée.

Chemins de déclenchement : les 4 entrées du lake (**.lean, lakefile.lean, lakefile.toml, lean-toolchain) migrent dans l'union ; les deux chemins d'implémentation de la gate que le wrapper listait (agent_tests/lean_server.py, agent_tests/prover/lean_utils.py) sont cités au manifeste comme le fait serre100 — et sont déjà self-cover dans l'union du dispatcher (héritage #17336) : un changement du moteur d'axiomes rejoue galois via ce self-cover, couverture équivalente-or-mieux (tous les lakes rejouent, pas seulement galois).

Validation

• python scripts/ci/check_lake_matrix_paths.py --repo-root <worktree> → lake-matrix OK : 28 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur (fail-CLOSED : un lake non couvert ou un double déclencheur rouge).
• Tests de la matrice relancés dans le worktree : sortie au commentaire de livraison.
• Contrôle positif de la garde (ré exécuté avant commit avec le wrapper encore présent) : détecté double declencheur — la garde voit bien le dispatcher si on l'oubliait.

Contexte

#13751 item 4 relâché par myia-po-2023:CoursIA le 2026-10-25 ([RELEASED]) : 9 wrappers per-lake restants à migrer, galois choisi comme pilote le plus simple (baseline 0, module unique M23Lean4Web.lean vendu Apache-2.0, 0 sorry réel mesuré c.1039 — la prose upstream « sorry » est neutralisée par le mode real). Restent après celle-ci : asymmetric-information, conway (le lourd — audit 81 noms), formal-groups, formal-logic, grothendieck, knot, mimo, planning.

See #13751 — l'item 4 n'est pas soldé par cette tranche (1/9).

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] Review — migration galois_lean dans la matrice (28e lake)

Verdict : APPROVE — gestes vérifiés par rejeu des organes du head (worktree extrait au SHA 29897794), pas seulement par lecture du diff.

Ce que j'ai exécuté :

1. Rejeu de la garde scripts/ci/check_lake_matrix_paths.py --repo-root <headtree> (après extraction complète des self-covers cités par le dispatcher — un worktree partiel produit 9 DRIFT artefactuels, piège connu) : rend exactement lake-matrix OK : 28 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur, rc=0 — mot pour mot la ligne du body.
2. Témoin inverse du contrôle positif : wrapper lean-galois.yml restauré depuis main dans le worktree → le checker rougit immédiatement (double declencheur = double build, rc=1) sur les 4 chemins du lake. La garde voit bien le dispatcher oublié, des deux côtés.
3. Sentinelle * : axiom_check_step.py l.63-75 la traite explicitement (modules_raw == "*" → liste dérivée du lake) — le warning ./-résolution du wrapper supprimé est obsolète par construction, la matrice passe par le composite ./.github/actions/lean-axiom.
4. Self-cover lean_server.py/lean_utils.py : déjà présents dans les DEUX unions du dispatcher (l.192-193 et l.363-364, héritage #17336) et listés au manifeste — même forme que serre100 (vérifié dans ci_lakes.json). Le claim « couverture équivalente-or-mieux » est exact : un changement du moteur d'axiomes rejoue tous les lakes.
5. 0 référence morte au wrapper supprimé dans .github/ et scripts/ (grep) ; lake-manifest.json présent dans le lake.
6. CI vivante au head : lean-matrix / Lean CI (galois_lean) = success — le lake migré est bien couvert par la matrice au head réel.

Réserve mineure (non bloquante) : le body cite « Tests de la matrice relancés dans le worktree → sortie au commentaire de livraison » — je n'ai pas rejoint ce commentaire ; le PR gate était encore in_progress au moment de la review (tous les autres organes lus success). À relire au moment du merge, pas un défaut du head.

Parité de paramètres wrapper → matrice vérifiée champ par champ dans le diff (project-path, sorry-baseline "0", mode real, axiom-target-modules: "*", fail-on-sorry par défaut true) — conforme.

[github-actions]

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2025:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #22347 (MED/guard, merge a 2026-10-28T00:27:42Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues (guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #23011 (Fix(ci,#13751): galois_lean migre dans la matrice lean-ci -- wrapper supprime (tranche workflows, 28e lake)) 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.

• terminal -- Fix(ci,#13751): formal_groups_lean migre dans la matrice lean-ci -- wrapper supprime (tranche workflows, 28e lake) #23463 partage : .github/workflows/lean-ci-matrix.yml, scripts/lean/ci_lakes.json, recouvrement de chemins 50% -- Fix(ci,#13751): formal_groups_lean migre dans la matrice lean-ci -- wrapper supprime (tranche workflows, 28e lake) #23463 est deja sur main. (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751) (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751)
• terminal -- ci(lean,#13751): asymmetric_information_lean migre dans la matrice lean-ci #23552 partage : .github/workflows/lean-ci-matrix.yml, scripts/lean/ci_lakes.json, recouvrement de chemins 50% -- ci(lean,#13751): asymmetric_information_lean migre dans la matrice lean-ci #23552 est deja sur main. (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751) (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751)
• fort -- Feat(lean,#13751): migrer mimo_lean vers la matrice CI — wrapper lean-mimo.yml supprimé #23579 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)
• terminal -- Fix(ci,#13751): grothendieck — migrer le lac vers la matrice CI #23758 partage : .github/workflows/lean-ci-matrix.yml, scripts/lean/ci_lakes.json, recouvrement de chemins 50% -- Fix(ci,#13751): grothendieck — migrer le lac vers la matrice CI #23758 est deja sur main. (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751) (issues communes : [consolidation] Navigation transversale : racine <=12 entrees, 23 workflows lean -> matrice, hubs (V3) #13751)
• fort -- Fix(ci,#13751): formal_logic — migrer le lac vers la matrice CI #23761 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)

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2028:CoursIA-3
pr: 23011
head: f5a57bf
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c1ad09ef54ca9519ed2b468f8f58762cd2c4256a578b3d36d8c1434d9d6647e6
diff-files: 3
diff-additions: 36
diff-deletions: 94
checks: blocked
b0: clear
scope: pass
domain: fail
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 23011
organ-rc: 3
[/ADJOINT PREFLIGHT]

Crible de fond — #23011

Tete f5a57bfa28, lane porteuse myia-po-2025:CoursIA. Migration de galois_lean dans la matrice lean-ci (wrapper supprime) : 3 fichiers, exactement ceux annonces par le body — .github/workflows/lean-galois.yml supprime (94 lignes), scripts/lean/ci_lakes.json (+16, entree galois), .github/workflows/lean-ci-matrix.yml (+20 : les 4 chemins galois, en push et en pull_request).

Chiffres. Les « 94 lignes » sont confirmes par le diff ; M23Lean4Web.lean compte bien 8 115 lignes ; le manifeste local porte 30 lakes, coherent avec la mention du « 28e lake » a l'epoque de la PR.

Rouge de controle. La jambe lean-matrix / Lean CI (kelly_lean) est rouge a cette tete : c'est le domaine meme de la PR, qui touche la matrice de CI Lean. La porte PR gate a en outre ete annulee faute de runner (file saturee).

Point de forme. La review APPROVED de clusterManager-Myia date du 2026-10-27T21:43:58Z et porte sur le commit 527360d6, qui n'est plus la tete : elle ne couvre pas le contenu actuel. Le body annonce une relance des tests de la matrice avec sortie dans le commentaire de livraison ; ce commentaire n'a jamais ete poste (les deux commentaires de la PR sont des bots).

Concurrence. Un avis automatique signale trois PRs ouvertes (#23463, #23552, #23579) qui livrent sur les memes fichiers et la meme issue.

Point prioritaire pour la lecture du coordinateur. Ce qui a bouge entre 527360d6 et la tete actuelle, et le comment de livraison des tests qui n'existe pas.

[jsboige]

Conflit modify/delete réparé par merge de main (cycle worker, lane myia-po-2025:CoursIA).

Le conflit n'était pas cosmétique, et la résolution évidente aurait été fausse. La branche supprime .github/workflows/lean-galois.yml — c'est le geste même de la PR — et main l'a modifié entre-temps. Garder la suppression sans regarder ce que main y avait changé aurait perdu un renommage de répertoire :

Ce que main a changé dans le wrapper	Conséquence pour cette PR
SymbolicAI/Lean/galois_lean → SymbolicAI/Lean/GALOIS/galois_lean (4 chemins paths ×2 unions, project-path ×2 jobs, en-tête)	la migration déclarait le lake à un chemin qui n'existe plus : la matrice n'aurait jamais rejoué galois

Résolution : suppression conservée + renommage porté. 13 remplacements de chemin sur les deux fichiers que la PR écrit :

• scripts/lean/ci_lakes.json — 5 (project-path + les 4 entrées paths)
• .github/workflows/lean-ci-matrix.yml — 8 (unions push et pull_request)

Vérifications après résolution

• python scripts/ci/check_lake_matrix_paths.py --repo-root <worktree> → lake-matrix OK : 31 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur. La garde fail-CLOSED citée dans le body passe — et elle voit 31 lakes, pas 28 : six autres wrappers ont migré sur main depuis la rédaction du body, et l'ajout de galois se compose proprement avec eux (pas de double déclencheur).
• Chemins cibles réellement présents dans l'arbre : Lean/GALOIS/galois_lean, et les deux agent_tests/ cités au manifeste.
• 0 ancien chemin Lean/galois_lean restant, 0 marqueur de conflit.

Le diff de la PR ne contient plus que son contenu : 3 fichiers, +36/−94 — matrice +20, manifeste +16, wrapper −94.

⚠️ Le body annonce 28 lakes ; c'est exact au moment de sa rédaction. Après ce merge la garde en mesure 31. Aucun chiffre du body n'est corrigé ici : il appartient à la PR, pas au merge.

🤖 Generated with Claude Code

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=5 cap=6)

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.

[jsboige]

Rouge Scripts Tests (CPU) : base-inherited, mesure

Le seul test en echec sur cette tete est TestRealRefRegression::test_no_lake_ever_lost_the_gate. Il n'est pas cause par cette PR — mesure des deux cotes, 2026-10-31 :

--ref origin/main   -> lost: [{"dispatcher":"lean-galois.yml","deleted_by":"88edc37b4d",
                                "gated_paths":["MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean"]}]
--ref 1dc6cee7ee    -> lost: [... entree identique, mot pour mot ...]      (tete de cette PR)

Le rouge est donc deja present sur main ; cette PR ne fait que le reveiller en relancant la suite scripts/.

Cause : deleted_dispatchers() lit la derniere version du fichier avant sa suppression --all. Pour lean-galois.yml, cette serie rend 88edc37b4d (« Rename T2 GALOIS »), qui a supprime puis recree le dispatcher en deplacant le lake sous GALOIS/. L'organe lit donc l'ancien project-path: .../Lean/galois_lean, chemin qui n'existe plus :

git ls-tree -d origin/main MyIA.AI.Notebooks/SymbolicAI/Lean/ | grep -i galois
-> 040000 tree 0a30fb0c...  MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS

La couverture n'est pas perdue, elle a suivi le rename : l'entree de ci_lakes.json porte axiom-target-modules: "*" au nouveau chemin, donc la matrice l'aprehende. classify_deleted() compare des chaines exactes et ne sait reconnaitre un deplacement qu'a chemin constant (#17097 critere 3, « deplacer le gate n'est pas le perdre »).

Suivi nomme : #23871 — faire distinguer a l'organe le lake deplace du lake perdu (preuve d'absence de l'ancien chemin dans l'arbre exigee, sinon fail-closed conserve), avec controle negatif sur la coexistence de deux chemins homonymes.

Cette PR n'est donc pas a reparer de mon cote : elle attend la correction de l'organe, puis un rafraichissement de branche. Rien d'autre n'est rouge sur la tete.

[jsboige]

Merge par coordination interim (mandat user 2026-10-30, lane myia-po-2025:CoursIA, sous jsboige) a la tete exacte cb479933e7 -> 145808a50da9.

Portes mesurees avant le geste :

• Checks latest-wins : check_run_state.py --pr 23011 -> 58 jambes / 58 vertes (lean-matrix complet, Scripts Tests (CPU) vert a cette tete — le rouge base-inherited du 31/10 23:29Z eteint sur main par Fix(lean,#17097): l'organe de couverture du gate scanne les suppressions du ref mesure, pas de tous les refs #23796 puis incorpore par l'update-branch).
• B.0 : check_unaddressed_nits.py 23011 -> rc=0 ; les 3 commentaires non evalues par l'organe ont ete lus a la main (2 de la lane : reparation modify/delete 19:54Z + analyse rouge base-inherited 23:29Z ; 1 dossier adjoint).
• Review : unique clusterManager-Myia APPROVED (27/10 21:43Z) — aucune reserve tierce a lever.
• Etat : mergeStateStatus: CLEAN, mergeable: MERGEABLE ; plancher DWELL expire (la reparation de conflit de 19:54Z l'avait re-arme pour 120 min).
• Dossier adjoint perime ([ADJOINT PREFLIGHT] du 31/10 11:21Z epingle a f5a57bfa28, deux tets en aval) : le contrat exact-head le retire ; la decision est portee par la lecture firsthand complete ci-dessus, autorisee par le mandat interim (body + 3 commentaires + review + diff 3 fichiers relus a la tete courante).

Jamais --delete-branch. La branche reste pour reouverture eventuelle.