From 15bf8f084a22fa860970c8126d1ea0191c92f730 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 6 Oct 2026 14:50:40 +0200 Subject: [PATCH 1/2] fix(lean,#19480): errors='replace' sur subprocess.run utf-8 des 5 carnets Lean porteurs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- ...ean-03b-Formalized-Formal-Logic-Lean-Python.ipynb | 10 +++++----- .../Lean/Lean-21-MIMO-Detection-Flips.ipynb | 6 +++--- .../Lean/Lean-28-Complex-Structure-S6.ipynb | 4 ++-- .../Lean/Lean-34-Calculabilite-et-Limites.ipynb | 12 ++++++------ .../SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb | 10 +++++----- 5 files changed, 21 insertions(+), 21 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb index 3108d29c96..82d104a0ac 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb @@ -507,13 +507,13 @@ "# n'importe quel checkout (worktree ou clone post-merge).\n", "LAKE_DIR = subprocess.run(\n", " [\"wsl\", \"-e\", \"wslpath\", \"-a\", os.getcwd()],\n", - " capture_output=True, text=True, encoding=\"utf-8\").stdout.strip() + \"/formal_logic_lean\"\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\").stdout.strip() + \"/formal_logic_lean\"\n", "\n", "r = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && lake build FormalLogic.Bridge 2>&1 | tail -8; \"\n", " \"echo \\\"lake build rc=${PIPESTATUS[0]}\\\"\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=1800)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=1800)\n", "print(r.stdout.strip() or r.stderr.strip())" ] }, @@ -585,17 +585,17 @@ " \"#print axioms FormalLogic.Bridge.peirce_provable\\n\"\n", ")\n", "with tempfile.NamedTemporaryFile(\"w\", suffix=\".lean\", delete=False,\n", - " encoding=\"utf-8\", newline=\"\\n\") as f:\n", + " encoding=\"utf-8\", errors=\"replace\", newline=\"\\n\") as f:\n", " f.write(verify_src)\n", " verify_win = f.name\n", "wsl_path = subprocess.run(\n", " [\"wsl\", \"-e\", \"wslpath\", \"-a\", verify_win.replace(chr(92), \"/\")],\n", - " capture_output=True, text=True, encoding=\"utf-8\").stdout.strip()\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\").stdout.strip()\n", "\n", "r = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && lake env lean {wsl_path} 2>&1 | tail -10\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=900)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=900)\n", "print(r.stdout.strip() or r.stderr.strip())\n", "pathlib.Path(verify_win).unlink(missing_ok=True)" ] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb index 8275f98738..24798d1548 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb @@ -459,10 +459,10 @@ "\n", "def run_lean_snippet(snippet, tag):\n", " tmp = Path(tempfile.gettempdir()) / f\"lean21_{tag}.lean\"\n", - " tmp.write_text(snippet, encoding=\"utf-8\")\n", + " tmp.write_text(snippet, encoding=\"utf-8\", errors=\"replace\")\n", " res = subprocess.run([\"lake\", \"env\", \"lean\", str(tmp)],\n", " cwd=str(LAKE_DIR), capture_output=True, text=True,\n", - " encoding=\"utf-8\", timeout=600)\n", + " encoding=\"utf-8\", errors=\"replace\", timeout=600)\n", " print(res.stdout)\n", " print(res.stderr)\n", " tmp.unlink(missing_ok=True)\n", @@ -2004,4 +2004,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb index 6d52b7775a..a3f33a18a6 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb @@ -101,7 +101,7 @@ "\n", "def wsl(cmd):\n", " return subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\", cmd],\n", - " capture_output=True, text=True, encoding=\"utf-8\",\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\",\n", " errors=\"replace\", timeout=120).stdout.strip()\n", "\n", "statement = wsl(\"sed -n '/abbrev unitSphere/,/end Mathoverflow1973/p' ~/HopfProblem/Challenge.lean\")\n", @@ -497,7 +497,7 @@ "if not script.exists(): # execution depuis le notebook : chemin relatif au depot\n", " script = pathlib.Path(\"../../../scripts/notebook_tools/hopf_s6_reproduction.py\").resolve()\n", "proc = subprocess.run([sys.executable, str(script), \"check\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=240)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=240)\n", "rep = json.loads(proc.stdout)\n", "\n", "print(f\"SHA checkout : {rep['pinned_sha']}\")\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb index a8639d45b2..0b0364a394 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb @@ -102,12 +102,12 @@ "# n'importe quel checkout (worktree ou clone post-merge).\n", "LAKE_DIR = subprocess.run(\n", " [\"wsl\", \"-e\", \"wslpath\", \"-a\", os.getcwd()],\n", - " capture_output=True, text=True, encoding=\"utf-8\").stdout.strip() + \"/formal_logic_lean\"\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\").stdout.strip() + \"/formal_logic_lean\"\n", "\n", "r = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && cat lean-toolchain && lake --version | head -1\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=120)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=120)\n", "print(r.stdout.strip() or r.stderr.strip())" ] }, @@ -315,7 +315,7 @@ " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && lake build {' '.join(cibles)} 2>&1 | tail -10; \"\n", " \"echo \\\"lake build rc=${PIPESTATUS[0]}\\\"\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=1800)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=1800)\n", "print(r.stdout.strip() or r.stderr.strip())" ] }, @@ -386,16 +386,16 @@ "def audit_lean(src, timeout=900, tail=14):\n", " \"\"\"Ecrit src dans un .lean temporaire, le soumet au noyau via lake env lean.\"\"\"\n", " with tempfile.NamedTemporaryFile(\"w\", suffix=\".lean\", delete=False,\n", - " encoding=\"utf-8\", newline=\"\\n\") as f:\n", + " encoding=\"utf-8\", errors=\"replace\", newline=\"\\n\") as f:\n", " f.write(src)\n", " chemin = f.name\n", " wsl_path = subprocess.run(\n", " [\"wsl\", \"-e\", \"wslpath\", \"-a\", chemin.replace(chr(92), \"/\")],\n", - " capture_output=True, text=True, encoding=\"utf-8\").stdout.strip()\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\").stdout.strip()\n", " r = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && lake env lean {wsl_path} 2>&1 | tail -{tail}\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=timeout)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=timeout)\n", " pathlib.Path(chemin).unlink(missing_ok=True)\n", " print(r.stdout.strip() or r.stderr.strip())\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb index 0544604704..b569f77a0f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb @@ -151,7 +151,7 @@ "def wslpath(p):\n", " # Chemin Windows -> chemin WSL, calcule par WSL lui-meme.\n", " r = subprocess.run([\"wsl\", \"-e\", \"wslpath\", \"-a\", str(p).replace(chr(92), \"/\")],\n", - " capture_output=True, text=True, encoding=\"utf-8\")\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\")\n", " return r.stdout.strip()\n", "\n", "\n", @@ -165,7 +165,7 @@ " r = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cd {LAKE_DIR} && python3 {LEAN_EXEC} run --timeout {timeout} -- {commande}\"],\n", - " capture_output=True, text=True, encoding=\"utf-8\", timeout=timeout + 120)\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=timeout + 120)\n", " journal = [l for l in r.stderr.splitlines() if l.startswith(\"[lean_exec]\")]\n", " return r.returncode, r.stdout, journal\n", "\n", @@ -177,7 +177,7 @@ " else \"formal_logic_lean du depot\")\n", "cote_wsl = subprocess.run(\n", " [\"wsl\", \"-e\", \"bash\", \"-lc\", f\"cd {LAKE_DIR} && sha256sum \" + \" \".join(FICHIERS_BUILD)],\n", - " capture_output=True, text=True, encoding=\"utf-8\").stdout.split(\"\\n\")\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\").stdout.split(\"\\n\")\n", "empreintes_wsl = {l.split()[1]: l.split()[0] for l in cote_wsl if l.strip()}\n", "identiques = 0\n", "for nom in FICHIERS_BUILD:\n", @@ -649,7 +649,7 @@ "source": [ "import re\n", "\n", - "SOURCE_LEAN = (REPO_LAKE / \"FormalLogic\" / \"FairBotLoeb.lean\").read_text(encoding=\"utf-8\")\n", + "SOURCE_LEAN = (REPO_LAKE / \"FormalLogic\" / \"FairBotLoeb.lean\").read_text(encoding=\"utf-8\", errors=\"replace\")\n", "\n", "\n", "def declaration(nom):\n", @@ -746,7 +746,7 @@ " [\"wsl\", \"-e\", \"bash\", \"-lc\",\n", " f\"cat > {AUDIT_WSL} && cd {LAKE_DIR} && \"\n", " f\"python3 {LEAN_EXEC} run --timeout {timeout} -- lake env lean {AUDIT_WSL}\"],\n", - " input=ENTETE + corps, capture_output=True, text=True, encoding=\"utf-8\",\n", + " input=ENTETE + corps, capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\",\n", " timeout=timeout + 120)\n", " journal = [l for l in r.stderr.splitlines() if l.startswith(\"[lean_exec]\")]\n", " return r.returncode, r.stdout.replace(AUDIT_WSL, \"audit.lean\"), journal\n", From cced7743393c6dd0e8f9eac69b4a763d644b5310 Mon Sep 17 00:00:00 2001 From: jsboige Date: Tue, 6 Oct 2026 16:43:18 +0200 Subject: [PATCH 2/2] fix(lean,#19489): remove duplicate errors="replace" kwarg in Lean-28 cell 3 Per clusterManager-Myia review (2026-10-06T13:28:55Z, head 15bf8f08): duplicate keyword argument breaks compile() of cell 3 (SyntaxError: keyword argument repeated: errors). Other 4 notebooks pass compile-check. Cell 3 now compiles cleanly; 4 other cells with errors="replace" in the same notebook were already correct (single kwarg, post-fix). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb index a3f33a18a6..a8db7af1ea 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb @@ -101,8 +101,7 @@ "\n", "def wsl(cmd):\n", " return subprocess.run([\"wsl\", \"-e\", \"bash\", \"-lc\", cmd],\n", - " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\",\n", - " errors=\"replace\", timeout=120).stdout.strip()\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\", timeout=120).stdout.strip()\n", "\n", "statement = wsl(\"sed -n '/abbrev unitSphere/,/end Mathoverflow1973/p' ~/HopfProblem/Challenge.lean\")\n", "print(statement)"