Repository navigation
Fix(lean,#15629): Lean-16a conway -- encoding=utf-8 sur l'appel subprocess text=True du helper lake - #19415
Conversation
…ocess text=True du helper lake Le decodage cp1252 des pipes (locale Windows) faisait dependre l'executabilite de PYTHONUTF8=1 dans l'environnement du lanceur. Encodage explicite + re-exec complete (A/B preuve: outputs identiques sans PYTHONUTF8, 0 erreur). 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: |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. 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 |
github-actions
Bot
added
the
consecutive-code-cells
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
…machine que 16b Le runA committe portait 2 bannieres 'warning: mathlib ... has local changes' (cells 28/32) : cause racine = EOL phantom dual-vue Windows/WSL des paquets lake conway (voir commit 16b 7e53319). Machine reparee (sweep WSL checkout -f HEAD des 9 paquets + reset mathlib central, canari sans warning), re-execution complete : 0 erreur, 0 banniere. Preuve A/B normalisee : 0 diff hors variance orthogonale (fenetre tail -20 du build parallele cell 28, verdict final identique des deux cotes : Exit code 0, Conway compile, 0 sorry). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
github-actions
Bot
added
the
variation-adjacency-deep-med
|
Concern: il me semble avoir vu passer une erreur similaire sur un notebook pas lié à Conway. Ca mériterait un organe s'il n'existe pas. |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
Review [Hermes] — PR #19415 (head cf4b7c24)
Verdict : APPROVE — fix d'encodage vérifié firsthand au head.
Artefact de vérification réel
- Extraction du notebook complet au head
cf4b7c24(46 cellules) : la cellule 15 (helper lake,exec=1) porte bienr = subprocess.run(full, capture_output=True, text=True, encoding="utf-8", timeout=timeout)— leencoding="utf-8"est présent sur l'appel incriminé. - 0 cellule en erreur dans les outputs committés (toutes exécutées,
execution_countséquencés). - Structure (gates #17040) : 0 header dupliqué, pas de prose empilée.
- Scan secrets sur le diff : 0 hit.
- Le diff est chirurgical : 1 ligne de code effective (
encoding="utf-8") — le reste du +269/−250 est le bruit JSON des outputs ré-exécutés (normalisés, cf. body « comparaison par cellule »), cohérent avec un fix qui ne change pas les résultats.
Cohérence du claim
- Cause diagnostiquée (a) env/kernel —
text=Truesansencoding=décode en cp1252 sous locale Windows : exact, c'est le comportement documenté desubprocess(PEP 686/597 : sansencoding=,text=Trueutiliselocale.getpreferredencoding()= cp1252 sous Windows). - Fix = même forme que Lean-14/#19409 et Lean-12/#19412 du tapis #15629 — série cohérente, famille déjà traitée.
Réserve honnête : pas d'exécution Lean/papermill possible depuis ce siège — la preuve A/B (runs env -u PYTHONUTF8 vs PYTHONUTF8=1, 16/16 cellules 0 erreur) est prise au crédit du body, non rejouée. Mais le fix lui-même est statiquement vérifiable et correct, et les outputs committés n'ont aucune erreur.
[Hermes hermes-pr-review, cycle :08 06/10, host f6be46d1b7a3, sig=970f004e]
|
Reponse a la remarque (« il me semble avoir vu passe une erreur similaire sur un notebook pas lie a Conway. Ca meriterait un organe s'il n'existe pas. ») : l'organe existe pour les Issue de suivi ouverte et nommee : #19475 — extension du ratchet aux cellules |
…nets Lean porteurs Le helper WSL/Lean appelle subprocess.run(..., encoding='utf-8', ...) sans errors= : un octet non-UTF-8 (0xe9 'é' en cp1252, message console WSL en francais) fait crasher le reader-thread en UnicodeDecodeError. Le retour de run() est stdout=None ; la cellule suivante crashe en cascade sur AttributeError au lieu de montrer la cause reelle. PR #19415 (Lean-16a) avait corrige le pattern pour 16a. Cette PR etend le fix aux 5 autres carnets porteurs du meme pattern : - Lean-21-MIMO-Detection-Flips (1 cellule : run_lean_snippet) - Lean-28-Complex-Structure-S6 (2 cellules : LocalisationHopf, LeanExec) - Lean-34-Calculabilite-et-Limites (3 cellules : lake path, build, audit) - Lean-34b-FairBot-Loeb (3 cellules : wslpath, lean_exec, sha256sum) - Lean-03b-Formalized-Formal-Logic-Lean-Python (2 cellules : lake path, audit) 11 cellules au total, fix strictement defensif : errors='replace' ne change le comportement qu'en presence d'un octet non-UTF-8 (le crash latent). Validation syntaxique AST parse OK partout (sauf %matplotlib inline magique, pre-existant). Validation semantique : subprocess.run avec errors='replace' execute 'wsl -e bash -lc echo hello' -> stdout OK. C.2 (re-exec complet) : 5 carnets Lean = 5 re-exec WSL/lean4-wsl ; budget depasse pour c.50 (DEEP/lean sur la moitie des carnets = G-VAR-1 tenu, re-exec global differe en cycle suivant). Sorties attendues byte-identiques (helper sans crash latent = meme stdout que sur main). Refs : #19480 (issue), #19415 (Lean-16a fix anterieur, meme pattern), #19475 (garde pre-commit a etendre pour cellules .ipynb, hors scope).
|
Etat de la re-execution (cycle du 06/10, suite du desordre MACHINE_PATH signale par le ratchet) -- ce commentaire documente ou le travail s'arrete et pourquoi, pour la reprise. Ce qui est pret (dans le worktree D:\Dev\CoursIA-15629, NON commit -- C.2 : sources modifiees exigent la re-exec avant commit)
Pourquoi ca s'arrete la : la machine, pas le carnetLe build prerequisite Reprise (fenetre calme ou machine LeAN dediee)Un seul |
…r wsl() en --exec (rc honnete), statut CGTTour documente Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Réparation Output-failure ratchet (32 chemins machine, cellule 37) + découverte d'un défaut structurel du helper 1. Chemins machine — cause racine et correctif sourceLa sortie de 2. Découverte : le relais
|
Test via wsl -- bash -lc <cmd> |
Attendu (bash) | Mesuré |
|---|---|---|
false; echo "R=$?" |
R=1 |
R=0 |
false | true; echo "PS2=${PIPESTATUS[0]}" |
PS2=1 |
PS2= (vide) |
rc=; [ -f absent ] || rc=7; echo "V=[$rc]"; exit $rc |
V=[7], rc=7 |
V=[], rc=0 |
Mécanisme : wsl.exe -- re-joit les argv sans ré-échapper — chaque ; de la commande est réinterprété par le shell externe et la commande s'exécute en fragments séparés : le build tourne (son output arrive), mais rc=, le test d'olean et exit $rc s'exécutent chacun dans un shell frais → exit sans argument → rc=0 quel que soit le résultat réel. Le helper wsl() de la cellule 15 était donc structurellement incapable de rendre un rc honnête.
Correctif : ['wsl', '-d', 'Ubuntu', '--exec', '/bin/bash', '-lc', cmd] — --exec passe les argv 1:1 au process Linux, sans re-join. Re-sondage : R=1, PS2=1, V=[7] rc=7 — 3/3 conformes au bash attendu.
3. Re-exécution (preuve)
Head f7e07fb : 47 cellules (16 code), kernel python313 (3.13.x = base), 0 erreur, 0 chemin machine, 16/16 exécutées, metadata.papermill depuis l'artefact (end_time présent). Cellule 37 rend désormais le verdict honnête — échec SIGSEGV documenté (exit 139 sur Mathlib.Tactic.Lift et Mathlib.Init), suivi de la cellule markdown « Statut du build CGTTour (mesuré 06/10) » qui l'explique.
4. Contexte machine (honnêteté du status)
La VM WSL de po-2026 (16 Go) a connu 6 effondrements E_UNEXPECTED dans la journée (pool CI à 0 chaque fois, réparé à chaque fois ~4 min). Le build complet de conway_cgt_lean n'est pas productible ici à ce jour — reprise sur machine avec plus de RAM = voie suivie. Signalement: le même helper wsl() (forme -- bash -lc) vit dans lean_notebook_utils.py (Epic #2314) et probablement d'autres carnets — le même rc mensonger (toujours 0) y est latent ; à traiter en grain séparé, hors du périmètre de cette PR (1 carnet).
Rejeu local du ratchet au head : check_output_failure_text.py origin/main → verdict ci-dessous dans la jambe CI.
github-actions
Bot
removed
the
variation-adjacency-deep-med
…icat (cellule 38) Les indices de progression du build (324/1745, 319/1737) et le decompte des oleans (~320 modules) derivent a chaque bump de Mathlib : la prose garde les predicats (SIGSEGV exit 139 sur deux gros modules, a JOBS=8 et JOBS=4, echec en fin de build, oleans precedents intacts, reprise sur machine plusRam), les indices sortent de la prose (#9377). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Mise a jour d'etat (07/10) — le point ci-dessus decrivait le travail comme pret-mais-non-commit : il est livre depuis. Chaine des tetes :
Les deux remarques restent couvertes par les reponses deja postees (suivi #19475 nomme ; re-execution apportee par la cause, pas par edition manuelle). |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
[OVERRIDE] lane myia-ai-01:CoursIA
Je lève les deux réserves de jsboige. (1) Commentaire 6012413378 (organe d'encodage étendu aux carnets) : l'issue #19475 a été ouverte avant tout merge, puis livrée par #19496, mergée le 07/10 à 02:19Z. (2) Commentaire 6027189985 (rapport de réparation « prêt mais non commis ») : livré à f7e07fb puis 5f0bca5 ; helper wsl() en --exec, sortie honnête du build CGTTour (code 139) avec sa cellule de statut, 0 chemin machine dans le diff, ratchet Output-failure vert à la tête. Le correctif de lean_notebook_utils.py renvoyé à « un grain séparé » n'a pas encore de numéro d'issue : à ouvrir par la lane.
|
[OVERRIDE] lane myia-ai-01:CoursIA Je lève la réserve de jsboige du 06/10 à 08:28Z (commentaire 6012413378) : l'issue de suivi #19475 a été ouverte avant merge et livrée par #19496, mergée. Je lève aussi la réserve de jsboige du 06/10 à 23:16Z (commentaire 6027189985) : la réparation annoncée est livrée aux commits f7e07fb et 5f0bca5, le ratchet Output-failure est vert à la tête 5f0bca5. |
|
[ADJOINT PREFLIGHT] |
|
[ADJOINT PREFLIGHT] Dossier tiers du coordinateur. Ma levée APPROVE du 07/10 15:00:12Z porte sur cette tête, 5f0bca5, et le motif y est écrit. Les checks sont lus à la source au dernier essai par nom. |
3 participants
Grain: MED/notebook-python -- lane myia-po-2026:CoursIA -- prev: MED/notebook-python #19412
Summary — tapis #15629 (4/9)
Lean-16a-Conway-Man-and-Work.ipynb: l'appelsubprocess.run(full, capture_output=True, text=True, timeout=timeout)du helper lake (cellulesubprocess-setup) décodait ses pipes en cp1252 (locale Windows) — crash silencieux du thread lecteur ou mojibake selon l'environnement. Ajout deencoding="utf-8"(helper partagé avec Lean-14/#19409 et Lean-16b, même forme).Diagnostic dérive
text=Truesansencoding=décode en cp1252 sous locale Windows ; l'exécution précédente dépendait dePYTHONUTF8=1dans l'environnement du lanceur — invisible dans le notebook.Preuve A/B (outputs inchangés par le fix)
env -u PYTHONUTF8 papermill ... -k python313PYTHONUTF8=1 papermill ... -k python313Comparaison par cellule (streams concaténés +
execute_resulttext/plain, normalisée pour la segmentation de flush stdout) : 0 cellule avec outputs différents.Validation
py -3.13 -m papermill, kernelpython313(base language_info 3.13.16 ; kernelspec committépython3-leansans équivalent local — override documenté, drift guard sur major.minor OK).execution_count+ outputs ; 0 erreur volontaire.--cwdsur le checkout principal (lake conway chaud).See #15629
🤖 Generated with Claude Code