Skip to content

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

Description

@jsboige

Defaut

Les notebooks Lean de la serie MyIA.AI.Notebooks/SymbolicAI/Lean/ appellent subprocess avec text=True sans encoding="utf-8" : le decode des pipes se fait alors en cp1252 (locale Windows), et toute sortie Lean portant un caractere non-cp1252 (ℝ, ℕ, →, ✔ — omnipresents dans les #check) fait crasher le reader-thread de subprocess.

Incident vivant (mesure du 2026-09-11)

Re-execution papermill de Lean-21-MIMO-Detection-Flips.ipynb (kernel python3, lake mimo_lean), sans PYTHONUTF8=1 dans l'env du lanceur : 6 cellules degradees — la sortie reelle #check remplacee par :

Exception in thread Thread-5 (_readerthread):
Traceback (most recent call last):
  ...
None

Classe connue

Inventaire (heuristique de proximite, sous-estimee — un encoding= voisin masque le compte)

Notebook appels text=True sans encoding a proximite
Lean-1-Setup 24
Lean-3b-Formalized-Formal-Logic 4
Lean-12-Sensitivity-Theorem 3
Lean-15-Grothendieck-Tribute 2
Lean-14, 16a, 16b, 17c, 21c 1 chacun
Lean-21-MIMO-Detection-Flips 1 (verifie vivant — le compte heuristique passe a cote, encoding du write_text voisin dans la fenetre)

Methode exacte de comptage a refaire par fichier (grep par appel, pas par fenetre).

Acceptance

  1. Tout appel subprocess a pipe texte dans les notebooks de la serie porte encoding="utf-8" explicite (le garde pre-commit devient inutile sur ces fichiers).
  2. Preuve par re-execution : outputs identiques avec et sans PYTHONUTF8=1 dans l'env du lanceur (la dependance env disparait).
  3. Serie par serie, un notebook par PR (C.3), chaque notebook modifie re-execute (C.2).

Activity

  1. added a commit that references this issue on Sep 11, 2026
  2. jsboige commented on Sep 11, 2026

    @jsboige
    OwnerAuthor

    [CLAIMED] lane myia-po-2027:CoursIA — tranche Lean-1-Setup.ipynb : porter encoding="utf-8" explicite sur les 24 appels subprocess a pipe texte qui en sont depourvus, puis re-executer le notebook avec ET sans PYTHONUTF8=1 pour etablir la disparition de la dependance env (acceptance 1+2).

    paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb

    Comptage exact par AST (et non par fenetre de proximite, comme le demande l'issue) : 39 appels texte sans encoding= sur la serie, dont 24 dans Lean-1-Setup (61 %). Un comptage naif surestime de 4 : il inclut les capture_output=True sans text=True, qui rendent des bytes et ne declenchent donc pas le decodage locale — ils sont hors defaut.

    Note de faisabilite : la cellule 15 est gardee par shutil.which("repl"), donc l'installation n'est rejouee que si repl est absent. La tranche est independante des autres notebooks (acceptance 3, un notebook par PR).

  3. jsboige commented on Sep 11, 2026

    @jsboige
    OwnerAuthor

    [CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb

    Resserrage du scope : la claim precedente etait epic-wide (pas de clause paths:), ce qui bloquait la serie entiere. La tranche livree est Lean-1-Setup.ipynb (24 sites sur 39). Le reste de la serie est rendu aux autres lanes.

    Notes de terrain mesurees, pour que la lane suivante ne les re-decouvre pas :

    Notebook Contrainte de re-execution mesuree
    Lean-3b-Formalized-Formal-Logic LAKE_DIR = subprocess.run(["wsl","-e","wslpath","-a", os.getcwd()]) puis cd {LAKE_DIR} && lake build FormalLogic.Bridge : le cwd du kernel doit etre MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean (le projet lake y vit, FormalLogic/Bridge.lean), sinon le build part dans un repertoire sans lakefile. Ce projet est froid (aucun .lake/) : prevoir un build complet, deps FormalizedFormalLogic/Foundation + Mathlib, timeout=1800 dans la cellule 11.
    Lean-1-Setup Cellule 19 localise le wrapper par Path.cwd().parent en repli quand __vsc_ipynb_file__ est absent (cas papermill) : le cwd doit etre le dossier du notebook (.../SymbolicAI/Lean), sinon [!] Wrapper script not found + echec de deploiement. Cellule 21 exige un venv WSL fonctionnel en ~/.python3-wsl-venv (voir ci-dessous).

    Environnement WSL, etat au 2026-09-11 (reparation effectuee, sans sudo) :

    • ~/.python3-wsl-venv etait casse et vide (32 K, symlinks python seuls, ni activate ni pip) — sequelle probable de l'incident du 04/09. Le script scripts/setup_wsl_python.sh ne le repare pas : sa garde if [ ! -d "$VENV_PATH" ] saute la creation parce que le dossier existe, puis source .../bin/activate echoue.
    • python3 -m venv ne marche pas en WSL : ensurepip absent, paquet python3.14-venv non installe, et sudo exige une authentification interactive (pas de sudoers NOPASSWD). Contournement applique : ~/.lean4-venv/bin/python3 -m venv ~/.python3-wsl-venv (3.11.16 + pip 24.0). L'ancien dossier est conserve en ~/.python3-wsl-venv.broken-20260911 (mis de cote, pas supprime).
    • Reste a faire cote machine, hors scope de cette PR : sudo apt install python3-venv pour que le venv systeme 3.14 soit recreable nativement.
  4. jsboige commented on Sep 11, 2026

    @jsboige
    OwnerAuthor

    [CLAIMED] lane myia-po-2026:CoursIA — tranche Lean-22-MIMO-Detection-Flips.ipynb (l'incident vivant mesuré dans le body : cell 9, appel lake env lean text=True sans encoding — vérifié ligne à ligne, le encoding= détecté par proximité était le tmp.write_text(...) voisin). Preuve A/B prévue : run sans PYTHONUTF8 (le contexte cp1252 de l'incident) + run avec, outputs identiques attendus après fix. Le reste de la série reste libre. Merci pour les notes de terrain de l'amend.

  5. added a commit that references this issue on Sep 12, 2026
  6. added 2 commits that reference this issue on Sep 12, 2026
  7. added a commit that references this issue on Sep 13, 2026
  8. added
    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)
    on Sep 13, 2026
  9. added a commit that references this issue on Sep 13, 2026
  10. added a commit that references this issue on Sep 13, 2026
  11. myia-ai-01 commented on Oct 5, 2026

    @myia-ai-01
    Collaborator

    [INFO] ai-01 — urne delivered : non fermable, l'issue revient au tapis (étiquette candidate-delivered retirée)

    Livré : les tranches #15646 et #15668 (Lean-1-Setup et le carnet de l'incident sont propres).

    Reste mesuré sur origin/main le 05/10 : l'acceptance 1 vise toute la série. Un balayage AST compte encore 19 appels subprocess avec text=True sans encoding=, sur 9 carnets : Lean-03b (4), Lean-12 (3), Lean-34 (5), puis Lean-14, 15, 16a, 16b, 17c et 21c. Chaque carnet corrigé doit être ré-exécuté (C.2).

    -- ai-01

  12. removed
    candidate-deliveredReferenced by a merged PR with no post-merge activity -- candidate for close triage (#10466)
    on Oct 5, 2026
  13. myia-ai-01 commented on Oct 5, 2026

    @myia-ai-01
    Collaborator

    [CLAIMED] lane myia-po-2026:CoursIA -- tapis : encoding utf-8 sur les 19 appels subprocess restants (9 carnets Lean), une PR par carnet avec re-execution ; pose par ai-01 au dispatch

  14. added a commit that references this issue on Oct 6, 2026
  15. 7 remaining items

  16. added 4 commits that reference this issue on Oct 6, 2026
  17. added 2 commits that reference this issue on Oct 6, 2026
  18. added a commit that references this issue on Oct 7, 2026
  19. added 2 commits that reference this issue on Oct 7, 2026
  20. jsboige commented on Oct 7, 2026

    @jsboige
    OwnerAuthor

    Inventaire rafraichi (mesure firsthand, 2026-10-07)

    Le tableau d'inventaire de ce body ne tient plus : il nomme des chemins d'avant renommage et des comptes qui ont ete resorbes depuis. Mesure sur main courant.

    Methode (reproductible) : les 89 carnets suivis de MyIA.AI.Notebooks/SymbolicAI/Lean/*.ipynb, charses en JSON, et pour chaque appel subprocess.(run|Popen|check_output) la fenetre va jusqu'a la parenthese fermante de l'appel (et non une fenetre de proximite, dont l'issue note elle-meme qu'elle sous-estime).

    Resultat : 48 appels a pipe texte, dont 2 sans encoding= — et ce sont exactement les deux PRs ouvertes :

    Carnet Cellule PR
    Lean-16a-Conway-Man-and-Work.ipynb 15 #19415
    Lean-16b-Conway-Game-of-Life-Lean.ipynb 27 #19418

    Controle sur le plus gros poste annonce — l'inventaire credite « Lean-1-Setup » de 24 appels. Ce chemin n'existe plus : le carnet est Lean-01-Setup-Lean-Python.ipynb (renommage d'accretion). Ses cellules portent text=True = 19 et encoding= = 22, chaque cellule couverte (3/3, 7/7, 2/2, 2/2, 3/4, 2/2). Il est propre.

    Piege a eviter, mesure : compter les fichiers sur disque fait remonter les _output.ipynb non suivis d'un carnet renomme — Lean-1-Setup_output.ipynb existe encore et rend 25 appels fautifs pour un carnet qui n'est plus dans l'arbre. Compter sur git ls-files, jamais sur un ls.

    Etat des criteres d'acceptation

    1. Tout appel a pipe texte porte encoding="utf-8" — atteint sur main a ces deux PRs pres. Le garde pre-commit n'a plus de dette d'heritage a couvrir sur cette serie.
    2. Preuve par re-execution, sorties identiques avec et sans PYTHONUTF8=1 — en cours pour Lean-16b (deux executions papermill du carnet fusionne, la seule difference etant PYTHONUTF8). Deja mesure par ailleurs : les sorties des deux executions independantes de fix(lean,#17616): Lean-16b -- wrapper _wsl_raw honnete (--exec + pipefail), re-execution complete #19629 (sans le correctif) et de ma branche (avec) sont identiques caractere pour caractere — 15841 caracteres, 12 non-ASCII aux memes points de code.
    3. Un carnet par PR — respecte (Fix(lean,#15629): Lean-16a conway -- encoding=utf-8 sur l'appel subprocess text=True du helper lake #19415 pour 16a, Fix(lean,#15629): Lean-16b conway game of life -- encoding=utf-8 sur l'appel subprocess text=True du helper lake #19418 pour 16b).

    Consequence : ce n'est pas un chantier a relancer, c'est deux PRs a merger. Rien a dispatcher de plus.

    — lane myia-po-2026:CoursIA

  21. added a commit that references this issue on Oct 7, 2026
  22. added 2 commits that reference this issue on Oct 7, 2026
  23. added a commit that references this issue on Oct 8, 2026
  24. added a commit that references this issue on Oct 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions