From 6b208c610f6829009ed9568c11bb4d308504a342 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 22 Jun 2026 01:48:23 +0000 Subject: [PATCH 1/3] Added multiple lean versions to run parallely. --- src/itp_interface/lean/.gitignore | 1 + src/itp_interface/lean/tactic_parser.py | 32 ++++++++++++++++++------- 2 files changed, 24 insertions(+), 9 deletions(-) create mode 100644 src/itp_interface/lean/.gitignore diff --git a/src/itp_interface/lean/.gitignore b/src/itp_interface/lean/.gitignore new file mode 100644 index 0000000..f49dfc6 --- /dev/null +++ b/src/itp_interface/lean/.gitignore @@ -0,0 +1 @@ +tactic_parser_*/ \ No newline at end of file diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index 2c03f17..e920e58 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -279,22 +279,29 @@ class RequestType(Enum): BREAK_CHCKPNT = "break_chckpnt" PARSE_DEPENDS = "parse_depends" # 13 chars - for dependency analysis -def get_path_to_tactic_parser_project() -> str: +def get_lean_version_from_env() -> Optional[str]: + """Get the Lean version from the environment variable, if set.""" + return os.getenv("LEAN_VERSION", "4.30.0") + +def get_path_to_tactic_parser_project(lean_version: str|None=None) -> str: """Get the path to the tactic parser project directory.""" lean_dir = os.path.dirname(__file__) tactic_parser_path = os.path.join(lean_dir, "tactic_parser") abs_path = os.path.abspath(tactic_parser_path) + if lean_version is not None: + version_dir_str = lean_version.replace('.', '') + abs_path = f"{abs_path}_{version_dir_str}" return abs_path -def get_path_to_tactic_parser_executable() -> str: +def get_path_to_tactic_parser_executable(lean_version: str|None=None) -> str: """Get the path to the tactic parser executable.""" - abs_path = get_path_to_tactic_parser_project() + abs_path = get_path_to_tactic_parser_project(lean_version) tactic_parser_bin_path = os.path.join(abs_path, ".lake", "build", "bin", "tactic-parser") return tactic_parser_bin_path -def toolchain_version_and_env_version(): - lean_version_needed = os.getenv("LEAN_VERSION", "4.30.0") - tactic_parser_project = get_path_to_tactic_parser_project() +def toolchain_version_and_env_version(version_dir: str|None=None) -> tuple[str, str, str]: + lean_version_needed = get_lean_version_from_env() + tactic_parser_project = get_path_to_tactic_parser_project(version_dir) # Check the version of the built parser toolchain_file = os.path.join(tactic_parser_project, "lean-toolchain") assert os.path.isfile(toolchain_file), f"lean-toolchain file not found at {toolchain_file}, something is wrong." @@ -317,8 +324,13 @@ def change_toolchain_version(lean_version_needed: str, toolchain_file: str, tool def is_tactic_parser_built() -> bool: """Check if the tactic parser executable exists.""" - path_to_exec = get_path_to_tactic_parser_executable() toolchain_file, toolchain_content, lean_version_needed = toolchain_version_and_env_version() + version_dir = get_path_to_tactic_parser_project(lean_version_needed) + if not os.path.exists(version_dir): + shutil.copytree(get_path_to_tactic_parser_project(), version_dir) + toolchain_file = os.path.join(version_dir, "lean-toolchain") + path_to_exec = get_path_to_tactic_parser_executable(lean_version_needed) + toolchain_file, toolchain_content, lean_version_needed = toolchain_version_and_env_version(lean_version_needed) if not os.path.isfile(path_to_exec): if lean_version_needed is not None: change_toolchain_version(lean_version_needed, toolchain_file, toolchain_content) @@ -377,7 +389,8 @@ def build_lean4_project(project_folder, logger: Optional[logging.Logger] = None, def build_tactic_parser_if_needed(logger: Optional[logging.Logger] = None): """Build the tactic parser if not already built.""" if not is_tactic_parser_built(): - build_lean4_project(get_path_to_tactic_parser_project(), logger, has_executable=True) + lean_version = get_lean_version_from_env() + build_lean4_project(get_path_to_tactic_parser_project(lean_version), logger, has_executable=True) def _get_process_group_rss_kb(pgid: int) -> int: """Sum RSS (kB) of all processes in a process group by scanning /proc.""" @@ -641,7 +654,8 @@ def _start(self): self.logger.debug(f"Starting parser in standalone mode from: {working_dir}") # Ensure the parser is built build_tactic_parser_if_needed(self.logger) - path_to_tactic_parser_exec = get_path_to_tactic_parser_executable() + lean_version = get_lean_version_from_env() + path_to_tactic_parser_exec = get_path_to_tactic_parser_executable(lean_version) assert os.path.isfile(path_to_tactic_parser_exec), f"Tactic parser executable not found at {path_to_tactic_parser_exec}, please build it first." cmds = ["lake", "env", path_to_tactic_parser_exec] self.process = subprocess.Popen( From fab318a100dbb121d381d9cff57366a9e53b18d0 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 22 Jun 2026 04:55:58 +0000 Subject: [PATCH 2/3] Update default Lean version to 4.30.0 in environment variable handling --- src/itp_interface/lean/tactic_parser.py | 8 +++++--- src/itp_interface/main/install.py | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index e920e58..a9c2162 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -279,7 +279,7 @@ class RequestType(Enum): BREAK_CHCKPNT = "break_chckpnt" PARSE_DEPENDS = "parse_depends" # 13 chars - for dependency analysis -def get_lean_version_from_env() -> Optional[str]: +def get_lean_version_from_env() -> str: """Get the Lean version from the environment variable, if set.""" return os.getenv("LEAN_VERSION", "4.30.0") @@ -415,9 +415,11 @@ def _get_process_group_rss_kb(pgid: int) -> int: return total -def get_path_to_dependency_parser_executable() -> str: +def get_path_to_dependency_parser_executable(lean_version: str|None=None) -> str: """Get the path to the dependency parser executable.""" - abs_path = get_path_to_tactic_parser_project() + if lean_version is None: + lean_version = get_lean_version_from_env() + abs_path = get_path_to_tactic_parser_project(lean_version) dependency_parser_bin_path = os.path.join(abs_path, ".lake", "build", "bin", "dependency-parser") return dependency_parser_bin_path diff --git a/src/itp_interface/main/install.py b/src/itp_interface/main/install.py index 0c38ed0..f45a0cb 100644 --- a/src/itp_interface/main/install.py +++ b/src/itp_interface/main/install.py @@ -40,8 +40,8 @@ def install_itp_interface(): def install_lean_repl(): print("Updating Lean") print("Checking if Lean version is set in environment variables as LEAN_VERSION") - print("If not, defaulting to 4.24.0") - lean_version = os.environ.get("LEAN_VERSION", "4.24.0") + print("If not, defaulting to 4.30.0") + lean_version = os.environ.get("LEAN_VERSION", "4.30.0") # Make sure that .elan is installed print("Checking if .elan is installed") From 3e971d861f4338ecef6bcde268e5d42b5d02b477 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 22 Jun 2026 05:03:22 +0000 Subject: [PATCH 3/3] Bump version to 1.10.0 in pyproject.toml --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index d84a1f9..995f242 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -5,7 +5,7 @@ requires = [ build-backend = "hatchling.build" [project] name = "itp_interface" -version = "1.9.0" +version = "1.10.0" authors = [ { name="Amitayush Thakur", email="amitayush@utexas.edu" }, ]