diff --git a/scripts/gen_all_batches.py b/scripts/gen_all_batches.py index 70965a5..39895d2 100644 --- a/scripts/gen_all_batches.py +++ b/scripts/gen_all_batches.py @@ -1,15 +1,20 @@ 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 +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 = mk_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) + r = gen_batch.build(n0, n1) + 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_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..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 @@ -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..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 @@ -260,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() -io.open(r"c:/Users/teort/Github/sendov/Sendov/Common/Sinh.lean", "w", +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")