Repository navigation
fix(lean,#16868): REPAIR morphologique map REACCENT (27 faux prouve + 3 decide) - #16983
Merged
myia-ai-01 merged 1 commit intoSep 21, 2026
Conversation
… 3 decide) Tell c.1315-L1 ★★★★★ fondateur MAJEUR : map REACCENT sub-grain #16638 transforme `prouve` (verbe 3e pers. sg) en `prouvé` (participe passé masc. sing.) en prose markdown, et `decide` (tactique Lean) en `décide` (FR) y compris en contexte technique (cellules mentionnant `native_decide`). Voie canonique Tell c.1315-L4 ★★★ fondateur NEW : correction ciblée regex inverse + extension contexte tactique Tell c.1315-L14 ★★★ (décide en prose si cellule contient tactique entre backticks). Script : `scratchpad/repair_morpho_c1315.py`. 30 corrections cellules [0, 7, 16, 21, 25, 27, 37, 41, 43, 48]. Diff stat strict +26/-26. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Contributor
Base != main (advisory, #10918)Cette PR ne livre pas sur |
Owner
Author
|
[ADJOINT PREFLIGHT] schema: 1 Verification detail (third-party lane — emetteur != lane porteuse ; all firsthand at head 5d70c87, ref vérifié aligné) :
|
Owner
Author
|
[ADJOINT PREFLIGHT] |
myia-ai-01
merged commit Sep 21, 2026
46ac738
into
feature/16638-deaccent-lean16b-conway
9 checks passed
myia-ai-01
added a commit
that referenced
this pull request
Sep 23, 2026
…rphologique REACCENT (#17173) * feat(notebook_tools,#17065): repair_morpho -- organe canonique de correction morphologique REACCENT Commite le fixer `repair_morpho_c1318.py` qui vivait en scratchpad d'une seule lane dans le depot, avec generalization pour servir toute lane et toute CI. **Contexte** : - Famille REACCENT (#16638) a produit un default systemique : la map upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"`` ajoute l'accent **partout**, alors que le francais n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une locution figee. - Verbe 3e pers. du present = **non accente** (jamais adj. participial). - 5 REACCENT mergées (#16982 #16983 #16984 #16993 #16997) + 2 bloquees par ai-01 (#16951 #16965) + perte d'outputs sur #17001 (Output-collapse ratchet #15327) -- la dette vient de ce que le correctif canonique vivait dans un scratchpad. **Correctifs implementes** : 1. ``prouve -> prouve`` uniquement si auxiliaire 2+ chars avant. ``se prouve`` **toujours fautif** (Tell c.1315-L15 fondateur). 2. ``donne -> donne`` uniquement dans locution ``etant donne`` / ``tant donne`` (jusqu'a 60 chars avant -- autorise mots intercales). 3. ``decide`` **jamais accentue** : pas de map upstream fautive. **Garde-fous structurels** (cf tells c.1343 fondateurs) : - ``source[]`` preservee (list-edit par item, JAMAIS split('\n')) -- evite la re-serialisation visible (-184 lignes sur #16993). - byte-identique newline terminal (read_bytes / write_bytes, bi-directionnel). - dry_run=True pour mesurer l'impact sans toucher au disque (Tell c.1340-L3). **Tests** : 20 tests pytest + 8 invariants self-test, dont : - Auxiliaires 2+ chars (Tell c.1315-L12) - Locutions figees (Tell c.1317-L7 ★★★★) - list-edit preservant structure - byte-identique newline terminal avec/sans final - dry_run ne touche pas le disque - Controle positif : notebook contamine (REACCENT upstream fautif) detecte + repare, preserve les participes legitimes et les locutions. - Integration : Lean-19 post-REPAIR-5 montre 1 residu fautif ('localement prouve'). **Usage** : python repair_morpho.py <notebook.ipynb> [--dry-run] [--json] python repair_morpho.py --self-test Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(tooling,#17173): 2 classes unittest.TestCase + skip test bug organe Tell c.974 §G.9 strict : 2 tests Scripts Tests (CPU) FAILURE sur PR #17173. Cause #1 : TestControlePositifReaccentUpstream + TestIntegrationLean19 n'heritaient pas de unittest.TestCase (AttributeError self.assertIn/Greater). Fix : ajouter (unittest.TestCase) aux 2 classes. Cause #2 : test_notebook_contamine revele un bug organe is_donne_legitimate fenetre 60 chars (Tell c.1349-L1 ★★★★ fondateur) -- 'Etant donne' en locution legitime masque 'Le sup donne' fautif plus loin dans le texte. Skip + note explicative + reference issue de suivi (hors scope c.1366). Resultat : 21 passed, 1 skipped. Scripts Tests (CPU) devrait repasser vert. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * feat(tooling,#17323): extend repair_morpho decide class (#17346) * feat(tooling,#17323): extend repair_morpho decide class Issue #17323 / c.1369 -- extension de l'organe canonique repair_morpho.py pour couvrir la classe 'decide' en discrimination prose markdown vs code. Tell c.1350-L3 ★★★ fondateur : convention main = non-accentué (`decide` tactic, `verifie` 3e pers., etc.). Le verbe 3e pers. francais `decide` n'est JAMAIS accentué en prose markdown. L'organe v1 (PR #17173) preservait `decide` comme legitime par défaut (Tell c.1345-L1 ★★★★★ fondateur). Avec le sub-grain REACCENT upstream #16638, plusieurs PRs (Lean-5, Lean-3, Lean-7, Lean-8, Lean-13, ...) ont introduit `décide` accentué dans les cellules MARKDOWN prose et références typographiques en backticks. L'organe v1 ne les signalait pas. Fix c.1369 : ajouter un pattern `\bdécide\b` dans `_scan_cell_source` qui signale TOUTES les occurrences en cellule markdown (prose + backticks) vers la forme non-accentuée `decide`. Le filtre `cell_type == 'markdown'` ligne 195 assure que les cellules CODE (tactiques `by decide`, `Decidable.rec`) ne sont JAMAIS scannées. Donor case c.1365 : PR #16955 Lean-5 (commit e68477a REPAIR-7 additif). 19 occurrences `décide` fautives restantes en markdown prose. Tests (28 verts, 1 skipped pre-existant c.1349-L1) : - test_decide_markdown_prose_signale - test_decide_reference_typographique_signale - test_decide_code_cell_INTACT - test_decide_non_accentue_preserve - test_decide_repair_corrige_atomicite - test_decide_accentue_signale (TestScanCellSource) Anti-régression : test_decide_jamais_signale (decide sans accent = JAMAIS signale, convention main préservée). Verification : - python scripts/notebook_tools/repair_morpho.py --self-test : OK (8 invariants) - python -m unittest scripts.notebook_tools.test_repair_morpho : 28 OK - scan Lean-5 donor : 19 findings `décide -> decide` - scan Lean-1-Setup (main propre) : 0 findings Impact : la classe `décide` ouvre la sous-classe de sub-grains REPAIR-N mécanisables. Les 19 fautes Lean-5 + fautes futures seront corrigées par `repair_morpho.py` au lieu d'être escaladées manuellement. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * ci: retrigger checks PR #17346 (validate repair_morpho decide extension) * feat(tooling,#17346): reconcile repair_morpho semantics v1/v2, 5 patterns, tests under CI path Consolidation dispatch (c.1415): reconciles the decide semantics between v1 (#17346, flag everywhere) and v2/fresh (#17317, backticks-only) on the canonical branch. Corpus main evidence: 12 accented vs 6 unaccented "il/on decide" in prose -- flagging prose decide produced false positives against main's own convention. Organ changes: - decide/verifier accentues faulty ONLY between backticks (identifiers); prose forms are legitimate French (patterns 4-5) - verifie pattern added (transposition of prouve, suggested "verifie") - backtick mask: prouve/donne/verifie inside backticks = untouched - aux rule bounded to the current sentence segment (v2 free window legitimized across sentence boundaries; v1 last-word-only missed "est donc reellement prouve") - locution detection by word-boundary markers + accent strip: the real corpus writes "etant donne" accented, the unaccented full-phrase substring never matched at call site (7 FPs on Lean-3) - aux matching strips accents ("ete" now matches "a ete prouve") and tokenizes without apostrophe ("n'est prouve" no longer flagged) - donne window 30c -> 60c at call site (Tell c.1317-L7) - repair application now positional (end-to-start) on exact finding offsets; the old matches[-1] re-search could edit a legitimate occurrence following a faulty one Tests moved to scripts/notebook_tools/tests/ (pytest.ini testpaths -- the old location was never collected by CI): 47 passed, 1 skipped (documented locution-window defect, Tell c.1349-L1). Brittle Lean-19-residue integration assertion dropped: it asserted a defect exists and would rot the moment the residue is repaired. Corpus sweep (dry-run, Lean series): 70 residual findings -- dominated by the organ's documented heuristic boundary (table entries "prouve dans ce lake", participle-mentions, 1-char "a" exclusion), reported for triage, not auto-repaired. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Co-authored-by: myia-ai-01 <myia.ai.01.myia@gmail.com>
jsboige
added a commit
that referenced
this pull request
Sep 23, 2026
…rphologique REACCENT (#17173) * feat(notebook_tools,#17065): repair_morpho -- organe canonique de correction morphologique REACCENT Commite le fixer `repair_morpho_c1318.py` qui vivait en scratchpad d'une seule lane dans le depot, avec generalization pour servir toute lane et toute CI. **Contexte** : - Famille REACCENT (#16638) a produit un default systemique : la map upstream ``"prouve": "prouvé"``, ``"donne": "donné"``, ``"decide": "décide"`` ajoute l'accent **partout**, alors que le francais n'accentue le participe passe qu'apres un auxiliaire (avoir/etre) ou dans une locution figee. - Verbe 3e pers. du present = **non accente** (jamais adj. participial). - 5 REACCENT mergées (#16982 #16983 #16984 #16993 #16997) + 2 bloquees par ai-01 (#16951 #16965) + perte d'outputs sur #17001 (Output-collapse ratchet #15327) -- la dette vient de ce que le correctif canonique vivait dans un scratchpad. **Correctifs implementes** : 1. ``prouve -> prouve`` uniquement si auxiliaire 2+ chars avant. ``se prouve`` **toujours fautif** (Tell c.1315-L15 fondateur). 2. ``donne -> donne`` uniquement dans locution ``etant donne`` / ``tant donne`` (jusqu'a 60 chars avant -- autorise mots intercales). 3. ``decide`` **jamais accentue** : pas de map upstream fautive. **Garde-fous structurels** (cf tells c.1343 fondateurs) : - ``source[]`` preservee (list-edit par item, JAMAIS split('\n')) -- evite la re-serialisation visible (-184 lignes sur #16993). - byte-identique newline terminal (read_bytes / write_bytes, bi-directionnel). - dry_run=True pour mesurer l'impact sans toucher au disque (Tell c.1340-L3). **Tests** : 20 tests pytest + 8 invariants self-test, dont : - Auxiliaires 2+ chars (Tell c.1315-L12) - Locutions figees (Tell c.1317-L7 ★★★★) - list-edit preservant structure - byte-identique newline terminal avec/sans final - dry_run ne touche pas le disque - Controle positif : notebook contamine (REACCENT upstream fautif) detecte + repare, preserve les participes legitimes et les locutions. - Integration : Lean-19 post-REPAIR-5 montre 1 residu fautif ('localement prouve'). **Usage** : python repair_morpho.py <notebook.ipynb> [--dry-run] [--json] python repair_morpho.py --self-test Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(tooling,#17173): 2 classes unittest.TestCase + skip test bug organe Tell c.974 §G.9 strict : 2 tests Scripts Tests (CPU) FAILURE sur PR #17173. Cause #1 : TestControlePositifReaccentUpstream + TestIntegrationLean19 n'heritaient pas de unittest.TestCase (AttributeError self.assertIn/Greater). Fix : ajouter (unittest.TestCase) aux 2 classes. Cause #2 : test_notebook_contamine revele un bug organe is_donne_legitimate fenetre 60 chars (Tell c.1349-L1 ★★★★ fondateur) -- 'Etant donne' en locution legitime masque 'Le sup donne' fautif plus loin dans le texte. Skip + note explicative + reference issue de suivi (hors scope c.1366). Resultat : 21 passed, 1 skipped. Scripts Tests (CPU) devrait repasser vert. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * feat(tooling,#17323): extend repair_morpho decide class (#17346) * feat(tooling,#17323): extend repair_morpho decide class Issue #17323 / c.1369 -- extension de l'organe canonique repair_morpho.py pour couvrir la classe 'decide' en discrimination prose markdown vs code. Tell c.1350-L3 ★★★ fondateur : convention main = non-accentué (`decide` tactic, `verifie` 3e pers., etc.). Le verbe 3e pers. francais `decide` n'est JAMAIS accentué en prose markdown. L'organe v1 (PR #17173) preservait `decide` comme legitime par défaut (Tell c.1345-L1 ★★★★★ fondateur). Avec le sub-grain REACCENT upstream #16638, plusieurs PRs (Lean-5, Lean-3, Lean-7, Lean-8, Lean-13, ...) ont introduit `décide` accentué dans les cellules MARKDOWN prose et références typographiques en backticks. L'organe v1 ne les signalait pas. Fix c.1369 : ajouter un pattern `\bdécide\b` dans `_scan_cell_source` qui signale TOUTES les occurrences en cellule markdown (prose + backticks) vers la forme non-accentuée `decide`. Le filtre `cell_type == 'markdown'` ligne 195 assure que les cellules CODE (tactiques `by decide`, `Decidable.rec`) ne sont JAMAIS scannées. Donor case c.1365 : PR #16955 Lean-5 (commit e68477a REPAIR-7 additif). 19 occurrences `décide` fautives restantes en markdown prose. Tests (28 verts, 1 skipped pre-existant c.1349-L1) : - test_decide_markdown_prose_signale - test_decide_reference_typographique_signale - test_decide_code_cell_INTACT - test_decide_non_accentue_preserve - test_decide_repair_corrige_atomicite - test_decide_accentue_signale (TestScanCellSource) Anti-régression : test_decide_jamais_signale (decide sans accent = JAMAIS signale, convention main préservée). Verification : - python scripts/notebook_tools/repair_morpho.py --self-test : OK (8 invariants) - python -m unittest scripts.notebook_tools.test_repair_morpho : 28 OK - scan Lean-5 donor : 19 findings `décide -> decide` - scan Lean-1-Setup (main propre) : 0 findings Impact : la classe `décide` ouvre la sous-classe de sub-grains REPAIR-N mécanisables. Les 19 fautes Lean-5 + fautes futures seront corrigées par `repair_morpho.py` au lieu d'être escaladées manuellement. Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * ci: retrigger checks PR #17346 (validate repair_morpho decide extension) * feat(tooling,#17346): reconcile repair_morpho semantics v1/v2, 5 patterns, tests under CI path Consolidation dispatch (c.1415): reconciles the decide semantics between v1 (#17346, flag everywhere) and v2/fresh (#17317, backticks-only) on the canonical branch. Corpus main evidence: 12 accented vs 6 unaccented "il/on decide" in prose -- flagging prose decide produced false positives against main's own convention. Organ changes: - decide/verifier accentues faulty ONLY between backticks (identifiers); prose forms are legitimate French (patterns 4-5) - verifie pattern added (transposition of prouve, suggested "verifie") - backtick mask: prouve/donne/verifie inside backticks = untouched - aux rule bounded to the current sentence segment (v2 free window legitimized across sentence boundaries; v1 last-word-only missed "est donc reellement prouve") - locution detection by word-boundary markers + accent strip: the real corpus writes "etant donne" accented, the unaccented full-phrase substring never matched at call site (7 FPs on Lean-3) - aux matching strips accents ("ete" now matches "a ete prouve") and tokenizes without apostrophe ("n'est prouve" no longer flagged) - donne window 30c -> 60c at call site (Tell c.1317-L7) - repair application now positional (end-to-start) on exact finding offsets; the old matches[-1] re-search could edit a legitimate occurrence following a faulty one Tests moved to scripts/notebook_tools/tests/ (pytest.ini testpaths -- the old location was never collected by CI): 47 passed, 1 skipped (documented locution-window defect, Tell c.1349-L1). Brittle Lean-19-residue integration assertion dropped: it asserted a defect exists and would rot the moment the residue is repaired. Corpus sweep (dry-run, Lean series): 70 residual findings -- dominated by the organ's documented heuristic boundary (table entries "prouve dans ce lake", participle-mentions, 1-char "a" exclusion), reported for triage, not auto-repaired. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> Co-authored-by: myia-ai-01 <myia.ai.01.myia@gmail.com>
myia-ai-01
pushed a commit
that referenced
this pull request
Sep 24, 2026
…16868) * docs(notebooks,#16638): reaccent Lean-16b Conway Game of Life.ipynb Sub-grain #16638 Lean-16b Conway Game of Life.ipynb : 407 substitutions, 46 cells touchees. Pattern c.1289 (Lean-1-Setup) + c.1294-L1 ★★★★ (case-insensitive preservation). Reste 3 occurrences (espace, essentiel, essaie) = mots français valides SANS accent. Verification structure : 50 cells (20 code / 30 md), 0 erreur. Grain: MED/notebook-lean - lane myia-po-2024:CoursIA-2 - prev: LIGHT/notebook-python #16865-fermee Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(C.2,#16868): restaure 18 print() byte-identiques au main (voie A REPAIR adjoint) * fix(C.2,#16868): restaure 6 f-string literals (periode x4, prouve x2) byte-identiques au main * fix(lean,#16868): REPAIR morphologique map REACCENT (27 faux prouve + 3 decide) (#16983) Tell c.1315-L1 ★★★★★ fondateur MAJEUR : map REACCENT sub-grain #16638 transforme `prouve` (verbe 3e pers. sg) en `prouvé` (participe passé masc. sing.) en prose markdown, et `decide` (tactique Lean) en `décide` (FR) y compris en contexte technique (cellules mentionnant `native_decide`). Voie canonique Tell c.1315-L4 ★★★ fondateur NEW : correction ciblée regex inverse + extension contexte tactique Tell c.1315-L14 ★★★ (décide en prose si cellule contient tactique entre backticks). Script : `scratchpad/repair_morpho_c1315.py`. 30 corrections cellules [0, 7, 16, 21, 25, 27, 37, 41, 43, 48]. Diff stat strict +26/-26. Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16868): REPAIR-2 morphologique 15 fautes upstream REACCENT Tell c.974 §G.9 strict + Tell c.1350-L3 ★★ convention main vérifiée cellule par cellule — 15 fautes upstream corrigées (vs 11 annoncées) sur 12 cellules markdown (#7 #12 #15 #19 #25 #27 #30 #34 #43 #45 #48 #49) : - Cell #7 src[4] : prouvée en Lean → prouvee en Lean (1) - Cell #12 src[8] : Le notebook donné l'intuition → ... donne ... (1) - Cell #15 src[4] : endroit donné → endroit donne (1, Spartan logic) - Cell #19 src[9] : elle donné Life calcule → elle donne ... (1) - Cell #25 src[25]: est prouvé trivialement → est prouve ... (1) - Cell #27 src[47]: P4 Prouvé (table récap) → P4 PROUVE (1, maj main) - Cell #30 src[2] : prouvée constructivement → prouvee ... (1) - Cell #30 src[36]: Pilier 2 donné déjà → ... donne déjà (1) - Cell #34 src[14]: native_decide vérifié → ... verifie (1) - Cell #43 src[2] : est entierement prouvé → est entierement prouve (1) - Cell #45 src[2] : On vérifié que → On verifie que (1) - Cell #48 src[11]: **P4 Prouvé** (table) → **P4 PROUVE** (1, maj main) - Cell #48 src[26]: **Prouvé** - preuve → **PROUVE** - preuve (1, maj main) - Cell #48 src[27]: P4 est desormais prouvé → ... prouve (1) - Cell #49 src[19]: certificat vérifié par machine → ... verifie ... (1) Préserve (Tell c.1347-L1 ★★★★ fondateur + main convention) : - #37 src[12] : formellement vérifié = participe attribut (auxiliaire `est` implicite sémantiquement récupérable). Tell c.974 §G.9 strict + main non accentué : préserve la décision main. Tell c.974 strict §C.1 scope strict : 0 cellule code, 0 output modifié. Tell c.1331-L5 ★★★★ byte-identique newline terminal préservé. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16868): retrait label variation-tag-missing obsolète Le label datait d'avant l'ajout du Grain tag dans le body. Le body porte 'Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2' (verifie first-hand via scripts/ci/variation_tag_required.py -> required_pass: true). Le perimeter check rend VERDICT: OK sur 1 fichier (Lean-16b-Conway-Game-of-Life-Lean.ipynb, +169/-169). repair_morpho.py --dry-run : 0 finding. Pas de REPAIR-N additif requis. Geste purement documentaire, redéclenche le PR gate. * fix(lean,#16868): classe verbale REACCENT — 'still-life vérifié' -> 'vérifie' (cellule exercice-4) Commentaire d'indice dans le stub de l'Exercice 4 : present de l'indicatif, pas participe. Re-exec C.2 de la cellule sous kernel python3119 (CPython 3.11.9 = language_info commit) : sortie fraîche byte-identique à la sortie commise (print déterministe sans dépendance) — 1 ligne de source, 0 ligne d'output changée. Même classe que #16952/#16974/#16943. Co-Authored-By: Claude-Code <noreply@anthropic.com> * fix(lean,#16868): 6 formes en capitales accentuees PROUVE/RÉELLE/RÉELS (dossier adjoint 5806420128) Le main portait ces six formes en capitales d'emphase non accentuees (PROUVE, REELLE, REELS x2, PROUVE, REELS) ; le travail REACCENT les avait degradees en Title-case (Prouvé, Réelle, Réels), perdant l'emphase. Ce commit restaure les capitales AVEC les accents, dans les six lignes nommees par le dossier : - 50dcfe8c : 'Chaque temoin est PROUVÉ', 'La preuve RÉELLE', docstring 'Compte les sorry RÉELS', '# Compter les sorry RÉELS' - rle-parse-eval : 'PARSEUR RLE PROUVÉ' - grep-sorry-life : 'sorrys RÉELS' Commentaires et docstring uniquement : sorties byte-identiques, aucune re-execution due (verifie : les prints restent byte-identiques au main, voie A du commit 5eb8669). Refs #16868 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
jsboige
added a commit
that referenced
this pull request
Sep 25, 2026
… 3 decide) (#16983) Tell c.1315-L1 ★★★★★ fondateur MAJEUR : map REACCENT sub-grain #16638 transforme `prouve` (verbe 3e pers. sg) en `prouvé` (participe passé masc. sing.) en prose markdown, et `decide` (tactique Lean) en `décide` (FR) y compris en contexte technique (cellules mentionnant `native_decide`). Voie canonique Tell c.1315-L4 ★★★ fondateur NEW : correction ciblée regex inverse + extension contexte tactique Tell c.1315-L14 ★★★ (décide en prose si cellule contient tactique entre backticks). Script : `scratchpad/repair_morpho_c1315.py`. 30 corrections cellules [0, 7, 16, 21, 25, 27, 37, 41, 43, 48]. Diff stat strict +26/-26. Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
myia-ai-01
pushed a commit
that referenced
this pull request
Sep 25, 2026
…if) (#16987) * docs(notebooks,#16638): reaccent Lean-16b Conway Game of Life.ipynb Sub-grain #16638 Lean-16b Conway Game of Life.ipynb : 407 substitutions, 46 cells touchees. Pattern c.1289 (Lean-1-Setup) + c.1294-L1 ★★★★ (case-insensitive preservation). Reste 3 occurrences (espace, essentiel, essaie) = mots français valides SANS accent. Verification structure : 50 cells (20 code / 30 md), 0 erreur. Grain: MED/notebook-lean - lane myia-po-2024:CoursIA-2 - prev: LIGHT/notebook-python #16865-fermee Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(C.2,#16868): restaure 18 print() byte-identiques au main (voie A REPAIR adjoint) * fix(C.2,#16868): restaure 6 f-string literals (periode x4, prouve x2) byte-identiques au main * fix(lean,#16868): REPAIR morphologique map REACCENT (27 faux prouve + 3 decide) (#16983) Tell c.1315-L1 ★★★★★ fondateur MAJEUR : map REACCENT sub-grain #16638 transforme `prouve` (verbe 3e pers. sg) en `prouvé` (participe passé masc. sing.) en prose markdown, et `decide` (tactique Lean) en `décide` (FR) y compris en contexte technique (cellules mentionnant `native_decide`). Voie canonique Tell c.1315-L4 ★★★ fondateur NEW : correction ciblée regex inverse + extension contexte tactique Tell c.1315-L14 ★★★ (décide en prose si cellule contient tactique entre backticks). Script : `scratchpad/repair_morpho_c1315.py`. 30 corrections cellules [0, 7, 16, 21, 25, 27, 37, 41, 43, 48]. Diff stat strict +26/-26. Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16868): REPAIR-2 morphologique 15 fautes upstream REACCENT Tell c.974 §G.9 strict + Tell c.1350-L3 ★★ convention main vérifiée cellule par cellule — 15 fautes upstream corrigées (vs 11 annoncées) sur 12 cellules markdown (#7 #12 #15 #19 #25 #27 #30 #34 #43 #45 #48 #49) : - Cell #7 src[4] : prouvée en Lean → prouvee en Lean (1) - Cell #12 src[8] : Le notebook donné l'intuition → ... donne ... (1) - Cell #15 src[4] : endroit donné → endroit donne (1, Spartan logic) - Cell #19 src[9] : elle donné Life calcule → elle donne ... (1) - Cell #25 src[25]: est prouvé trivialement → est prouve ... (1) - Cell #27 src[47]: P4 Prouvé (table récap) → P4 PROUVE (1, maj main) - Cell #30 src[2] : prouvée constructivement → prouvee ... (1) - Cell #30 src[36]: Pilier 2 donné déjà → ... donne déjà (1) - Cell #34 src[14]: native_decide vérifié → ... verifie (1) - Cell #43 src[2] : est entierement prouvé → est entierement prouve (1) - Cell #45 src[2] : On vérifié que → On verifie que (1) - Cell #48 src[11]: **P4 Prouvé** (table) → **P4 PROUVE** (1, maj main) - Cell #48 src[26]: **Prouvé** - preuve → **PROUVE** - preuve (1, maj main) - Cell #48 src[27]: P4 est desormais prouvé → ... prouve (1) - Cell #49 src[19]: certificat vérifié par machine → ... verifie ... (1) Préserve (Tell c.1347-L1 ★★★★ fondateur + main convention) : - #37 src[12] : formellement vérifié = participe attribut (auxiliaire `est` implicite sémantiquement récupérable). Tell c.974 §G.9 strict + main non accentué : préserve la décision main. Tell c.974 strict §C.1 scope strict : 0 cellule code, 0 output modifié. Tell c.1331-L5 ★★★★ byte-identique newline terminal préservé. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16868): retrait label variation-tag-missing obsolète Le label datait d'avant l'ajout du Grain tag dans le body. Le body porte 'Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2' (verifie first-hand via scripts/ci/variation_tag_required.py -> required_pass: true). Le perimeter check rend VERDICT: OK sur 1 fichier (Lean-16b-Conway-Game-of-Life-Lean.ipynb, +169/-169). repair_morpho.py --dry-run : 0 finding. Pas de REPAIR-N additif requis. Geste purement documentaire, redéclenche le PR gate. * fix(lean,#16987): restaurer docstrings EN accentuees + CAPS (reserve sec-c41) + re-exec complete Reserve secretary c.41 : la map REACCENT avait (a) accentue 2 docstrings anglaises (Execute -> Exécute, execution -> exécution, c2) et (b) degrade 8 formes CAPS d'emphase (PROUVE->Prouvé x2, REELS->Réels x3, REELLE->Réelle, PARSEUR RLE PROUVE, P4 PROUVE x2). - 10 restaurations exactes au merge-base 3b82612 (verification diff mb vs head, francais courant intact) - re-execution complete kernel python3 (worktree c1416-16987, cwd Lean) : 20/20 cellules, 0 erreur, execution_count 1-20 sequentiels, 1422s (conway_lean WSL reel) - metadata.papermill retiree post-exec Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(lean,#16987): 4 verbes 3e pers. corriges (REPAIR-2 faux positifs map REACCENT) Le REPAIR-2 morphologique (commit de la branche origin/fix/c1317-repair2-morpho-lean16b) avait accentué « vérifie » → « vérifié » dans 4 contextes où « vérifie » est un verbe 3e pers. sg. (sujet inanimé : `native_decide`, `still-life`, `On`), pas un participe passé. Geste scope strict, 1 fichier (Lean-16b-Conway-Game-of-Life-Lean.ipynb), 4 cellules (34, 40, 45, 48) : - Cellule 34 (markdown) : `native_decide\` vérifié \`true/false\`` → `native_decide\` vérifie \`true/false\``. Le « vérifie » porte sur `native_decide` (sujet), pas sur une hypothèse passée. - Cellule 40 (code) : `# ... un still-life vérifié step(g) == g` → `# ... un still-life vérifie step(g) == g`. Le commentaire décrit la propriété (« vérifie que step(g) == g »), pas un état passé. - Cellule 45 (markdown) : `On vérifié que la fondation Life ...` → `On vérifie que la fondation Life ...`. « On » est le sujet, « vérifie » est le verbe. - Cellule 48 (markdown) : `**Prouvé**` → `**PROUVE**`. Le tag de la ligne de roadmap garde `**P4 PROUVE**` (identifiant du tag), le texte descriptif doit s'aligner (mêmes lettres capitales, pas d'accent). Les autres occurrences `prouve` minuscule sont des verbes 3e pers. sg. et ne changent pas. Re-execution de la cellule 40 vérifiée : `execution_count: 16` et outputs cohérents, scope strict commentaire. Pas de re-execution sur les autres cellules (markdown only). Tell c.974 §G.9 vérif first-hand : 4/4 patterns grepés sur git show <sha_branche_actuelle>:<notebook> avant correction, cellules cibles vérifiées une à une, autres `vérifié` du notebook inspectées et laissées intactes (participes passés legitimes). Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean,#16987): env lake repris d'aplomb + re-exec reelle sous python3119 — sorties des cellules 38/42/46 restaurees Réponse à la réserve po-2026:CoursIA-3 (tête aa28e7e) : la re-exec de 9ffaa89 avait tourné dans un env lake cassé (checkout mathlib refusé, sorties dégradées rc=-1 / 0 verdicts / error: masqué par le rc du pipe). Réparation par la cause (Stop & Repair) : - .lake/packages/mathlib repositionné sur le rev épinglé 520045ab14, oleans prébuilds via lake exe cache get (6.2G, 8527 fichiers) ; - lake build Conway.Life{,Spaceships,Oscillators} + Conway.Life.RLE : Build completed successfully (3000 jobs), 0 error: ; - re-exécution INTÉGRALE du notebook sous kernel python3119 (CPython 3.11.9 = language_info de la base — le drift 3.13.7 introduit par la re-exec cassée est résorbé) ; Acceptance de la review, mesurée au head : - cell 38 : « 7/7 predicats du zoo A4 evalues a true » ; - cell 42 : « 7/7 #eval du parseur RLE conformes » ; - cell 46 : lignes info: sans error:, « Build completed successfully », SUCCESS réel cette fois (le défaut wrapper rc-masqué est tracké en issue #17616) ; - 20/20 cellules code, exec 1..20 contigus, 0 erreur, 0 chemin machine. Grain: REPAIR/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16868 Co-Authored-By: Claude-Code <noreply@anthropic.com> * fix(lean,#16987): Hermes reserve donne→donné (cellule 15, a un endroit donne) La reserve Hermes du 20/09 tient toujours: a un endroit donne est un participe passe adjectif legitime ('un endroit precis'), pas un verbe donner 3e pers. Tell c.1317-L1 REPAIR-1 a trop zele en aplatissant aussi cette occurrence, distincte de la locution figee 'etant donne'. Les 3 autres occurrences de 'donne' (verbes legitimes) sont conservees: - cell[12] section-3b-interp: 'Le notebook donne l intuition visuelle' - cell[19] acte1-otca: 'elle donne *Life*' - cell[30] section-7-turing: 'Pilier 2 (OTCA Metapixel) donne deja' Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com> * fix(lean): prose Conway sans compteurs 'N cells' (population N) -- prose-counts strict --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16956-repair-open
Résumé
REPAIR morphologique de la PR #16868 Lean-16b Conway Game of Life : la map REACCENT sub-grain #16638 a transformé
prouve(verbe 3e pers. sg) enprouvé(participe passé masc. sing.) en prose markdown, etdecide(tactique Lean) endécide(FR) en contexte technique. 30 corrections cellules [0, 7, 16, 21, 25, 27, 37, 41, 43, 48]. Diff stat strict +26/-26.Diagnostic Tell c.1315-L1 ★★★★★ fondateur MAJEUR
Le défaut a été identifié par scan ciblé des PRs sub-grain #16638 mergées + ouvertes. Lean-16b contenait 27 faux
prouvéen prose + 3décide(cellules mentionnantnative_decideentre backticks). Cause racine identique à #16956 Lean-4 = map REACCENT sans discrimination morphologique.Voie canonique Tell c.1315-L4 ★★★ fondateur NEW
Même script que PR #16956 Lean-4 :
scratchpad/repair_morpho_c1315.py. Heuristiquedécideétendue Tell c.1315-L14 ★★★ : contexte tactique (cellule avec tactique entre backticks) ⇒décideest probablement la tactique implicite en prose, pas le verbe FR.Cas ambigus signalés
3 occurrences
décidecell #21 Lean-16b corrigées automatiquement :decide(description de la preuve)decide(rendu = verbe, décide = tactique dans ce contexte)decide(mais accord fautif de toute façon, le notebook garde la forme anglaise)Note : la 3e occurrence ("être décide") est sémantiquement ambiguë — l'anglais "to decide" n'a pas d'équivalent direct en participe passé FR. Laissé tel quel après correction vers
decide; à voir avec auteur pour reformulation.Intégrité C.2
prouvérestantestouaauxiliaire = légitime)déciderestant🤖 Generated with Claude Code