trishullab · amit9oct · Jun 8, 2026 · Jan 16, 2026 · May 31, 2026 · Jun 1, 2026
diff --git a/.github/workflows/github-build-actions-python314t.yaml b/.github/workflows/github-build-actions-python314t.yaml
@@ -14,6 +14,7 @@ jobs:
       options: --user 0  # Running as root; no sudo needed
     env:
       HOME: /root
+      ITP_DEP_PARSER_MEM_LIMIT: "0.9"
 
     steps:
       - name: Checkout repository

diff --git a/.github/workflows/github-build-actions.yaml b/.github/workflows/github-build-actions.yaml
@@ -14,6 +14,7 @@ jobs:
       options: --user 0  # Running as root; no sudo needed
     env:
       HOME: /root
+      ITP_DEP_PARSER_MEM_LIMIT: "0.9"
 
     steps:
       - name: Checkout repository

diff --git a/.gitmodules b/.gitmodules
@@ -16,3 +16,21 @@
 [submodule "src/data/test/batteries"]
 	path = src/data/test/batteries
 	url = https://github.com/leanprover-community/batteries.git
+	ignore = dirty
+[submodule "src/data/test/Strata"]
+	path = src/data/test/Strata
+	url = https://github.com/strata-org/Strata.git
+	ignore = dirty
+[submodule "src/data/test/cslib"]
+	path = src/data/test/cslib
+	url = https://github.com/leanprover/cslib.git
+	ignore = dirty
+[submodule "src/data/test/miniF2F-lean4"]
+	path = src/data/test/miniF2F-lean4
+	url = https://github.com/yangky11/miniF2F-lean4
+[submodule "src/data/test/PutnamBench"]
+	path = src/data/test/PutnamBench
+	url = https://github.com/trishullab/PutnamBench.git
+[submodule "src/data/test/clever"]
+	path = src/data/test/clever
+	url = https://github.com/trishullab/clever.git
diff --git a/README.md b/README.md
@@ -17,7 +17,7 @@ Generic interface for hooking up to any Interactive Theorem Prover (ITP) and col
 pip install itp-interface
 ```
 
-2. Run the following command to prepare the REPL for Lean 4. The default version is 4.24.0. You can change the version by setting the `LEAN_VERSION` environment variable. If no version is set, then 4.24.0 is used.
+2. Run the following command to prepare the REPL for Lean 4. The default version is 4.30.0. You can change the version by setting the `LEAN_VERSION` environment variable. If no version is set, then 4.30.0 is used.
 >NOTE: The Lean 4 version must match the version of the Lean 4 project you are working with. `itp-interface` **supports Lean 4 versions v4.15.0 through v4.30.0**. (It has been tested till version 4.30.0, but might as well work for future versions too, if the future versions are completely backwards-compatible).
 
 ```bash
@@ -30,11 +30,21 @@ install-lean-repl
 ```bash
 install-itp-interface
 ```
->NOTE: `install-itp-interface` also respects the `LEAN_VERSION` environment variable to determine which Lean version to compile the tactic parser with. It defaults to `4.24.0` when not set. **Both `install-lean-repl` and `install-itp-interface` must use the same `LEAN_VERSION`** — mismatching versions will cause elaboration errors at runtime. If you set `LEAN_VERSION` for one, set it for both:
+>NOTE: `install-itp-interface` also respects the `LEAN_VERSION` environment variable to determine which Lean version to compile the tactic parser with. It defaults to `4.30.0` when not set. **Both `install-lean-repl` and `install-itp-interface` must use the same `LEAN_VERSION`** — mismatching versions will cause elaboration errors at runtime. If you set `LEAN_VERSION` for one, set it for both:
 ```bash
 export LEAN_VERSION="4.30.0" && install-lean-repl && install-itp-interface
 ```
 
+### Memory limit for the dependency parser
+
+When `itp-interface` analyzes a Lean file (e.g. one that `import Mathlib`), it launches a `dependency-parser` subprocess that loads the full Lean environment and can use several GB of RAM. A soft memory monitor kills the process if it exceeds **30 % of total system RAM** by default, to avoid OOM-killing the host.
+
+On machines with ample memory (large CI runners, workstations) this default can be too conservative. Override it with:
+```bash
+export ITP_DEP_PARSER_MEM_LIMIT=0.9   # allow up to 90 % of total RAM
+```
+The value is a float in (0, 1]. It is read at runtime — no rebuild needed.
+
 >NOTE: These steps are only tested on Linux. For Windows, you can use WSL. These steps will not setup the Coq interface.
 
 # Full Setup for Coq and Lean:

diff --git a/pyproject.toml b/pyproject.toml
@@ -5,7 +5,7 @@ requires = [
 build-backend = "hatchling.build"
 [project]
 name = "itp_interface"
-version = "1.6.0"
+version = "1.7.0"
 authors = [
   { name="Amitayush Thakur", email="amitayush@utexas.edu" },
 ]

diff --git a/requirements.txt b/requirements.txt
diff --git a/src/data/test/Mathlib/lake-manifest.json b/src/data/test/Mathlib/lake-manifest.json
@@ -1,21 +1,21 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
+   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
+   "inputRev": "v4.30.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,37 +45,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.99",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
+   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«repl-mathlib-tests»",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/src/data/test/Mathlib/lakefile.lean b/src/data/test/Mathlib/lakefile.lean
@@ -3,9 +3,8 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.24.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where
-  globs := #[.submodules `test]
   -- add library configuration options here
diff --git a/src/data/test/Mathlib/lean-toolchain b/src/data/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.30.0
diff --git a/src/data/test/PutnamBench b/src/data/test/PutnamBench
diff --git a/src/data/test/Strata b/src/data/test/Strata
diff --git a/src/data/test/batteries b/src/data/test/batteries
diff --git a/src/data/test/clever b/src/data/test/clever
diff --git a/src/data/test/cslib b/src/data/test/cslib
diff --git a/src/data/test/lean4_proj/lake-manifest.json b/src/data/test/lean4_proj/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a0187b2361a9c9b82580bb0d68c25e16f9e96a9e",
+   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,37 +45,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.99",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
+   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "lean4_proj",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/src/data/test/lean4_proj/lean-toolchain b/src/data/test/lean4_proj/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.30.0
diff --git a/src/data/test/miniF2F-lean4 b/src/data/test/miniF2F-lean4
diff --git a/src/itp_interface/lean/simple_lean4_sync_executor.py b/src/itp_interface/lean/simple_lean4_sync_executor.py
@@ -622,18 +622,19 @@ def _skip_to_theorem(self, theorem: str):
                 file_path = self.associated_file()
                 assert file_path is not None, "File path should not be None"
                 if os.path.exists(extraction_path):
-                    temp_extraction_path_file = open(extraction_path, "r", encoding="utf-8")
-                    file_dep_analysis_str = temp_extraction_path_file.read()
+                    with open(extraction_path, "r", encoding="utf-8") as temp_extraction_path_file:
+                        file_dep_analysis_str = temp_extraction_path_file.read()
                     file_dep_analysis = [FileDependencyAnalysis.load_from_string(file_dep_analysis_str)]
                 else:
                     file_dep_analysis = self.extract_all_theorems_and_definitions(
                         json_output_path=extraction_path, file_path=file_path)
                     assert file_dep_analysis is not None, "File dependency analysis should not be None"
                     assert len(file_dep_analysis) > 0, "File dependency analysis should not be empty"
-
-                    temp_extraction_path_file = open(extraction_path, "w", encoding="utf-8")
-                    with temp_extraction_path_file:
-                        temp_extraction_path_file.write(file_dep_analysis[0].to_json())
+                    # Only cache non-empty results; an OOM-killed parser returns empty declarations
+                    # and caching that would poison every subsequent call for this file.
+                    if file_dep_analysis[0].declarations:
+                        with open(extraction_path, "w", encoding="utf-8") as temp_extraction_path_file:
+                            temp_extraction_path_file.write(file_dep_analysis[0].to_json())
                 with open(file_path, "r", encoding="utf-8") as f:
                     lines = f.readlines()
             else: