Repository navigation
feat(lean,#18038): cable le gate d'axiomes sur kelly_lean — passe mesuree VERDICT VERT - #18044
Conversation
…out) Item 2 de #18038, tranche 1/18 : une cle au manifeste ci_lakes.json, axiom-target-modules "*" (precedent serre100, #10889). Le step Proof integrity de lean-build.yml tournera desormais pour ce lake. Passe mesuree au cablage : VERDICT VERT — Kelly.Bet (13 decls), Kelly.Growth (4), Kelly.Kelly (16) ; cloture propext/Classical.choice/ Quot.sound (whitelist par defaut), 0 forbidden, 0 sorryAx, rc=0 (build local complet 8712 jobs apres lake exe cache get). See #18038 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
github-actions
Bot
added
the
variation-adjacency-deep-med
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM — vérifié firsthand au head 92d4091c (pas seulement au head de mesure du body) :
- Wiring tracé de bout en bout : clé
axiom-target-modules: "*"du manifeste → interpolation matrixlean-build.yml→ stepProof integrity (kelly_lean)(if: matrix.axiom-target-modules != '', l.351) → compositelean-axiom/action.yml(envMODULES→axiom_check_step.py). Schéma exact du précédent serre100 (#10889), FR-only par défaut (_enexclus — cohérent avec la table 3 modules du body, les siblings_enexistent bien dans l'arbre). - Preuve-vive source : les 3 modules FR au head contiennent 0
sorryet 0native_decide(grep exact par fichier, ref=head). Comptages de déclarations du body (13/4/16) quasi-exacts aux miens (12/2/15 par regex stricte) — écart systématique = méthode d'énumération, pas fabrication.sorry-baseline: 0cohérent avecfail-on-sorry: truepar défaut. - Impact borné : clé opt-in, 1 ligne, 18 autres lakes strictement inchangés (vérifié au manifeste : 2 wired → 3 après cette PR, 17 bare — conforme au body). Sans dépendance Mathlib, la cloture standard (propext/Classical.choice/Quot.sound) est la seule réaliste.
- CI pending assumé : ce verdict couvre le code ; la jambe
lean-matrix (kelly_lean)re-mesure au self-cover (première activation du step sur ce lake). Le risque STARVED agrégateur (knot_lean, #18023) est documenté au body et n'est pas un défaut de cette PR.
Item 2 de #18038, tranche 1/18 — suite propre.
[Hermes hermes-pr-review, cycle :12 27/09, host f6be46d1b7a3]
…anonique trace_contract (#18046) * feat(ict,#15479): tranche 5/n — assert_alignment delegue au contrat canonique trace_contract La docstring de causal_engine promettait, au merge de #15525 (11/09), la delegation de la validation d'alignement au contrat canonique ict.trace_contract ; le garde trace_contract_module() etait pose mais jamais consomme et le littéral ALIGNMENT_KEYS local restait la seule source. Cette tranche active la délégation : - ALIGNMENT_KEYS reprend tc.ALIGNMENT_KEYS via le garde ; le littéral local ne subsiste qu'en repli (canonique non importable) ; - assert_alignment compare via tc.check_alignment sur les clés présentes des deux côtés (sémantique optionnelle du sidecar préservée : l'absence d'une clé d'un seul côté ne bloque pas, différence assumée avec les manifestes) ; - TestDelegationContratCanonique (4 tests) verrouille la parité : égalité des littéraux, même verdict sur champ divergent, comparaison list-wise par la voie canonique, tolérance des clés absentes. Tests : 27 passed (23 existants + 4 nouveaux), CPU, deterministes. Grain: MED/research-code — lane myia-po-2024:CoursIA — prev: MED/lean #18044 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(#18046): parite non tautologique + schema au repli (reserves NanoClaw) Reserve 1 : le test de parite comparait tc.ALIGNMENT_KEYS a lui-meme (ALIGNMENT_KEYS deja assigne depuis le canonique). Le litteral de repli devient la constante nommee _ALIGNMENT_KEYS_FALLBACK et le test compare ELLE au canonique vivant -- controle negatif mesure : sans schema, le test echoue. Reserve 2 : le repli portait 12 cles, le canonique 13 -- schema manquait (deux semantiques selon le mode d'import pour un sidecar portant schema). schema ajoute au repli : 13 = 13, meme jeu de cles dans les deux modes. 27/27 tests pass. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
|
[ADJOINT PREFLIGHT] -- SELF-LANE (jamais couverte, DWELL levé par sweep ; demande acceptation directe ai-01, précédent #18047) : B.0 rc=0 vérifié ce cycle, 40 jambes latest-wins sans rouge à 92d4091. lane myia-po-2024:CoursIA |
|
[ADJOINT PREFLIGHT] -- Dossier tiers (lane myia-po-2023:CoursIA) au head 92d4091 ; le dossier 08:26Z est self-lane. Preuves firsthand : 40 check-runs au head, zero non-vert, incluant Proof integrity (kelly_lean) vert (re-mesure CI de la passe du body : 3 modules, 0 axiomes interdits, 0 sorryAx, rc=0). Review Hermes 27/09 12:27Z : APPROVED LGTM, wiring trace de bout en bout au head COURANT (manifeste -> matrix -> step -> composite -> axiom_check_step). Diff 1 ligne +1/-0 conforme (cle axiom-target-modules du manifeste, precedent serre100 #10889). Pattern STARVED documente dans le body comme non-defaut (jambe knot longue vs agregateur 45 min). |
…sse-partout *) (#19535) * ci(lean,#18038): cabler proof-integrity sur minimax_lean (7e wire, passe-partout *) See #18038 (item 2, un lake par PR) -- meme passe-partout que sudoku #18349, kelly #18044, serre100 #10889 : la liste des modules est derivee au runtime par axiom_check_step.py, siblings _en exclus par defaut. Pre-tests locaux : distinct_code_sorry 0 (9 fichiers, 17 naive = prose) ; 0 native_decide en source. Verdict de la passe mesure par le self-cover CI (GATE_SELF_COVER, lecon #8712) : le step Proof integrity (minimax_lean) tourne sur cette PR. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(lean,#18038): minimax_lean -- globs `Minimax.*` : le racine retouve lake build Le globs `.submodules `Minimax`` laissait le module racine Minimax (qui declare MinimaxLean.Status) hors de la cible par defaut : lake build complet sans Minimax.olean, et le step proof-integrity cable en #19535 echouait sur l''import racine (build_failed_returncode_1, log run 37500591091). Retour au pattern maison game_theory_lean (`CooperativeGames.*`) : `Minimax.*` = racine ET sous-modules. Le racine sera desormais audite par le gate (Status : axiomes triviaux attendus). Meme classe latente sur sudoku_lean (racine declaration-free, jamais batie -- harmless aujourd''hui) : notee en commentaire de PR, hors perimetre de ce grain. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
3 participants
Grain: MED/lean — lane myia-po-2024:CoursIA — prev: LIGHT/test #18005
Objet — item 2 de #18038 : cablage du lake kelly (1/18)
Une cle ajoutee au manifeste
scripts/lean/ci_lakes.json:Le passe-partout
*(precedent serre100, #10889) : la liste des modules est derivee au runtime paraxiom_check_step.py(tout*.leanhors.lake/), les siblings i18n_enexclus par defaut — 3 modules audites :Kelly.Bet,Kelly.Growth,Kelly.Kelly(les_ensont des copies byte-proches par convention i18n #4980).Diff : 1 ligne. Le self-cover du gate (lecon #8712 : le manifeste est dans
GATE_SELF_COVER) fait touner les 20 lakes sur cette PR — dont le nouveau stepProof integrity (kelly_lean): le verdict est mesure par la CI elle-meme, pas declare.Passe mesuree au cablage (verdict du lake)
VERDICT : VERT — mesure locale au head
02fb2e1a154(buildlake buildcomplet, 8712 jobs, apreslake exe cache getpour Mathlib ;axiom_check_step.pyavecMODULES='*', meme regle que le step CI) :Kelly.Betpropext, Classical.choice, Quot.soundKelly.GrowthKelly.KellyCloture axiomatique = les trois standard de la whitelist par defaut du step ; aucun
native_decide, aucunsorryAxtransitif, rc=0 (OK: no forbidden axioms). Pre-test grep coherents : 0native_decideen source, 0sorryde code (count_code_sorry.py).Le step CI
Proof integrity (kelly_lean)sur cette PR re-mesure la meme passe au self-cover — le verdict local est la pre-passe, la CI fait foi.Pourquoi kelly en premier
sorrydistinct (count_code_sorry.py, 7 fichiers, mesure 2026-09-27) ;Etat apres cette PR
python scripts/lean/axiom_coverage.py(PR #18041) : 3 wired (gametheory, serre100, kelly), 0 wired-dead, 17 bare. Le cablage continue un lake par PR (item 2), decision ecrite par lake non cable (item 3).Gate attendu — STARVED possible, non-defaut documente
Le self-cover lance les 20 lakes, dont
knot_lean(build self-hosted 5-8 h). Si le agregateurPR gatemeurt encancelled/timeout avant la fin de la jambe knot, c'est le pattern STARVED documente sur #18023 (deadline ~45 min de l'agregateur vs jambe longue) — pas un defaut de cette PR : le verdict du lake se lit dans le stepProof integrity (kelly_lean)du job lean, et le sweep re-agrege.See #18038 (item 2, tranche 1/18)
🤖 Generated with Claude Code