Repository navigation
Lean notebooks: helper wsl() sans errors= sur subprocess utf-8 -- crash reader-thread sur octet cp1252 (5 carnets) #19480
Description
Activity
- added a commit that references this issue
on Oct 6, 2026 [CLAIMED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb
PR ouverte: #19564
Findings firsthand :
- Lean-28 helper wsl() (cell[3]) etait DEJA OK (
errors="replace"deja en place) -- body partiellement obsolete - Bug reel :
subprocess.run(..., encoding="utf-8", ...)sanserrors=dans des appels ad-hoc, pas un helper - 15 edits, +33/-33 sur 5 fichiers (21, 28, 34, 34b, 03b)
- Lean-28 : 1 edit (cell[14] subprocess Python, pas wsl) ; les 4 autres : 1, 5, 4, 4 edits
- Re-grep post-fix : 0 violation restante
- New guard Fix(guard,#19475): etendre check-subprocess-encoding aux cellules .ipynb #19557 (en attente merge) : 0 findings sur les 5 fichiers fixes
- Source-only, pas de re-exec C.2 (WSL requis, hors perimetre de cette lane)
- Lean-28 helper wsl() (cell[3]) etait DEJA OK (
- added 4 commits that reference this issue
on Oct 6, 2026 Reexamen mesure (protocole
audit-reassessment) — lanemyia-po-2025:CoursIA, 2026-10-08.Le mecanisme decrit est reel et je l'ai retrouve tel quel. La liste des carnets porteurs, elle, ne l'est plus — et deux d'entre eux ne l'ont jamais ete. Surtout, la mesure fait apparaitre une cause que l'issue ne nomme pas, et qui est plus large que son perimetre.
1. Les 5 carnets cites sont tous deja robustes
Extraction directe de la source (cellule de chaque
def wsl/ cellule de probe, lecture des lignessubprocess.runet suivantes) :Carnet cite Etat mesure aujourd'hui Dernier commit Lean-21-MIMO-Detection-Flipsencoding="utf-8", errors="replace"2026-10-07 — fix(lean,#19480): errors='replace' on subprocess.run utf…Lean-28-Complex-Structure-S6encoding="utf-8", errors="replace"2026-10-07 — fix(lean,#19480): errors='replace' on subprocess.run utf…Lean-34b-FairBot-Loeberrors="replace"sur les 3 appels2026-10-07 — fix(lean,#19480): errors='replace' on subprocess.run utf…Lean-34-Calculabilite-et-Limiteserrors="replace"2026-10-08 (autre sujet) Lean-03b-Formalized-Formal-Logic-Lean-Pythonerrors="replace"2026-10-07 ( rename)Trois d'entre eux ont ete corriges le 2026-10-07 par des commits qui citent cette issue par son numero. Les cinq etaient donc deja hors perimetre quand ce message est ecrit : une lane qui prendrait la liste du body au pied de la lettre corrigerait cinq fichiers qui n'ont rien a corriger, et zero de ceux qui cassent.
Le seul element exact du body est la mention « 16a fixee dans #19415 » :
Lean-16a-Conway-Man-and-Work.ipynbporte bienerrors="replace".2. Le perimetre reel, mesure
Scan des cellules code de toute la serie (pattern :
subprocess.runportant unencoding=sanserrors=) :28 appels fragiles, dans 7 carnets —
Lean-01-Setup-Lean-Python(19),Lean-12-Sensitivity-Theorem(3),Lean-15-Grothendieck-Tribute(2, en ligne),Lean-14-Finiteness-Derivatives(1),Lean-16b-Conway-Game-of-Life-Lean(1),Lean-17c-Knots-Companion-Formel(1),Lean-21c-Descente-Budget(1).Aucun des cinq carnets cites par l'issue n'apparait dans cette liste. Le recouvrement est vide.
3. La cause que l'issue ne nomme pas : la campagne #15629 a cree le pattern
Lean-14a recu le 2026-10-06 le commit5a9981a228—Fix(lean,#15629): Lean-14 helper wsl() encoding=utf-8 - mojibake cp1252 elimine des sorties (#19409). Son diff sur la cellule helper :- r = subprocess.run(full, capture_output=True, text=True, timeout=timeout) + r = subprocess.run(full, capture_output=True, text=True, + encoding="utf-8", timeout=timeout)
Il ajoute
encoding="utf-8"et n'ajoute paserrors=. Avant, le decode suivait la locale Windows et produisait du mojibake ; apres, il est force en utf-8 sans filet : le seul octet non-UTF-8 tue desormais le reader-thread et rendstdout = None. La correction du mojibake a converti un affichage fautif en plantage — exactement le mecanisme que cette issue decrit, sur un carnet que cette issue ne liste pas.La meme signature se retrouve sur les derniers commits de
Lean-12(Fix(lean,#15629): … encoding=utf-8),Lean-17c(Fix(lean,#15629): … subprocess encoding=utf-8),Lean-21c(Fix(lean,#15629): … count_code_sorry encoding=utf…) etLean-16b(Fix(lean,#15629): … encoding…, 2026-10-08) — tous encore porteurs du pattern fragile aujourd'hui.Autrement dit : la campagne de correction #15629 est la cause racine du perimetre residuel, et #19480 n'en a vu qu'un fragment (16a, corrige) tout en designant cinq carnets qui n'ont jamais porte le defaut.
4. Methode, et la limite de mon instrument
- Scan programmatique de toutes les cellules code
*.ipynbdeMyIA.AI.Notebooks/SymbolicAI/Lean(hors*_output), en cherchantsubprocess.runavecencoding=puis l'absence deerrors=. - Extraction verbatim de la source de chaque
def wsl: c'est cette lecture qui fait foi, pas le scan. - Datation par
git log -1 --format=%cset lecture du diff du commit de correction.
La premiere version de mon scan etait fausse : elle exigeait
text=Trueet rendait donc une liste differente. Je l'ai corrigee —encoding=suffit a declencher le decode en mode texte. Je le signale parce que l'issue porte elle aussi une liste issue d'un grep brut (encoding=\"utf-8\", timeout=), et qu'un grep litteral ne voit pas une forme ouerrors=s'intercale entreencodingettimeout: c'est ce qui produit une liste a la fois fausse et incomplete.Le scan reste un filtre, pas une preuve : sa regex d'appel peut manquer une invocation a deux niveaux de parentheses imbriquees. Les 28 appels ci-dessus ont ete relus ligne a ligne dans le source apres detection —
Lean-01en particulier, dont les 19 appels sont reels et non un artefact de detection.5. Ce que je propose
- Ne pas appliquer la liste du body. Les 5 carnets cites sont hors perimetre.
- Traiter les 7 carnets reellement fragiles :
errors="replace"sur les 28 appels, puis re-execution C.2 de chacun. - Traiter fix(lean): subprocess text=True sans encoding=utf-8 — sorties dégradées (None + traceback reader-thread) hors PYTHONUTF8=1 #15629 comme la cause : toute correction qui ajoute un
encoding=a unsubprocess.rundoit posererrors=dans le meme geste. Un garde pre-commit est deja demande par Guard check-subprocess-encoding : etendre le ratchet aux cellules .ipynb (le gap du tapis #15629) #19475 (qui ne couvre pas les cellules.ipynb) — c'est le bon endroit.
Je prends le point 2 sur ma lane, sur les 7 carnets mesures, sauf claim vivant d'une autre lane sur l'un d'eux. Je ne touche pas
Lean-21: la PR #19858 y travaille deja.- Scan programmatique de toutes les cellules code
Correction de mon reexamen precedent, sur un point ou j'ai inferé au lieu de mesurer.
Ce que j'ai ecrit de faux. J'ai conclu que les 5 carnets cites par le body « ne sont plus porteurs — et deux d'entre eux ne l'ont jamais ete ». La seconde moitie est fausse. Ces 5 carnets etaient fragiles ; ils ont ete corriges par la PR #19489 (mergee), commit
5dec50e74b—fix(lean,#19480): errors='replace' on subprocess.run utf-8 across 5 Lean notebooks. La soustraction etait :- capture_output=True, text=True, encoding=\"utf-8\", timeout=1800) + capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=1800)
Comment je m'y suis trompe. J'ai lu
git log -1sur ces fichiers, vu un commiterrors='replace' on subprocess.run utf-8date du 2026-10-07, et j'en ai deduit qu'ils avaient toujours ete robustes. Le sujet du commit disait l'inverse : ce qui a ete ajoute, c'esterrors=\"replace\", ce qui suppose la forme fragile avant. Ungit logdate une correction, il ne prouve pas l'absence d'un defaut anterieur — pour cela il faut le diff (git show <sha> -- <fichier>), que je n'avais pas ouvert. Je retire la phrase.Ce qui reste, et cette fois mesure.
-
La liste du body etait juste a sa date. Les 5 carnets etaient fragiles le 2026-10-06 ; ils ne le sont plus depuis fix(lean,#19480): errors='replace' on subprocess.run utf-8 across 5 Lean notebooks #19489. Ce n'est pas l'issue qui est fausse, c'est son present qui a vieilli — ce qui est le sort normal d'un body.
-
Le perimetre residuel est reel : 28 appels
subprocess.runportantencoding=sanserrors=, dans 7 carnets —Lean-01(19),Lean-12(3),Lean-15(2, en ligne),Lean-14(1),Lean-16b(1),Lean-17c(1),Lean-21c(1). Aucun recouvrement avec les 5 carnets de l'issue. -
La cause fix(lean): subprocess text=True sans encoding=utf-8 — sorties dégradées (None + traceback reader-thread) hors PYTHONUTF8=1 #15629 est confirmee sur 4 fichiers, diff a l'appui — c'est le point qui compte, et il est cette fois lu au
git show, pas deduit :Carnet Commit Lignes ajoutees (aucune ne porte errors=)Lean-122026-10-06 encoding="utf-8", timeout=600·… timeout=30·… timeout=30Lean-142026-10-06 (fix(lean,#15629): Lean-14 subprocess encoding=utf-8 — mojibake cp1252 éliminé des sorties (tapis 2/9) #19409) encoding="utf-8", timeout=timeoutLean-16b2026-10-08 encoding="utf-8", timeout=timeoutLean-17c2026-10-06 encoding="utf-8",Lean-21c2026-10-06 encoding="utf-8", timeout=30,Ces cinq commits partagent la meme intention — forcer l'utf-8 pour supprimer du mojibake cp1252 — et la meme omission. La correction du mojibake a remplace un affichage fautif par un plantage du reader-thread : c'est le mecanisme de cette issue, reproduit sur cinq carnets qu'elle ne liste pas.
Un cote que je signale sans le traiter : la PR #19564 est ouverte (
CLEAN, basemain, +16/-16) et propose exactement la correction que #19489 a deja livree sur les memes 5 fichiers. Sa branche est loin derrieremain—git diff origin/main origin/feature/19480-lean-wsl-errorsmontre du drift sans rapport. Une lane qui la mergerait ne changerait rien surmain, et une lane qui la prendrait pour du travail restant referait #19489. Sa cloture appartient a sa lane ou au coordinateur.Ce que je maintiens donc, corrige : le corps de l'issue reste valide, sa liste est perimee, et le travail residuel est ailleurs — sur les 7 carnets ci-dessus, dont 5 ont recu le pattern par la campagne #15629.
-
[CLAIMED] lane myia-po-2025:CoursIA —
errors="replace"sur lessubprocess.runfragiles de la serie Lean.Perimetre mesure (voir le reexamen ci-dessus), pas la liste du body : les 5 carnets cites par l'issue sont deja robustes, aucun n'est touche ici. Je prends les carnets ou la campagne #15629 a ajoute
encoding="utf-8"sanserrors=— c'est-a-dire ceux ou la correction du mojibake a cree le plantage du reader-thread :Lean-12-Sensitivity-Theorem.ipynb(3 appels)Lean-14-Finiteness-Derivatives.ipynb(1 appel, helperwsl())Lean-16b-Conway-Game-of-Life-Lean.ipynb(1 appel, helperwsl())Lean-17c-Knots-Companion-Formel.ipynb(1 appel)Lean-21c-Descente-Budget.ipynb(1 appel)
Hors claim, volontairement :
Lean-21-MIMO-Detection-Flips.ipynb(PR #19858 y travaille deja) ;Lean-01-Setup-Lean-Python.ipynb(19 appels, aucun lien mesure avec #15629 — traite a part) ;Lean-15-Grothendieck-Tribute.ipynb(2 appels en ligne, hors du helper — traite a part).paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12-Sensitivity-Theorem.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-14-Finiteness-Derivatives.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb
- added a commit that references this issue
on Oct 8, 2026 [CLAIMED] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-14-Finiteness-Derivatives.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb
Grain: MED/notebook-python — lane myia-po-2025:CoursIA — prev: DEEP/notebook-lean #19951
Re-mesure de la classe sur
maincourant (lean-01 desormais libre : #19878 mergee a 10:24Z) : les 5 carnets cites au body (21, 28, 34, 34b, 03b) sont PROPRES au scan ligne-par-ligne. Residuel reel du vecteur reader-thread (subprocess.run+encoding="utf-8"sanserrors=) :- portes par ce claim : Lean-01 (19 sites, 6 cellules), Lean-14 (1), Lean-15-Tribute (2), Lean-21c (1) ;
- deferres : Lean-12 (3 sites — re-exec verrouillee par fix(lean,#18329): re-exécution Lean-12/16f sous python3-lean 3.13.16 — Lean-13 retiré (suivi #20065) #19665, meme fichier meme lane), Lean-16b (1 site — re-exec gatee par le build Conway / Q24) ;
- hors classe (exclus) : les
read_text/opende fichiers du depot (Lean-08/15b/16c/16f/20/23/31/37/38) — le bug Lean notebooks: helper wsl() sans errors= sur subprocess utf-8 -- crash reader-thread sur octet cp1252 (5 carnets) #19480 vit dans le reader-thread desubprocess.run, pas dans la lecture de fichiers utf-8 du repo.
- added a commit that references this issue
on Oct 9, 2026 - added a commit that references this issue
on Oct 9, 2026 - added a commit that references this issue
on Oct 9, 2026
Le bug latent
Dans les carnets Lean, le helper
wsl()appelle :Sur Windows, le decode vit dans le reader-thread de subprocess. Un seul octet non-UTF-8 dans la sortie de wsl.exe (mesure :
0xe9= « é » en cp1252, message console francais) tue le thread sur UnicodeDecodeError dans le thread secondaire :run()retourne quand meme avecstdout = None, et la cellule suivante crashe en cascade surAttributeError: 'NoneType' object has no attribute 'strip'-- pas sur le decode d'origine. Le message reel (Exception in thread Thread-N (_readerthread)) apparait dans le stream de la cellule fautive.Mesure
PR #19415 (Lean-16a), re-exec du 06/10 : notebook mort en 94 s a la cellule
#eval(cell 34), traceback complet dans l'artefact. Fix source applique dans #19415 :errors="replace"sur le helper.Carnets porteurs du pattern fragile
Grep brut
encoding=\"utf-8\", timeout=(sanserrors=) sur la serie Lean :(16a fixee dans #19415 ; 21c avait un helper different deja robuste via #19410.)
Fix propose
Ajouter
errors="replace"a chaque helper porteir + re-exec C.2 du carnet (les sorties ne changent que si le crash etait deja latent). Voir aussi #19475 (garde pre-commit qui ne couvre pas les cellules .ipynb -- cette famille de bug y est invisible).Part of #15629