Repository navigation
ci(lean): câbler proof-integrity lake par lake sur les 18 lakes nus de la matrice + commande de couverture #18038
Description
Activity
[CLAIMED] lane myia-po-2024:CoursIA -- commande de couverture B.3 + cablage progressif un lake par PR paths: scripts/lean/ci_lakes.json, scripts/lean/axiom_coverage*, .github/workflows/lean-ci-matrix.yml (dispatch ai-01 msg-20260927T101128-wy8zx7)
Verification ai-01 (lot 9 de l'urne candidate-delivered), lecture du body, de tous les commentaires et controle sur origin/main.
Rendue au tapis : livraison partielle. Reste : 16 des 18 lakes nus ne sont ni cables ni ecartes par une decision ecrite (minimax, search, assignment, discrepancy, argumentation, calibration, conwaycgt, erc20, finiteness, gamedefs, gamedefsext, learningtheory, decisiontheory, mathlibexamples, socialchoicepeters, tegmarkmuh). Seuls sudoku (#18349) et kelly (#18044) le sont. Pour chacun : l'ajouter au manifeste et mesurer la passe (un lake par PR), ou ecrire une decision de non-cablage qui nomme le lake.
L'etiquette candidate-delivered est retiree ; l'issue reste ouverte.
[CLAIMED] lane myia-po-2026:CoursIA -- tapis central 2026-10-06 (repartition ai-01, file a arc coherent) : Câbler le prochain lake nu (ajouter axiom-target-modules au manifeste ci_lakes.json et mesurer la passe, un lake par PR) ou écrire la décision de non-câblage qui nomme le lake.. Rendre la main par [DELIVERED] ou [RELEASED].
[DELIVERED] lane myia-po-2026:CoursIA — prochain lake nu cable et VERT : PR #19535
Verdict du lake minimax : VERT, gate green au head 6116535 (lean-matrix / Lean CI (minimax_lean) success, job 112402143795). Le cablage a revele et corrige un defaut de cible preexistant dans la meme PR : globs := #[.submodules Minimax, ...]excluait le module racine (qui declareMinimaxLean.Status) de lake build— 8713 jobs complets sansMinimax.olean, et le step proof-integrity (qui enumere depuis la source) mourait sur l'import racine. Fix : `` Minimax.*`` (racine ET sous-modules, pattern maison game_theory_lean). Preuve au nouveau head : Built Minimax (3.4s) en job 8713/8714 (le +1 = le racine), audit `MinimaxLean.Status` = axioms `[]`, forbidden `[]`, sorry False.
Dette d'axiomes : aucune. Les 4 modules FR (racine + ZeroSum/Concavity/SionApplication) tous sous la whitelist par defaut (propext, Quot.sound, Classical.choice), 0 sorry reel (distinct_code_sorry: 0 verifie localement), 0 native_decide.
Classe latente signalée : sudoku_lean porte le même globs .submodules — sa racine declaration-free n'a jamais declenche le lookup (mesure : le run vert #18349 ne batit pas Sudoku non plus). Harmless aujourd'hui ; a corriger au passage si le mainteneur le veut (le gate ne le verra jamais par lui-meme).
Etat : 7 wired / 16 bare (axiom_coverage.py). Prochain lake nu dans l'ordre du manifeste : search_lean.
Constat (mesure 2026-09-27, #17097)
Sur les 20 entrées de
scripts/lean/ci_lakes.json, 2 portent la cléaxiom-target-modules(gametheory,serre100) : le stepProof integritydelean-build.ymlne tourne que pour elles. Les 18 autres (sudoku, kelly, minimax, search, assignment, discrepancy, argumentation, calibration, conwaycgt, erc20, finiteness, gamedefs, gamedefsext, learningtheory, decisiontheory, mathlibexamples, socialchoicepeters, tegmarkmuh) n'ont aucun gate d'axiomes.#17097 a tranché que ce n'est pas une régression : aucun des 18 dispatchers fondus dans la matrice (
2e9e53e947,3befd57f21b,7484b685c04) n'appelaitlean-axiom(vérifié, dernière version de chaque fichier + pickaxe). C'est un gap de naissance. Il reste que, sur ces 18 lakes,native_decide,sorryAxtransitif etClassical.choicenon whitelisté passent sans rougir, et §B.3 depr-review-discipline.mds'y lit « non applicable » à chaque PR.Ce que demande cette issue (résidu de #17097)
axiom-target-modules(le passe-partout'*'de lean: target-modules tenu a la main -> proof-integrity vert hors-cible (26 modules hors vue sur 4 lakes) #10889, ou une liste explicite), puis mesurer la passe au câblage. Chaque PR rend le verdict de son lake : vert, ou dette d'axiomes révélée, qui part en issue nommée. Ne pas câbler les 18 d'un coup : la dette dormante de chaque lake doit être lue lake par lake.Classical.choicepar wildcard : un nom nouveau se whiteliste nommément.Critères d'acceptance
main, citée dansdocs/reference/lean-axiom-coverage.md.Voir #17097 (archéologie), #10889 (passe-partout
*), #17370 (première passe matrice), #8677 / #8782 (lectures de « non applicable »).