From 6297305aa53849350cf1d5d0ee0802021124338c Mon Sep 17 00:00:00 2001 From: Taksh Date: Sun, 30 Aug 2026 09:17:28 +0530 Subject: [PATCH 1/3] fix: import gen_batch and write under the repo tree gen_all_batches imported a nonexistent mk_batch module and hardcoded a machine-local Windows path, so the regenerator could not run. --- scripts/gen_all_batches.py | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/scripts/gen_all_batches.py b/scripts/gen_all_batches.py index 70965a5..bc64f10 100644 --- a/scripts/gen_all_batches.py +++ b/scripts/gen_all_batches.py @@ -1,13 +1,16 @@ import sys, subprocess, pickle, io, os +from pathlib import Path + PLAN = [(6,6),(8,9),(10,11),(12,13),(14,15),(16,18),(18,20),(20,22),(22,24),(24,26), (26,27),(28,29),(30,31),(32,33),(34,35),(36,37),(38,39),(40,41),(42,43),(44,45), (46,47),(48,49),(50,51),(52,53),(54,55),(56,58),(58,60),(60,63),(64,69),(70,79),(80,100)] -REPO = r"c:/Users/teort/Github/sendov/Sendov/FiniteRange" -import mk_batch +REPO = Path(__file__).resolve().parents[1] / "Sendov" / "FiniteRange" +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import gen_batch ok, fail = [], [] for (n0, n1) in PLAN: try: - r = mk_batch.build(n0, n1) + r = gen_batch.build(n0, n1) pickle.dump(r, open(f"batch_{n0}_{n1}.pkl", "wb")) subprocess.run([sys.executable, "emit_batch.py", f"batch_{n0}_{n1}.pkl"], check=True) src = f"Degree{n0}_{n1}.lean" From 7406052d158496f4edd8b83916961e8e8c54e0c8 Mon Sep 17 00:00:00 2001 From: Taksh Date: Mon, 31 Aug 2026 15:12:49 +0530 Subject: [PATCH 2/3] fix: write cover/endgame/sinh Lean under the repo tree Same hardcoded Windows path bug as gen_all_batches: generate into Sendov/... relative to the script instead of c:/Users/teort/... --- scripts/gen_cover.py | 3 ++- scripts/gen_endgame.py | 3 ++- scripts/gen_sinh.py | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/scripts/gen_cover.py b/scripts/gen_cover.py index 621e981..7c59092 100644 --- a/scripts/gen_cover.py +++ b/scripts/gen_cover.py @@ -1,4 +1,5 @@ import io +from pathlib import Path PLAN = [(6,6),(8,9),(10,11),(12,13),(14,15),(16,18),(18,20),(20,22),(22,24),(24,26), (26,27),(28,29),(30,31),(32,33),(34,35),(36,37),(38,39),(40,41),(42,43),(44,45), (46,47),(48,49),(50,51),(52,53),(54,55),(56,58),(58,60),(60,63),(64,69),(70,79), @@ -91,6 +92,6 @@ end Sendov ''' src = head + imports + doc + "\n".join(L) + tail -io.open(r"c:/Users/teort/Github/sendov/Sendov/FiniteRange/Cover.lean", "w", +io.open(Path(__file__).resolve().parents[1] / "Sendov" / "FiniteRange" / "Cover.lean", "w", encoding="utf-8", newline="\n").write(src) print(f"{len(runs)} branches covering degrees 5..100") diff --git a/scripts/gen_endgame.py b/scripts/gen_endgame.py index 45dd34c..3534e58 100644 --- a/scripts/gen_endgame.py +++ b/scripts/gen_endgame.py @@ -100,6 +100,7 @@ def poly(cs, var="α"): Authors: Terence Tao -/ import Sendov.LargeDegree.Monotone +from pathlib import Path /-! # The large-degree claim @@ -238,6 +239,6 @@ def poly(cs, var="α"): end Sendov ''' -io.open(r"c:/Users/teort/Github/sendov/Sendov/LargeDegree/Endgame.lean", "w", +io.open(Path(__file__).resolve().parents[1] / "Sendov" / "LargeDegree" / "Endgame.lean", "w", encoding="utf-8", newline="\n").write(src) print(f"written Endgame.lean, {len(src)} bytes") diff --git a/scripts/gen_sinh.py b/scripts/gen_sinh.py index 5557467..0ebd2e1 100644 --- a/scripts/gen_sinh.py +++ b/scripts/gen_sinh.py @@ -83,6 +83,7 @@ def poly_str(cs, var="y"): import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp import Mathlib.Analysis.Calculus.MeanValue +from pathlib import Path /-! # `log (sinh h / h) ≤ √(h² + 9) - 3` @@ -262,6 +263,6 @@ def poly_str(cs, var="y"): # f-string would swallow, so it is kept beside this script rather than inlined. src = src.replace("\nend Sendov\n", "\n") + io.open( "sinh_tail.lean.txt", encoding="utf-8").read() -io.open(r"c:/Users/teort/Github/sendov/Sendov/Common/Sinh.lean", "w", +io.open(Path(__file__).resolve().parents[1] / "Sendov" / "Common" / "Sinh.lean", "w", encoding="utf-8", newline="\n").write(src) print(f"written Sinh.lean, {len(src)} bytes") From 279d288a6ac1fa76d734f37b20e265e2aa9d6178 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 2 Sep 2026 18:10:48 +0530 Subject: [PATCH 3/3] Keep pathlib imports in Python, not in generated Lean PR tip put `from pathlib import Path` inside Lean templates for Endgame and Sinh, and still ran emit_batch cwd-relative. Move Path to the Python module scope, resolve sinh_tail beside the script, and invoke emit_batch via SCRIPTS paths. --- scripts/gen_all_batches.py | 8 +++++--- scripts/gen_endgame.py | 2 +- scripts/gen_sinh.py | 5 ++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/scripts/gen_all_batches.py b/scripts/gen_all_batches.py index bc64f10..39895d2 100644 --- a/scripts/gen_all_batches.py +++ b/scripts/gen_all_batches.py @@ -4,15 +4,17 @@ PLAN = [(6,6),(8,9),(10,11),(12,13),(14,15),(16,18),(18,20),(20,22),(22,24),(24,26), (26,27),(28,29),(30,31),(32,33),(34,35),(36,37),(38,39),(40,41),(42,43),(44,45), (46,47),(48,49),(50,51),(52,53),(54,55),(56,58),(58,60),(60,63),(64,69),(70,79),(80,100)] -REPO = Path(__file__).resolve().parents[1] / "Sendov" / "FiniteRange" +SCRIPTS = Path(__file__).resolve().parent +REPO = SCRIPTS.parents[0] / "Sendov" / "FiniteRange" sys.path.insert(0, str(Path(__file__).resolve().parent)) import gen_batch ok, fail = [], [] for (n0, n1) in PLAN: try: r = gen_batch.build(n0, n1) - pickle.dump(r, open(f"batch_{n0}_{n1}.pkl", "wb")) - subprocess.run([sys.executable, "emit_batch.py", f"batch_{n0}_{n1}.pkl"], check=True) + pkl = SCRIPTS / f"batch_{n0}_{n1}.pkl" + pickle.dump(r, open(pkl, "wb")) + subprocess.run([sys.executable, str(SCRIPTS / "emit_batch.py"), str(pkl)], cwd=str(SCRIPTS), check=True) src = f"Degree{n0}_{n1}.lean" io.open(os.path.join(REPO, src), "w", encoding="utf-8", newline="\n").write( io.open(src, encoding="utf-8").read()) diff --git a/scripts/gen_endgame.py b/scripts/gen_endgame.py index 3534e58..d17f625 100644 --- a/scripts/gen_endgame.py +++ b/scripts/gen_endgame.py @@ -1,4 +1,5 @@ import sympy as sp, io +from pathlib import Path a = sp.symbols('a') g = 300 + 47*a - a**2 @@ -100,7 +101,6 @@ def poly(cs, var="α"): Authors: Terence Tao -/ import Sendov.LargeDegree.Monotone -from pathlib import Path /-! # The large-degree claim diff --git a/scripts/gen_sinh.py b/scripts/gen_sinh.py index 0ebd2e1..fddb9bc 100644 --- a/scripts/gen_sinh.py +++ b/scripts/gen_sinh.py @@ -1,4 +1,5 @@ import sympy as sp, io +from pathlib import Path y = sp.symbols('y', real=True) U = y**3 - 10*y**2 + 36*y - 36 @@ -83,7 +84,6 @@ def poly_str(cs, var="y"): import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp import Mathlib.Analysis.Calculus.MeanValue -from pathlib import Path /-! # `log (sinh h / h) ≤ √(h² + 9) - 3` @@ -261,8 +261,7 @@ def poly_str(cs, var="y"): ''' # The analytic tail carries no generated data, and contains brace characters that an # f-string would swallow, so it is kept beside this script rather than inlined. -src = src.replace("\nend Sendov\n", "\n") + io.open( - "sinh_tail.lean.txt", encoding="utf-8").read() +src = src.replace("\nend Sendov\n", "\n") + io.open(Path(__file__).resolve().with_name("sinh_tail.lean.txt"), encoding="utf-8").read() io.open(Path(__file__).resolve().parents[1] / "Sendov" / "Common" / "Sinh.lean", "w", encoding="utf-8", newline="\n").write(src) print(f"written Sinh.lean, {len(src)} bytes")