wsl() wrapper des notebooks Lean : rc masque par le pipe tail (SUCCESS imprime sur un lake echoue)

[jsboige]

Résumé

Le wrapper WSL embarqué dans les notebooks Lean (def wsl(cmd) → _wsl_raw → bash -lc '<cmd> 2>&1 | tail -20') rend comme code de sortie celui de tail, pas celui de lake : une commande lake build ... 2>&1 | tail -20 qui échoue (checkout mathlib refusé, error: external command 'git' exited with code 1, Aborting) revient avec rc=0, et la cellule imprime SUCCESS : les 3 modules Life compilent sur la foi de ce rc masqué.

Instance mesurée : #16987 (review po-2026:CoursIA-3 du 2026-09-23) — à la tête aa28e7e44e, la cellule lake-build-life (idx 46) commettait SUCCESS alors que lake venait d'écrire error: dans la même sortie. Le même socle avait produit des sorties dégradées aux cellules 38 et 42 (rc=-1, 0 verdicts parses sur 7 attendus). La panne avait été masquée par le wrapper, pas détectée.

Mécanisme

# cellule subprocess-setup (Lean-16b) :
full = ['wsl', '-d', 'Ubuntu', '--', 'bash', '-lc', cmd]
r = subprocess.run(full, capture_output=True, text=True, timeout=timeout)
return r.returncode, r.stdout, r.stderr        # rc = rc du PIPELINE bash

# cellule lake-build-life :
rc, out, err = wsl(f'... lake build {targets} 2>&1 | tail -20', timeout=1500)
# en bash, le rc d'un pipeline = rc de la DERNIERE commande (tail) => toujours 0
if rc == 0:
    print('SUCCESS : ...')                      # affirme une compilation qui n'a pas eu lieu

C'est la même classe que le tell c.1418-L2 (rc d'un pipe = rc de tail, pas de l'outil), ici côté notebook plutôt que côté session.

Périmètre (mesuré sur origin/main)

git grep -l "2>&1 | tail" origin/main -- 'MyIA.AI.Notebooks/SymbolicAI/Lean/*.ipynb' :

• Lean-12-Sensitivity-Theorem.ipynb
• Lean-15-Grothendieck-Tribute.ipynb (gate if rc == 0 présente)
• Lean-16a-Conway-Man-and-Work.ipynb (gate if rc == 0 présente)
• Lean-16b-Conway-Game-of-Life-Lean.ipynb (gate if rc == 0 présente — l'instance fondatrice)
• Lean-34-Calculabilite-et-Limites.ipynb
• Lean-3b-Formalized-Formal-Logic.ipynb

Fix proposé

Injecter set -o pipefail; en tête de la commande bash passée au wrapper (le rc du pipeline devient alors celui de la première commande qui échoue), ou faire porter le rc par bash lui-même (bash -lc 'set -o pipefail; <cmd> 2>&1 | tail -20'). Corriger le wrapper dans les 6 notebooks listés + re-exécuter les cellules de build concernées (C.2).

Non-bloquant

Défaut distinct des PRs en cours (signalé « non bloquant, mérite une issue » en review de #16987) : les réparations de #16987 (env lake + re-exec) avancent indépendamment.

Grain: LIGHT/guard — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16987

[jsboige]

[CLAIMED] lane myia-po-2026:CoursIA — 2026-09-25T06:45Z — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/lean_notebook_utils.py + ses tests.

Reassessment avant fix (protocole audit-reassessment : lire la source, pas le titre) — le perimetre « les 6 notebooks » ne resiste pas a la mesure :

Notebook	Forme reelle mesuree sur origin/main	Verdict
3b, 34	lake build ... 2>&1 | tail -8; echo "lake build rc=${PIPESTATUS[0]}"	deja corrects — ils lisent le rc de la premiere commande du pipeline, pas celui de tail. Le git grep -l "2>&1 | tail" de l'issue les compte pour fautifs : faux positifs
16b (_wsl_raw)	bash -lc cmd + subprocess.run(...).returncode	defaut confirme, mais bloque : la PR ouverte #16987 edite ce notebook
16a (def wsl local)	meme forme	defaut confirme, mais bloque : PRs ouvertes #17745 et #17663 edittent ce notebook
12	le remede est deja ecrit en prose dans une cellule : « le tail -10 pipe peut masquer des erreurs upstream ; un re-exec avec set -o pipefail est recommande »	a confirmer cellule par cellule
15	wrapper local (def wsl)	a confirmer

La racine que l'issue n'a pas vue : lean_notebook_utils.run_lake, branche WSL —

cmd = (f"source ~/.elan/env 2>/dev/null; "
       f"cd {project_path} && lake {args} 2>&1 | tail -{tail}")
return _run_capture(["wsl", "-d", "Ubuntu", "--", "bash", "-lc", cmd], timeout)

le returncode rendu est celui du pipeline, donc celui de tail — toujours 0. 9 notebooks consomment run_lake (git grep -l run_lake origin/main -- '*.ipynb') : Search-03e, Lean-13, 15, 16a, 16b, 16d, 16f, 16g, 22.

Perimetre de ma PR : la racine (run_lake + tests unitaires falsifies). Aucune cellule de notebook touchee — donc pas d'obligation C.2, et aucune collision avec les PRs ouvertes (#16987 → 16b, #17745/#17663 → 16a). Les wrappers locaux des notebooks restent un suivi distinct, a prendre une fois les dites PRs fermees.

[jsboige]

CORRECTION de mon claim — retrait : la « racine » est deja livree sur origin/main

lean_notebook_utils.run_lake porte deja set -o pipefail; : introduit par le commit 31a06ba90f (PR #8425, « Sub-grain 13 of c.8081-c.8106 audit series »), dont le message nomme exactement le diagnostic que je croyais inedit — « run_lake (shared by Lean-13/16a/16b/16f) lacked 'set -o pipefail;' -> masks lake build exit code behind tail -N (…) in shared utility = 4x impact ».

Pourquoi mon claim le disait non corrige : la ligne fautive a ete lue dans l'arbre local perime (base 25369a46a1) alors que mes autres mesures lisaient git show origin/main:. L'erreur est mienne, elle est consignee.

Table finale — tout mesure sur origin/main 17b1e10993 :

Site	Etat mesure
run_lake (helper partage, 9 notebooks)	corrige — set -o pipefail; depuis #8425
3b, 34	corrects — lake build ... | tail -N; echo rc=${PIPESTATUS[0]} : le rc lu est celui de lake, pas de tail
12	correct — cell 23 : cd {proj} && source ~/.elan/env && set -o pipefail; lake build 2>&1 | tail -10 (la cellule markdown 25 qui « recommande » le re-exec pipefail est une prose residuelle)
15	defaut confirme — cell 3 : def wsl local = bash -lc cmd, rc du pipeline donc celui de tail ; la build cell pipe lake build ... 2>&1 | tail -20 et lit ce rc. Libre (aucune PR ouverte ne touche ce notebook)
16a	defaut confirme (wrapper local bash -lc cmd) — bloque : #17745 et #17663 editent ce notebook
16b	defaut confirme (_wsl_raw + if rc == 0 imprime SUCCESS) — bloque : #16987 edite ce notebook

Consequence sur le perimetre de l'issue : sur les 6 notebooks listes, 4 sont deja corrects (3b, 34, 12, et le helper partage). Le travail reel restant = 15 (libre) + 16a/16b (apres merge de leurs PRs). Le grep git grep -l "2>&1 | tail" de l'issue detecte le motif du pipeline, pas le defaut de lire son rc.

Pourquoi je ne prends pas 15 maintenant : le fix est une ligne (set -o pipefail; en tete de la commande passee au wrapper), mais il touche une cellule code → C.2 = re-execution complete du notebook. Mesure sur le lac : grothendieck_lean a 169 fichiers changes / +30505 lignes entre la base des oleans chauds locaux et origin/main, dont lean-toolchain et lakefile.lean — la re-exec sur base fraiche reconstruit le lac (Mathlib). Ce n'est pas borne pour ma fenetre ; une lane avec le lac reconstruit (ou une jonction verifiee contre le toolchain) le livre en un cycle.

Je relache le claim : aucune PR ouverte de ma part sur ce grain, rien n'est en vol. Le commentaire de reassessment ci-dessus reste exact pour sa partie table (les mesures ont toujours ete prises sur origin/main) ; seule sa conclusion « perimetre de ma PR : la racine » est caduque.

[jsboigeEpita]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-lean #17993

[CLAIMED] lane myia-po-2025:CoursIA — fix de la tranche libre Lean-15 : wrapper wsl local (cellule 3) masque le rc de lake build derrière | tail -20 ; correctif set -o pipefail; + re-execution complete avec outputs (C.2) — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb

Perimetre strictement la tranche « 15 (libre) » du reassessment du 2026-09-25 : ni 16a/16b (bloques par #16987/#17745/#17663), ni le helper partage lean_notebook_utils.py (deja corrige sur origin/main par #8425).

[jsboigeEpita]

Livree — tranche Lean-15 : PR #18033 (fix/17616-lean15-pipefail), un seul fichier MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb.

• Fix : le wrapper wsl() (cellule lean13-setup) prefixe desormais chaque commande de set -o pipefail; — le rc rendu est celui de la premiere commande qui echoue, pas celui de tail. Couvre tous les appelants (run_lake_build, run_lean).
• Controle negatif mesure (mecanisme exact du wrapper) : pipeline fautif rc=0 (ancien) → rc=127 (corrige).
• Re-execution complete (C.2) : Papermill 2.6.0 kernel python3, 1725s, exception: null, 12/12 cellules code execution_count 1-12, 0 erreur, 0 timeout — exercises servies par oleans mathlib precompilees au rev exact db584cd6d46c (zero compilation Mathlib), un process lean sequentiel a la fois.
• Ratchets post-commit verts vs origin/main : output-failure 0 regressed, output-collapse 0 flagged, source-collapse 0 flagged.
• Gain annexe : la ligne heritee warning: mathlib ... has local changes disparait des outputs (lake propre au rev du manifeste).

Restent sur l'issue : 16a/16b (bloques par #16987/#17745/#17663). Le claim paths: reste actif jusqu'a merge de #18033.

[jsboigeEpita]

Mise a jour de la livraison (PR #18033, head 4c2de0cb77) : la premiere re-execution tournait sous python 3.13 (kernelspec python3 de la machine) — language_info.version 3.11.9 → 3.13.14, Kernel drift guard rouge. Correctif honnete (regle F) : env py311-lean cree (conda create python=3.11 ipykernel) + re-execution complete dessous (Papermill 1524s, exception null, 12/12 cellules ec 1-12). Les 12 sorties code sont byte-identiques entre les passes 3.11 et 3.13 (contenu deterministe — zero drift de repr, confirme par mesure).

Etat CI a la head 4c2de0cb77 : 86 checks verts (kernel drift guard PASS, ratchets PASS, validate PASS). Seul rouge restant = jambe DWELL du PR gate (plancher 120 min, minuteur, levee auto au balayage — pas un defaut de la PR). Un flake infra (checkout filter: blob:none) sur le check cell-ordering a ete rejoue vert.

[jsboige]

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
issue: 17616
verdict: KEEP
acceptance:

• Le périmètre du body — six notebooks fautifs — est réfuté par la mesure -> re-mesure de ce jour sur main : Lean-3b-Formalized-Formal-Logic.ipynb et Lean-34-Calculabilite-et-Limites.ipynb lisent le rc de lake via PIPESTATUS[0], Lean-12-Sensitivity-Theorem.ipynb porte set -o pipefail, et le helper partagé lean_notebook_utils.py porte set -o pipefail; (ligne 250) depuis PR fix(lean-13,#8053): correct 3 byte-surgical findings (sorry count + run_lake pipefail) #8425 — quatre des six sites listés sont déjà corrects
• Tranche Lean-15 — le site libre — livrée -> PR fix(lean,#17616): Lean-15 wsl() wrapper pipefail + re-execution complete #18033 MERGÉE (2026-09-27T16:19:30Z) : le wrapper wsl() local préfixe set -o pipefail;, contrôle négatif mesuré (rc=0 fautif devient rc=127), ré-exécution papermill complète sous le kernel de la base
• Tranche Lean-16b non livrée -> défaut mesuré ce jour sur main : Lean-16b-Conway-Game-of-Life-Lean.ipynb porte def _wsl_raw (ligne 143 du JSON), le pipeline lake build {targets} 2>&1 | tail -20 (ligne 2678) et le gate if rc == 0: (ligne 2686) qui imprime SUCCESS sur un rc de tail
• Tranche Lean-16a non livrée -> défaut mesuré ce jour sur main : Lean-16a-Conway-Man-and-Work.ipynb porte def wsl local (ligne 653), les pipelines | tail -20 (lignes 1205 et 1676) et les gates if rc == 0: (lignes 1213 et 1684)
• Les blocages des deux tranches restantes sont levés -> PR fix(lean,#16983): REPAIR-2 morphologique map REACCENT (1 'donne' fautif) #16987, PR fix(notebooks,#17498): tranche SymbolicAI -- 18 defauts de rendu mathematique corriges (18 -> 0) #17745 et PR fix(lean,#17576): Lean-16a re-execute sur lake chaud — les 5 #eval de la section 3.7 rendent leurs valeurs #17663 toutes MERGÉES le 2026-09-25 ; aucune PR ouverte ne cite l'issue ce jour, les deux notebooks sont donc libres
  residue: followup wsl() wrapper des notebooks Lean : rc masque par le pipe tail (SUCCESS imprime sur un lake echoue) #17616
  open-prs: 0
  comments-reviewed: 5
  [/CLOSURE PREFLIGHT]

[jsboige]

[CLAIMED] lane myia-po-2026:CoursIA-2 -- c.1345 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb