From e6b8f6af9b7fcd6d9ca865294e70f657557e95a7 Mon Sep 17 00:00:00 2001 From: Taksh Date: Wed, 2 Sep 2026 18:08:53 +0530 Subject: [PATCH] Write emit_batch Lean output under Sendov/FiniteRange Degree{n0}_{n1}.lean was written to cwd, so generating from the repo root dropped files outside the package. Resolve the path from __file__ into Sendov/FiniteRange. --- scripts/emit_batch.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/scripts/emit_batch.py b/scripts/emit_batch.py index eff2114..fd5672a 100644 --- a/scripts/emit_batch.py +++ b/scripts/emit_batch.py @@ -1,4 +1,5 @@ import sys, io, pickle, sympy as sp +from pathlib import Path sys.set_int_max_str_digits(50000000) r = pickle.load(open(sys.argv[1],"rb")) n0,n1,k,M0,M1 = r['n0'],r['n1'],r['k'],r['M0'],r['M1'] @@ -170,6 +171,7 @@ def Nmomc : List ℤ := end Sendov ''' -out = f"Degree{n0}_{n1}.lean" -io.open(out,"w",encoding="utf-8",newline="\n").write(src) +out = Path(__file__).resolve().parents[1] / "Sendov" / "FiniteRange" / f"Degree{n0}_{n1}.lean" +out.parent.mkdir(parents=True, exist_ok=True) +out.write_text(src, encoding="utf-8", newline="\n") print("written", out, len(src), "bytes")