Constat (mesuré en livrant #17336)
L'extension du garde check_lake_matrix_paths.py au critère de RECROISEMENT DE CHEMINS (au lieu du seul nom de fichier lean-<lake>.yml) révèle deux doubles déclencheurs PREEXISTANTS sur main :
| Wrapper |
Lake manifeste |
Chemins partagés (extraits) |
lean-asymmetric-information.yml |
gamedefsext |
MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/**.lean, lakefile.toml |
lean-social-choice.yml |
gametheory |
MyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean, lean-toolchain |
Chaque PR touchant ces chemins construit le lake DEUX FOIS (jambe matricielle + wrapper), et pour les lakes portant un pass B.3, l'axiom check double aussi.
Pourquoi le garde ne les voyait pas
La règle 3 du garde vérifie l'existence de lean-<lake>.yml PAR NOM (gamedefsext → lean-gamedefsext.yml, absent → vert). Le vrai critère d'un double déclencheur est le recroisement des on.paths : un wrapper nommé pour un autre lake mais couvrant les chemins d'un lake manifeste passe entre les gouttes. Le cas fondateur côté nouveau : lean-serre.yml couvrait serre100_lean (nom de fichier ≠ nom du lake) — c'est ce qui a exposé l'angle mort en livrant #17336.
État après la PR #17370
- Le garde gagne le check par recroisement (fail-closed).
- Ces deux paires entrent dans
KNOWN_DOUBLE_TRIGGERS (allowlist documentée citant cette issue) pour ne PAS rougir main avant leur résolution.
Acceptance
See #17336 (grain qui a exposé l'angle mort) · #13751 (garde d'origine)
Constat (mesuré en livrant #17336)
L'extension du garde
check_lake_matrix_paths.pyau critère de RECROISEMENT DE CHEMINS (au lieu du seul nom de fichierlean-<lake>.yml) révèle deux doubles déclencheurs PREEXISTANTS sur main :lean-asymmetric-information.ymlgamedefsextMyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/**.lean,lakefile.tomllean-social-choice.ymlgametheoryMyIA.AI.Notebooks/GameTheory/game_theory_lean/lakefile.lean,lean-toolchainChaque PR touchant ces chemins construit le lake DEUX FOIS (jambe matricielle + wrapper), et pour les lakes portant un pass B.3, l'axiom check double aussi.
Pourquoi le garde ne les voyait pas
La règle 3 du garde vérifie l'existence de
lean-<lake>.ymlPAR NOM (gamedefsext→lean-gamedefsext.yml, absent → vert). Le vrai critère d'un double déclencheur est le recroisement deson.paths: un wrapper nommé pour un autre lake mais couvrant les chemins d'un lake manifeste passe entre les gouttes. Le cas fondateur côté nouveau :lean-serre.ymlcouvraitserre100_lean(nom de fichier ≠ nom du lake) — c'est ce qui a exposé l'angle mort en livrant #17336.État après la PR #17370
KNOWN_DOUBLE_TRIGGERS(allowlist documentée citant cette issue) pour ne PAS rougir main avant leur résolution.Acceptance
on.pathsles chemins du lake manifeste (si le wrapper couvre aussi d'autres lakes non migrés).KNOWN_DOUBLE_TRIGGERS(le garde redevient strict).lean_game_defs_ext/**.leanne déclenche plus qu'UN build du lake.See #17336 (grain qui a exposé l'angle mort) · #13751 (garde d'origine)