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" }, ] 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..a9c2162 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() -> 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.""" @@ -402,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 @@ -641,7 +656,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( 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")