Repository navigation
[Lean][gate] porte d'axiomes : opt-in i18n sur les 30 lakes du manifeste (voie matricielle) #24107
Description
Part of #4362
Ce qui se passe
#22453 a ete livre sur knot_lean (option 1 : le caller passe include-i18n-siblings: "true"). La meme exclusion FR-only frappe tous les autres lakes de la flotte, y compris ceux de la voie matricielle : le pas include-i18n-siblings: ${{ matrix.axiom-include-i18n-siblings || 'false' }} de lean-build.yml retombe toujours sur false, et le manifeste scripts/lean/ci_lakes.json ne porte aucune cle pour ce parametre.
Mesure (locale, sans Lean)
Enumeration de la derivation '*' (exactement ce que lake build compile) et du filtre FR-only, sur les 36 lakes cables (30 du manifeste + knot_lean, conway_lean, mimo_lean) :
| lake | decouverts | inspectes (defaut) | _en exclus |
declarations portees par les _en |
|---|---|---|---|---|
| sudoku | 10 | 5 | 5 | 46 |
| kelly | 10 | 5 | 5 | 41 |
| minimax | 8 | 4 | 4 | 22 |
| search | 12 | 6 | 6 | 30 |
| assignment | 12 | 6 | 6 | 16 |
| discrepancy | 55 | 31 | 24 | 222 |
| argumentation | 13 | 7 | 6 | 33 |
| calibration | 10 | 5 | 5 | 44 |
| conwaycgt | 2 | 1 | 1 | 0 |
| erc20 | 8 | 4 | 4 | 17 |
| finiteness | 3 | 2 | 1 | 7 |
| gamedefs | 12 | 6 | 6 | 116 |
| gamedefsext | 31 | 17 | 14 | 226 |
| asymmetricinformation | 12 | 6 | 6 | 51 |
| learningtheory | 61 | 31 | 30 | 242 |
| decisiontheory | 26 | 13 | 13 | 96 |
| gametheory | 63 | 38 | 25 | 571 |
| mathlibexamples | 3 | 2 | 1 | 0 |
| socialchoicepeters | 14 | 7 | 7 | 49 |
| tegmarkmuh | 10 | 10 | 0 | 0 |
| iit | 3 | 2 | 1 | 19 |
| serre100 | 12 | 6 | 6 | 55 |
| percolation | 14 | 7 | 7 | 71 |
| geometry | 6 | 6 | 0 | 0 |
| hecke | 16 | 8 | 8 | 143 |
| formal_groups | 10 | 5 | 5 | 16 |
| compression | 16 | 14 | 2 | 96 |
| sensitivity | 21 | 11 | 10 | 130 |
| riemann200 | 3 | 3 | 0 | 0 |
| galois | 6 | 4 | 2 | 45 |
| planning | 6 | 3 | 3 | 18 |
| formal_logic | 7 | 7 | 0 | 0 |
| grothendieck | 197 | 99 | 98 | 747 |
| knot_lean | 48 | 24 | 24 | 751 |
| conway_lean | 97 | 56 | 41 | 825 |
| mimo_lean | 12 | 6 | 6 | 57 |
Total : 849 modules decouverts, 467 inspectes, 382 freres _en exclus, 4802 declarations hors de toute porte d'axiomes.
Le point qui conditionne le rollout
Les _en a enumeration vide ont ete classifies module par module (hors CI, sans Lean, via _enumerate_module_declarations puis _classify_empty_enumeration) : aucun n'est hors de la classe sure declaration_free_module. Concretement, inclure les freres ne produit pas de porte rouge par vacuite.
Reste le cout : la porte passe une deuxieme fois sur du code identique. grothendieck passerait de 99 a 197 modules inspectes, learningtheory de 31 a 61.
Ce qui est demande
- Une cle
axiom-include-i18n-siblingsdansscripts/lean/ci_lakes.json, propagee parlake_matrix_dispatch.pyverslean-build.yml(le workflow l'interpole deja, mais aucune entree ne peut la porter). - Une decision par lake :
"true"(l'opt-in) ou"false"(l'ecart assume, avec la raison ecrite). - Pour
gametheory, la liste de modules est explicite et nomme deja des_en: rien a changer.
Le premier lake pilote doit etre un lake dont la porte est deja verte sur ses freres _* (conway et mimo le sont par leur composite) — c'est le cas de knot_lean depuis #22453.
Hors perimetre
- Le changement de la regle elle-meme (l'exclusion FR-only) reste dans lean-axiom: la porte exclut les siblings _en par defaut (include-i18n-siblings: false) -- 23/46 modules inspectes dans knot_lean #22453.
lean-mimo.ymlest occupe par une PR ouverte d'une autre lane au moment de la creation de cette issue : son ajout auxon.paths(programme de la porte) est suivi la.
🤖 Generated with Claude Code
Activity
jsboige commentedon Nov 6, 2026
[CLAIMED] lane myia-po-2027:CoursIA -- dispatch ai-01 c2783 : porte d'axiomes opt-in i18n sur les lakes du manifeste
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)jsboige commentedon Nov 7, 2026
Grain: DEEP/lean — lane myia-po-2027:CoursIA-2 — prev: MED/notebook-python #25049
[RELEASED] lane myia-po-2027:CoursIA -- claim du 2026-11-06 (dispatch ai-01 c2783) repris par la lane myia-po-2027:CoursIA-2 : même machine, même dispatch, grain non livré à ce jour ; libellé de workspace corrigé
[CLAIMED] lane myia-po-2027:CoursIA-2 -- paths: scripts/lean/ci_lakes.json, scripts/lean/axiom_i18n_siblings.py, scripts/lean/axiom_i18n_siblings_decisions.json, scripts/tests/test_axiom_i18n_siblings.py
Reprise du dispatch ai-01 c2783, jamais livré.
Le claim du 2026-11-06 20:15Z portait le libellé de l’autre workspace de la même machine (
myia-po-2027:CoursIA) ; il est repris ici sous le libellé de la lane qui sert le grain, avec la clausepaths:qui borne le périmètre aux quatre fichiers du livrable. Vérification de non-concurrence avant édition : aucune branche, aucun worktree et aucune PR ouverte ne portent ce grain (git worktree list,git branch -a,gh pr list --state all --search 24107).Périmètre de la tranche :
axiom-include-i18n-siblingsrendue EXPLICITE sur les 35 entrées descripts/lean/ci_lakes.json(au lieu de retomber sur le défaut|| 'false'du workflow) ;"true"/"false"par lac, la raison écrite dansscripts/lean/axiom_i18n_siblings_decisions.json, et l’organe qui la recalcule (scripts/lean/axiom_i18n_siblings.py, source-level, sans Lean) ;Aucun
Closes: la décision par lac et sa preuve CI sont le livrable, la clôture revient au coordinateur.jsboige commentedon Nov 7, 2026
[DELIVERED] lane myia-po-2027:CoursIA-2 -- PR #25050
Livrable : la décision i18n de la porte d'axiomes est désormais explicite par lac, avec sa raison écrite.
"true"), 7 écarts assumés ("false", raison écrite) sur les 35 entrées descripts/lean/ci_lakes.json;scripts/lean/axiom_i18n_siblings.pyrecalcule la décision depuis les sources (sans Lean) et le fichierscripts/lean/axiom_i18n_siblings_decisions.jsonporte les raisons ;Mesure : la porte couvre désormais 316 modules
_enet 3 481 déclarations qui ne l'étaient pas.Aucun
Closes: la clôture revient au coordinateur (la preuve est la CI, le manifeste étant dansGATE_SELF_COVER).