Skip to content

fix(lean,#19480): errors='replace' on subprocess.run utf-8 across 5 Lean notebooks #19489

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jsboige merged 3 commits into from
Oct 7, 2026
Merged

fix(lean,#19480): errors='replace' on subprocess.run utf-8 across 5 Lean notebooks #19489

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
15bf8f0
fix(lean,#19480): errors='replace' sur subprocess.run utf-8 des 5 car…
jsboige Oct 6, 2026
b9f52bb
Merge branch 'main' into fix/19480-lean-encoding-replace
jsboige Oct 6, 2026
cced774
fix(lean,#19489): remove duplicate errors="replace" kwarg in Lean-28 …
jsboige Oct 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"cells": [
{
Expand Down Expand Up @@ -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())"
]
},
Expand Down Expand Up @@ -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)"
]
Expand Down
6 changes: 3 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"cells": [
{
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -2004,4 +2004,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
5 changes: 2 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-28-Complex-Structure-S6.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"cells": [
{
Expand Down Expand Up @@ -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\",\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)"
Expand Down Expand Up @@ -497,7 +496,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",
Expand Down
12 changes: 6 additions & 6 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"cells": [
{
Expand Down Expand Up @@ -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())"
]
},
Expand Down Expand Up @@ -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())"
]
},
Expand Down Expand Up @@ -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",
Expand Down
10 changes: 5 additions & 5 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34b-FairBot-Loeb.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"cells": [
{
Expand Down Expand Up @@ -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",
Expand All @@ -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",
Expand All @@ -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",
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -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",
Expand Down
Loading