fix(lean,#15629): subprocess encoding="utf-8" sur l'appel lake env lean du notebook Lean-22 by jsboige · Pull Request #15668 · jsboige/CoursIA

jsboige · 2026-09-11T23:48:38Z

Grain: MED/notebook-lean — lane myia-po-2026:CoursIA — prev: MED/docs #15577

Sujet (tranche Lean-22 de #15629)

Le notebook Lean-22-MIMO-Detection-Flips.ipynb (cellule 9) appelle lake env lean via subprocess.run(..., text=True) sans encoding= : sur une machine ACP-1252, le thread lecteur du pipe décode en page de code ANSI et crashe sur les glyphes non-cp1252 des sorties Lean (ℝ, ℕ, →), laissant res.stdout = None — sans erreur remontée à Papermill (l'exécution paraît verte, la sortie est muette).

Fix (+2/−1, cellule 9)

subprocess.run(["lake", "env", "lean", str(tmp)],
               cwd=str(LAKE_DIR), capture_output=True, text=True,
               encoding="utf-8", timeout=600)

Recensement par parsing à parenthèses équilibrées des appels : exactement un appel text=True sans encoding dans ce notebook — les encoding="utf-8" détectés à proximité par un scan fenêtré sont ceux de tmp.write_text(...), pas du subprocess (faux positifs du scan naïf).

Contrôle positif du mécanisme (machine myia-po-2026, GetACP=65001)

Cette machine a l'option système UTF-8 active — le contexte cp1252 de l'incident ne peut pas y vivre naturellement. Le contrôle positif force l'encoding du pipe pour simuler une machine ACP-1252 sans le fix :

EMITTER = [sys.executable, "-c", "print('theorem flip_descend : Real ℝ (glyphs) ℕ → ✔')"]
subprocess.run(EMITTER, capture_output=True, text=True, encoding="cp1252")  # simulé sans fix
subprocess.run(EMITTER, capture_output=True, text=True, encoding="utf-8")   # le fix

Appel cp1252 — signature exacte de l'incident :

Exception in thread Thread-1 (_readerthread):
UnicodeDecodeError: 'charmap' codec can't decode byte 0x9d in position 30: character maps to <undefined>
res.stdout = None
res.stderr = ''

Appel utf-8 (le fix) :

res2.stdout = 'theorem flip_descend : Real ℝ (glyphs) ℕ → ✔\n'

Exécution réelle (C.2) — build + runs A/B

mimo_lean reconstruit : lake build 8702 jobs BUILD_OK, Converse.olean présent (Mathlib via cache).
Run A (sans PYTHONUTF8, env naturel du lanceur) : Papermill natif Windows, kernel python3, 41 cellules en 4:07 — 13 cellules code execution_count contigus 1..13, 0 erreur, 0 sortie dégradée "None", 5 cellules portent des glyphes non-cp1252 dans leurs sorties réelles.
Run B (avec PYTHONUTF8=1, mêmes MIMO_LEAN_PATH/--cwd) : 41 cellules en 3:36.
Outputs A/B identiques 13/13 (comparaison JSON cell-by-cell) — la dépendance à l'env du lanceur disparaît.

Le notebook committé est le run A exécuté (chemins metadata.papermill normalisés au basename, seule normalisation tolérée ; le hook de scrub des chemins absolus passe Passed).

See #15629 (tranche Lean-22 — l'issue reste ouverte pour les occurrences legacy restantes du pattern repo-wide)

🤖 Generated with Claude Code

…an du notebook Lean-22 La cellule 9 utilisait text=True sans encoding : sur une machine ACP-1252, le thread lecteur du pipe decode en page de code ANSI et crashe sur les glyphes non-cp1252 des sorties Lean, laissant res.stdout = None sans erreur remontee a Papermill. Fix : encoding="utf-8" explicite. Controle positif (machine GetACP=65001, encoding cp1252 force) : signature exacte de l'incident reproduite ; avec utf-8 la sortie est propre. Runs A/B Papermill (sans/avec PYTHONUTF8=1) : 41 cellules chacun, outputs 13/13 identiques - la dependance env disparait. Notebook committes = run A execute. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

github-actions · 2026-09-11T23:49:02Z

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

github-actions · 2026-09-11T23:49:31Z

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-11) :

TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=7 genre=15 cap=8)
GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=7 genre=15 cap=8)
NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

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 variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

github-actions · 2026-09-11T23:51:47Z

Notebook PR Validation: PASS

Notebooks checked: 1
Code cells validated: 13
Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

github-actions · 2026-09-11T23:53:42Z

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	10.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	9.7s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	11.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	10.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	9.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	6.9s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	69.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	8.9s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

github-actions · 2026-09-12T01:47:12Z

Path-collision (organ #13359/#13615)

Cette PR #15668 (fix(lean,#15629): subprocess encoding="utf-8" sur l'appel lake env lean du notebook Lean-22) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

faible -- renum(lean,#15612): refermer la colonne canonique (trous 18/25) — deux decalages (19..24 en N-1, 26..32 en N-2), arborescence finale 01..30 #15613 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb

Conflit unique : modify/delete sur Lean-22-MIMO-Detection-Flips.ipynb. Ma branche l'a renomme en Lean-21-MIMO-Detection-Flips.ipynb (refermeture du trou 18 : decalage 19-22 vers 18-21) ; main l'a modifie (fix #15668 -- encoding="utf-8" sur l'appel `lake env lean`, suivi d'une re-execution). Resolution : le fichier renomme porte la version de MAIN -- le fix et sa re-execution sont conserves -- avec le renumerotage re-applique a l'identique (6 lignes source + 2 chemins papermill). Le delta de la PR vs main redevient strictement le renumerotage. Choix de provenance : main resout le lac en `mimo_lean` (conforme au PROJECT_NAME de la cellule de setup) et sa re-execution est posterieure ; la mienne resolvait un lake `mimo-build` de nom different. Verifications : 0 reference pendante (52 refs distinctes README, 20 production-scope) ; COURSE_CATALOG.generated.json et le CSV de traductions symbolicai-lean byte-identiques a main (artefacts derives, non touches). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

#15626) La base du stack a avance (merge de main dans #15613 : fix #15668 -- encoding="utf-8" + re-execution du notebook MIMO -- renumerotage re-applique). Ce merge l'absorbe en conservant les SHA : pas de rebase sur un stack (regle merge-not-rebase, enfant #15626 sur base #15613). Conflit unique, contenu, sur Lean-21-MIMO-Detection-Flips.ipynb : - cote base avancee : version de MAIN (fix + re-execution, lac mimo_lean) avec le renumerotage ; - cote enfant : 2 corrections source mesurees (la mecanique subprocess renvoie a Tao Lean-19, pas PFR Lean-20 ; libelle du lien Search-03e). Resolution : version de la base conservee (provenance la plus recente et coherente), les 2 corrections de l'enfant re-appliquees. Le diff de la PR vs sa base redevient strictement les corrections de refs croisees. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

… (cp1252 safe) (#15816) - Bug: scripts/notebook_tools/detect_accent_stripping.py crashait avec UnicodeEncodeError sur Windows (cp1252 par defaut) des qu'un notebook contenait un caractere hors-cp1252 (↔, →, ←, ⇔, ≡) frequent en prose FR pedagogique. Touchait les deux modes --json (json.dump avant fin) et la sortie lisible (print). - Fix: 3 lignes apres imports, sys.stdout.reconfigure(encoding="utf-8") avec hasattr(sys.stdout, "reconfigure") pour compatibilite Python < 3.7. - Sibling pattern : meme fix deja applique sur scripts/notebook_tools/ (et autres) par #12811, #13191, #14154, #15185, #15668. detect_accent_stripping oublie dans la vague -- c'est exactement la classe de defaut que le sibling pattern ferme en 3 lignes. - Tests : scripts/tests/test_detect_accent_stripping_encoding.py, 2 tests subprocess avec PYTHONIOENCODING=cp1252 (encoding="utf-8", errors="replace" cote test lui-meme, conformement au meme pattern). Verifie absence de UnicodeEncodeError / charmap en modes --check et --json. Co-authored-by: myia-po-2027 <po-2027@coursia.lan>

…ndependant de l'ACP) (#17432) * fix(#17427): check_exec_ratchet emet en UTF-8 deterministe — le verdict ne depend plus de l'ACP Sur Windows ACP 1252, l'organe lance en subprocess encodait ses pipes en cp1252 : l'em-dash des annotations ::error partait en byte 0x97, le lecteur (tests TestCli, encoding="utf-8") levait UnicodeDecodeError dans le reader thread -> stderr=None -> 2 faux rouges sur main Windows (verdict masque). Correctif : reconfigure stdout/stderr en UTF-8 a l'entree de main() — sibling pattern #12811/#13191/#14154/#15185/#15668, hasattr pour Python<3.7 et flux captes. Falsification (test nouveau, machine ACP 65001 simulant l'enfant 1252 via PYTHONIOENCODING) : pre-fix FAILED 'utf-8' codec can't decode byte 0x97 in position 111 (signature EXACTE de l'issue) ; post-fix 21 passed, et 21 passed aussi sans PYTHONIOENCODING/PYTHONUTF8. Fichier frere test_check_exec_sequence.py : 23 passed. Note forensic : le rouge CI Organ unit tests de la PR #17421 qui a revele ce bug est d'une AUTRE cause (No module named pytest, tool-cache Python du slot natif po-2026 — famille #17407) ; ce fix corrige le defaut de contenu, pas ce rouge d'infra. Closes #17427 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * fix(#17432): re-trigger CI after Scripts Tests flaky failure --------- Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>

github-actions Bot mentioned this pull request Sep 12, 2026

renum(lean,#15612): refermer la colonne canonique (trous 18/25) — deux decalages (19..24 en N-1, 26..32 en N-2), arborescence finale 01..30 #15613

Merged

This was referenced Sep 12, 2026

ci(pr-gate): le seul check requis ne publie pas son motif — output.title/summary null sur 5/5 PRs, la cause n'existe que dans le log #15693

Closed

fix(ict,#15536): trace contract v1.1.0 — instrument jlens_trackp, loader trackP branché #15548

Merged

jsboige merged commit bc02d1a into main Sep 12, 2026
70 of 72 checks passed

jsboige mentioned this pull request Sep 12, 2026

fix(symboliclearning,#15658): SL-12b' cellule verdict — cas introuvable sans crash + comptes dérivés #15680

Merged

jsboige mentioned this pull request Sep 12, 2026

fix(ci,#15693): publier le motif du verdict PR gate (output.summary + trois etats) #15725

Merged

jsboige mentioned this pull request Sep 22, 2026

fix(#17427): check_exec_ratchet emet en UTF-8 deterministe (verdict independant de l'ACP) #17432

Merged

myia-ai-01 mentioned this pull request Oct 5, 2026

fix(lean): subprocess text=True sans encoding=utf-8 — sorties dégradées (None + traceback reader-thread) hors PYTHONUTF8=1 #15629

Closed

Navigation Menu

Repository navigation

fix(lean,#15629): subprocess encoding="utf-8" sur l'appel lake env lean du notebook Lean-22 - #15668

fix(lean,#15629): subprocess encoding="utf-8" sur l'appel lake env lean du notebook Lean-22#15668
jsboige merged 1 commit into
mainfrom
fix/15629-lean22-subprocess-encoding

jsboige commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 12, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

jsboige commented Sep 11, 2026

Sujet (tranche Lean-22 de #15629)

Fix (+2/−1, cellule 9)

Contrôle positif du mécanisme (machine myia-po-2026, GetACP=65001)

Exécution réelle (C.2) — build + runs A/B

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Uh oh!

github-actions Bot commented Sep 11, 2026

Notebook PR Validation: PASS

Uh oh!

github-actions Bot commented Sep 11, 2026

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Sep 12, 2026

Path-collision (organ #13359/#13615)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant