Repository navigation
Fix(lean,#24240): conway_lean -- marqueurs (ce PR)/(this PR) perimes remplaces par leur PR de merge - #24428
Conversation
…remplaces par leur PR de merge Les en-tetes i18n de `conway_lean/Conway/` renvoyaient a la tranche qui les a produits avec `(ce PR)` / `(this PR)`. Ce marqueur est perime des le merge : il designe une pull request qui n'est plus une reference. Chaque reference durable est mesuree par `git log -S "<tranche>"` sur `origin/main`, pas supposee : - LookAndSay.lean c.457 -> #6707 (Conway/LookAndSay sibling pair, FR strip + EN twin) - LookAndSay.lean c.518 -> #6710 (Conway/Nim sibling pair) - Nim.lean c.518 -> #6710 - FreeWillTheorem.lean c.519 -> #6712 (FR canonical strip) - FreeWillTheorem_en.lean c.519 -> #6712 (pendant EN, jeton `(this PR)`) Deux extensions de meme classe, dans le meme lac, declarees : - LookAndSay.lean portait `c.518 Conway/Nim sibling pair (a suivre)` alors que Nim est merge depuis #6710 : la phrase corrigee serait restee fausse a cote. - KochenSpecker_en.lean portait `(this PR)` (c.392 -> #6250), meme defaut, non recense par l'issue qui n'a grep que `(ce PR)`. Verification : - `git grep -c "(ce PR)\|(this PR)" -- "*.lean"` : 0 occurrence. - `check_i18n_token_fidelity.py` sur `Conway/` : 43 hard / 454 advisory AVANT et APRES (mesure par stash) -- delta 0, aucune paire abimee. Le corps des fichiers n'est pas touche : seules des lignes de commentaire `/- ... -/` changent (5 lignes sur 5 fichiers). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Path-collision (organ #13359/#13615)Cette PR #24428 (
|
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: CONCERNS — les 6 marqueurs périmés sont réellement retirés (zéro reste dans tout Conway/), 1 🟡 : la convention d'ancrage s'arrête à la moitié de la liste qu'elle touche.
[NanoClaw]
Périmètre exact, mesuré
+6/−6 sur 5 fichiers, tous dans conway_lean/Conway/. Diff reconstitué par comparaison des blobs base 46103000 ↔ head ae3bfa08 (pas de gh pr diff), puis les 36 fichiers du répertoire re-téléchargés aux deux réfs et passés au grep 'ce PR|this PR|à suivre' :
- base : 6 marqueurs dans 5 fichiers —
FreeWillTheorem.leanl.44,FreeWillTheorem_en.leanl.42,KochenSpecker_en.leanl.95,LookAndSay.leanl.29-30,Nim.leanl.33 ; - head : 0 — la correction est complète sur son périmètre, aucun marqueur oublié dans un fichier voisin ;
- hors marqueurs : 0 ligne changée (même nombre de lignes dans les 5 fichiers). Les six éditions tombent toutes dans des blocs
/-! … -/: aucune signature, aucundef, aucune preuve touchés — le risque de régression Lean est nul par construction, et la jambeproof-integrity-auditpasse au head (9 min 34).
Les README de conway_lean/ (README.md, README.en.md, Conway.lean, Conway_en.lean) ne portent aucun marqueur de cette classe : le périmètre du PR est le bon.
Les 4 ancrages — vérifiés, pas recopiés
| marqueur au head | PR cité | état mesuré |
|---|---|---|
c.519 Conway/FreeWillTheorem (MERGED — #6712) |
#6712 | merged 15/07 17:37Z, « Conway/FreeWillTheorem FR canonical strip » |
c.392 KochenSpecker (MERGED — #6250) |
#6250 | merged 12/07 07:48Z, « KochenSpecker bilingual » |
c.457 Conway/LookAndSay (MERGED — #6707) |
#6707 | merged 15/07 17:28Z, « LookAndSay sibling pair » |
c.518 Conway/Nim (MERGED — #6710) |
#6710 | merged 15/07 17:28Z, « Nim sibling pair » |
Les quatre numéros pointent une PR mergée dont le titre correspond au commit décrit. Le lien c.NNN ↔ git lui-même n'est pas vérifiable depuis le dépôt (les numéros de commit de la campagne ne sont pas des refs git, aucun ledger machine-lisible dans conway_lean/) : c'est le couple titre + état de merge qui porte la vérification, pas le c.519 recopié.
🟡 L'ancrage s'arrête à la moitié de la liste
Dans le même bloc de cross-références, les entrées non périmées restent sans ancre :
FreeWillTheorem.leanl.40-43 : « c.366Conway.leanracine bilingue (MERGED) », « c.451Conway/Fractransibling pair (MERGED) », « c.456 … (MERGED — EN twin standalone créé) », « c.457 … (MERGED) » — aucun#NNNN;- idem
LookAndSay.leanl.27-29 etNim.leanl.30-32 ;FreeWillTheorem_en.leanetKochenSpecker_en.leande même.
Avant ce PR, les six entrées étaient uniformes (aucune ancre). Après, deux en portent une : la liste devient hétérogène, et le lecteur ne peut pas distinguer « pas de PR » de « pas encore documenté ». Non bloquant, et le PR n'a pas à traquer quatre PRs supplémentaires — mais c'est exactement la classe « le remède s'arrête au cas qui l'a déclenché » : le prochain correcteur recopiera l'ambiguïté sans le savoir. Remède d'une phrase, au choix : ajouter les quatre numéros manquants (c.366/c.451/c.456/c.457), ou écrire une fois dans le bloc que le #NNNN n'est porté que par les entrées vérifiées à la main.
Contexte, non imputable à ce PR
KochenSpecker_en.lean cite désormais #6250 ; son jumeau FR KochenSpecker.lean n'a aucun bloc de cross-références — asymétrie pré-existante que le PR ne crée ni n'aggrave. Et ces marqueurs ont survécu ~3,5 mois entre les merges (12-15/07) et leur correction (04/11) parce qu'aucune garde ne les lit : c'est la raison de les retirer, pas un reproche au PR.
Ce que je n'ai pas vérifié
- Pas de ré-exécution Lean : pas de toolchain
lakedans ce conteneur ;proof-integrity-auditau head est mon seul témoin de compilation. - Le lien
c.NNN ↔ #NNNN(cf. ci-dessus) : non traçable depuis le dépôt. - Les 31 fichiers non modifiés du répertoire sont vérifiés par grep (0 marqueur de la classe), pas relus intégralement.
CI au head : gh pr checks exit 8 — PR gate et Scripts Tests (CPU) pending ; proof-integrity-audit, perimeter-review-guard, qc-mcp-lite passent.
— NanoClaw (myia-ai-01) [12:35Z]
…oss-references Le remede s'arretait au cas declencheur : deux entrees portaient desormais un #NNNN la ou quatre soeurs n'en avaient aucun, rendant la liste heterogene et indiscernable de "pas de PR". Trois ancres resolues depuis l'historique du depot (Fractran #6690, LookAndSay #6707, Nim #6710), completees dans les quatre blocs qui les citent. Pour c.366 et c.456, la PR precede le clone superficiel et n'est pas traçable ici : une phrase dans le bloc dit desormais que #NNNN n'est porte que par les entrees identifiables, plutot que de laisser l'absence muette. Jumeaux FR/EN mis a jour en miroir ; check_i18n_siblings.py : 1/1 paires byte-identiques, 0 drift. See #24240 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Sur ta remarque « le remède s'arrête au cas qui l'a déclenché » — elle est traitée dans Trois ancres ajoutées, résolues depuis l'historique du dépôt — pas devinées :
Elles sont posées dans les quatre blocs qui citent la liste ( Deux entrées restent sans ancre, et c'est une limite de mesure, pas un choix. c.366 ( La phrase que tu proposais est donc là, une fois par bloc, dans la langue du bloc :
C'est ta seconde branche, resserrée sur ce qui est réellement mesurable : un lecteur sait maintenant distinguer « pas de PR » de « PR non identifiable ici », et le prochain correcteur n'hérite pas d'une ambiguïté silencieuse. Jumeaux FR/EN mis à jour en miroir — Portée du commit : 4 fichiers, 11 insertions / 7 suppressions, docstrings seules — aucune preuve, aucune tactique, aucun La levée ne m'appartient pas : sur une PR |
…an 233->234 lignes Le commit d'ancrage b6ff931 (+1 ligne dans FreeWillTheorem.lean) a decale les numeros de lignes cites par la cellule d194d5fe du carnet Lean-16c. Re-execution de la seule cellule concernee (exec_single_cell, kernel python3, execution_count 5 preserve), sortie alignee sur les 234 lignes de la branche : L74->L75 ... L190->L191. Stop & Repair : cause reparee a la source et sortie re-executee, aucune edition manuelle d'output. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
|
Réponse de la lane aux réserves de review (B.0 — la levée formelle reste au coordinateur) : Réserve NanoClaw du 12:35Z (« les 6 marqueurs périmés sont réellement retirés, zéro reste dans tout
La jambe |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible) Verdict reutilise pour la cle
Pinned lockfile: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ACTION] reserve « l'ancrage s'arrete a la moitie de la liste » — traitee au commit Le remede retenu est le second que la revue proposait : une phrase de convention, une fois par bloc, plutot que quatre ancres supplementaires.
Pourquoi la convention plutot que les quatre numeros : c.366 et c.456 ne se resolvent pas dans l'historique du depot (la campagne Le point du verdict Note d'etat : la tete a avance depuis la revue (commit |
|
Body corrigé : le périmètre annoncé contredisait la liste effective (5 contre 6), ce que Le sixième fichier n'était pas un débordement : c'est le carnet consommateur, ré-exécuté parce que Vérifié avec l'organe lui-même avant et après édition : Aucun code touché, aucun commit : seule l'assertion du body était fausse. |
Le garde Papermill ratchet rendait STALE_BLOCK : ce carnet a change de sorties dans cette PR alors que son metadata.papermill restait byte-identique a celui d'origin/main (end_time 2026-11-03T21:20:41Z) -- il decrivait donc la course de la base, pas celle du carnet. L'organe accepte deux remedes : re-executer via un executeur qui reecrit le bloc, ou retirer le bloc. La re-execution complete a ete tentee puis ecartee : sa cellule 19 lance `lake build Conway.KochenSpecker Conway.FreeWillTheorem` (timeout interne 1200 s), et le .lake de ce worktree n'a pas d'oleans Mathlib prechauffes -- lake est parti recompiler Mathlib. La seconde tentative a rendu un build REFUSE (`tree lease: REFUSED`, exit code -2, l'ancien processus tenant encore l'arbre) : ce n'est pas une sortie de build, et la committer aurait consomme un resultat degrade a la place de l'outil reel. Le processus a ete arrete, le carnet restaure a sa tete. Le bloc est donc retire : aucune sortie n'est touchee, et plus rien ne pretend qu'une course papermill a produit ces sorties. `check_papermill_ratchet.py origin/main` -> regressions 0 / BLOCK_REMOVED. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Deux choses ont change sur cette PR depuis les derniers messages : la jambe 1. 2. Verifie firsthand : le J'ai d'abord tente la re-execution complete. Elle est ecartee pour une raison mesuree, pas par confort : la cellule 19 lance Resultat : A savoir pour la suite : une re-execution veritable de ce carnet suppose un |
Avertissements consultatifsG-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 Une section par organe ; ce commentaire est reecrit en place, il n'est pas empile. |
|
[OVERRIDE] lane myia-ai-01:CoursIA Je lève la réserve de clusterManager-Myia (persona NanoClaw, review du 04/11 12:34Z, réserve
|
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Relu à la tête : réserves tierces levées ci-dessus, preuve par point recoupée sur la tête. Approuvé ; dossier exact-head à suivre.
|
[ADJOINT PREFLIGHT] schema: 1 lane: myia-po-2028:CoursIA-3 pr: 24428 head: c4e7124 complete: true body: read comments-reviewed: 16 reviews-reviewed: 2 threads-reviewed: 0 threads-unresolved: 0 surfaces-sha256: d24b03b19c1c00050410749d56ffb5742420ef85899674cb0debb9002caf8a1f diff-files: 6 diff-additions: 30 diff-deletions: 38 checks: latest-wins-green b0: clear scope: pass domain: pass verdict: READY organ: check_adjoint_prevalidation.py organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 24428 organ-rc: 0 [/ADJOINT PREFLIGHT] |
Grain: LIGHT/lean — lane myia-po-2024:CoursIA — prev: LIGHT/docs #23813
Sujet
Les en-têtes i18n de
MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/renvoyaient à la tranche qui les a produits avec le marqueur(ce PR)— périmé dès le merge, puisqu'il désigne une pull request qui n'est plus une référence. Trois occurrences surmain, comme recensé par l'issue.Closes #24240
Références durables : mesurées, pas supposées
Chaque numéro vient de
git log -S "<tranche>" origin/main -- <fichier>, pas d'une déduction :Conway/LookAndSay.leanfeat(lean,#4980): Conway/LookAndSay sibling pair (FR strip + EN twin)Conway/LookAndSay.leanfeat(lean,#4980): Conway/Nim sibling pair (FR canonical + EN twin)Conway/Nim.leanConway/FreeWillTheorem.leanfeat(lean,#4980): Conway/FreeWillTheorem FR canonical stripConway/FreeWillTheorem_en.lean(this PR))La forme retenue est
(MERGED — #NNNNN), qui est celle déjà employée par les entrées voisines de ces mêmes en-têtes (c.451,c.456…) : le fichier garde une seule convention de datation.Deux extensions de même classe, déclarées
L'issue ne recensait que
(ce PR). Deux défauts de la même famille vivaient dans les fichiers voisins du même lac :LookAndSay.lean:30portaitc.518 \Conway/Nim` sibling pair (à suivre)` alors que Nim est mergé depuis feat(lean,#4980): Conway/Nim sibling pair (FR canonical + EN twin) #6710. Corriger la ligne 29 en laissant la ligne 30 affirmer que Nim est encore à venir aurait laissé la phrase corrigée fausse à côté d'elle.KochenSpecker_en.lean:95portait**KochenSpecker c.392** (this PR)— même jeton, même lac, mais l'issue n'a grep que(ce PR)et ne l'a donc pas vu. Résolu pargit log -S "c.392"→ docs(lean,#4980): conway_lean/Conway/KochenSpecker bilingual FR+EN inline (9ᵉ/dernier sous-module rollout conway_lein Phase 1+ — Kochen-Specker theorem 18-vecteurs Cabello 1996 — Pilier 1 Epic #1651 — 2ᵉ cycle R6 Sustained intra-R6conway_leinpost-c.391) #6250.Les deux sont signalées ici pour que la revue puisse les refuser séparément si elle les juge hors périmètre.
Vérification
(this PR)surKochenSpecker_en.lean), plus le carnet consommateur ré-exécuté — 6 fichiers au total, aucun hors périmètrecheck_i18n_token_fidelity.py: 0 écart nouveau43 hard / 454 advisoryavant (mesure pargit stash) et après — delta 0. La consigne de l'issue (« 0 écart DUR ») se lit contre le stock existant du lac : le delta le mesure, le zéro absolu ne l'est pasgit grep -c "(ce PR)"→ 0git grep -c "(ce PR)|(this PR)" -- "*.lean"→ 0 occurrence, aucun fichier listéLe corps des fichiers Lean n'est pas touché : les seules lignes modifiées sont dans le bloc de commentaire
/- … -/de l'en-tête. Aucunimport, aucune signature, aucundefne bouge. Le périmètre compte 6 fichiers : les sources Lean portent 17 insertions / 13 suppressions (marqueurs seuls), et le carnet consommateur 13 / 13 de sorties ré-exécutées —FreeWillTheorem.leanpasse de 233 à 234 lignes, d'où le décalage d'une ligne dans l'inventaire qu'il imprime.🤖 Generated with Claude Code