From 87a42082ef25bee8d6fb855ddbb88998590bd2a5 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Fri, 16 Jan 2026 04:37:22 +0000 Subject: [PATCH 01/16] Add configuration files for batteries benchmark data extraction --- .../configs/batteries_lean_data_extract.yaml | 13 +++++++++ .../batteries_benchmark_lean_ext.yaml | 27 +++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 src/itp_interface/main/configs/batteries_lean_data_extract.yaml create mode 100644 src/itp_interface/main/configs/benchmark/batteries_benchmark_lean_ext.yaml diff --git a/src/itp_interface/main/configs/batteries_lean_data_extract.yaml b/src/itp_interface/main/configs/batteries_lean_data_extract.yaml new file mode 100644 index 0000000..95a77bf --- /dev/null +++ b/src/itp_interface/main/configs/batteries_lean_data_extract.yaml @@ -0,0 +1,13 @@ +defaults: + # - benchmark: simple_benchmark_lean_training_data + # - run_settings: default_lean_data_generation_transforms + # - benchmark: simple_benchmark_1 + # - run_settings: default_lean4_data_generation_transforms + - benchmark: batteries_benchmark_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/batteries_benchmark_lean_ext + pool_size: 12 \ No newline at end of file diff --git a/src/itp_interface/main/configs/benchmark/batteries_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/batteries_benchmark_lean_ext.yaml new file mode 100644 index 0000000..12eff4d --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/batteries_benchmark_lean_ext.yaml @@ -0,0 +1,27 @@ +name: batteries_benchmark_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/batteries + files: [] + exclude_files: + - src/data/test/batteries/.lake + - src/data/test/batteries/.vscode + - src/data/test/batteries/BatteriesTest + - src/data/test/batteries/scripts + - src/data/test/batteries/docs + - src/data/test/batteries/Shake + - src/data/test/batteries/Batteries.lean + - src/data/test/batteries/bors.toml + - src/data/test/batteries/lake-manifest.toml + - src/data/test/batteries/.github + - src/data/test/batteries/.docker + - src/data/test/batteries/lakefile.toml + - src/data/test/batteries/.gitpod.yml + - src/data/test/batteries/.github + - src/data/test/batteries/lake-manifest.json \ No newline at end of file From 9efc9d3138732896a899add85a0a41bd96209e6c Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 31 May 2026 17:55:55 +0000 Subject: [PATCH 02/16] Add Strata dataset configuration and submodule integration --- .gitmodules | 3 +++ src/data/test/Strata | 1 + .../main/configs/lean_data_extract.yaml | 13 +++++++++++++ .../main/configs/strata_lean_data_extract.yaml | 13 +++++++++++++ 4 files changed, 30 insertions(+) create mode 160000 src/data/test/Strata create mode 100644 src/itp_interface/main/configs/lean_data_extract.yaml create mode 100644 src/itp_interface/main/configs/strata_lean_data_extract.yaml diff --git a/.gitmodules b/.gitmodules index 1b68b33..b7322a4 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,3 +16,6 @@ [submodule "src/data/test/batteries"] path = src/data/test/batteries url = https://github.com/leanprover-community/batteries.git +[submodule "src/data/test/Strata"] + path = src/data/test/Strata + url = https://github.com/strata-org/Strata.git diff --git a/src/data/test/Strata b/src/data/test/Strata new file mode 160000 index 0000000..dd9d2aa --- /dev/null +++ b/src/data/test/Strata @@ -0,0 +1 @@ +Subproject commit dd9d2aacf9b49c6b9460951d8577c7a66d74e6c0 diff --git a/src/itp_interface/main/configs/lean_data_extract.yaml b/src/itp_interface/main/configs/lean_data_extract.yaml new file mode 100644 index 0000000..79fdb4d --- /dev/null +++ b/src/itp_interface/main/configs/lean_data_extract.yaml @@ -0,0 +1,13 @@ +defaults: + # - benchmark: simple_benchmark_lean_training_data + # - run_settings: default_lean_data_generation_transforms + # - benchmark: simple_benchmark_1 + # - run_settings: default_lean4_data_generation_transforms + - benchmark: putnambench_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/putnambench_lean_ext + pool_size: 12 \ No newline at end of file diff --git a/src/itp_interface/main/configs/strata_lean_data_extract.yaml b/src/itp_interface/main/configs/strata_lean_data_extract.yaml new file mode 100644 index 0000000..b86dd12 --- /dev/null +++ b/src/itp_interface/main/configs/strata_lean_data_extract.yaml @@ -0,0 +1,13 @@ +defaults: + # - benchmark: simple_benchmark_lean_training_data + # - run_settings: default_lean_data_generation_transforms + # - benchmark: simple_benchmark_1 + # - run_settings: default_lean4_data_generation_transforms + - benchmark: strata_benchmark_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/strata_benchmark_lean_ext + pool_size: 12 \ No newline at end of file From 272d1095ea5e61f969fe45d3b43fece28278656d Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:30:15 +0000 Subject: [PATCH 03/16] Add cslib submodule for testing data --- .gitmodules | 3 +++ src/data/test/cslib | 1 + 2 files changed, 4 insertions(+) create mode 160000 src/data/test/cslib diff --git a/.gitmodules b/.gitmodules index b7322a4..5a180c0 100644 --- a/.gitmodules +++ b/.gitmodules @@ -19,3 +19,6 @@ [submodule "src/data/test/Strata"] path = src/data/test/Strata url = https://github.com/strata-org/Strata.git +[submodule "src/data/test/cslib"] + path = src/data/test/cslib + url = https://github.com/leanprover/cslib.git diff --git a/src/data/test/cslib b/src/data/test/cslib new file mode 160000 index 0000000..2f677bf --- /dev/null +++ b/src/data/test/cslib @@ -0,0 +1 @@ +Subproject commit 2f677bfc8ef76fa7a27feafc597c1e4a7eda3e42 From 99ab900da03719cbfb45f2b3bfc1c2602d0866c1 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:30:51 +0000 Subject: [PATCH 04/16] Update cslib submodule to latest commit --- src/data/test/cslib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/test/cslib b/src/data/test/cslib index 2f677bf..c7944a9 160000 --- a/src/data/test/cslib +++ b/src/data/test/cslib @@ -1 +1 @@ -Subproject commit 2f677bfc8ef76fa7a27feafc597c1e4a7eda3e42 +Subproject commit c7944a9fb44c3298f1a960a5e574ab23a6ab8ed5 From d154b375d8bd9eae15cc659afec95a83c2e7d9ec Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:32:18 +0000 Subject: [PATCH 05/16] Update Strata submodule to latest commit --- src/data/test/Strata | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/test/Strata b/src/data/test/Strata index dd9d2aa..d76b54e 160000 --- a/src/data/test/Strata +++ b/src/data/test/Strata @@ -1 +1 @@ -Subproject commit dd9d2aacf9b49c6b9460951d8577c7a66d74e6c0 +Subproject commit d76b54e80f2eb188e7c098d8c9aaba4ec0d0b354 From 52855dc743be66b729bf22d78157bc18007b2f98 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:33:23 +0000 Subject: [PATCH 06/16] Add ignore flag for batteries, Strata, and cslib submodules --- .gitmodules | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitmodules b/.gitmodules index 5a180c0..9d9431b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,9 +16,12 @@ [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 From c18288265adb1591597490a17ad2b43d6fda5f6e Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:33:44 +0000 Subject: [PATCH 07/16] Update dependencies to version 4.30.0 in lake-manifest.json, lakefile.lean, and lean-toolchain --- src/data/test/Mathlib/lake-manifest.json | 33 ++++++++++++------------ src/data/test/Mathlib/lakefile.lean | 3 +-- src/data/test/Mathlib/lean-toolchain | 2 +- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/data/test/Mathlib/lake-manifest.json b/src/data/test/Mathlib/lake-manifest.json index eabbf16..ed9c558 100644 --- 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 index b1f61b0..d22cb4c 100644 --- 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 index c00a535..af9e5d3 100644 --- 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 From c51b6956bdd820291e1805a612defb0ca88678c1 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 1 Jun 2026 06:44:44 +0000 Subject: [PATCH 08/16] Update batteries submodule to latest commit --- src/data/test/batteries | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/test/batteries b/src/data/test/batteries index 8da40b7..32dc18c 160000 --- a/src/data/test/batteries +++ b/src/data/test/batteries @@ -1 +1 @@ -Subproject commit 8da40b72fece29b7d3fe3d768bac4c8910ce9bee +Subproject commit 32dc18cde3684679f3c003de608743b57498c56f From 483ce49469da670346d94eb07b1b948ccb36b9d5 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 7 Jun 2026 17:46:22 +0000 Subject: [PATCH 09/16] Add new benchmark configurations for cslib and strata; update mathlib extraction settings --- .../benchmark/cslib_benchmark_lean_ext.yaml | 20 ++++++++++++++++ .../benchmark/mathlib_benchmark_lean_ext.yaml | 5 ++++ .../benchmark/stdlib_benchmark_lean_ext.yaml | 4 ++-- .../benchmark/strata_benchmark_lean_ext.yaml | 23 +++++++++++++++++++ .../main/configs/cslib_lean_data_extract.yaml | 9 ++++++++ .../configs/mathlib_lean_data_extract.yaml | 3 ++- 6 files changed, 61 insertions(+), 3 deletions(-) create mode 100644 src/itp_interface/main/configs/benchmark/cslib_benchmark_lean_ext.yaml create mode 100644 src/itp_interface/main/configs/benchmark/strata_benchmark_lean_ext.yaml create mode 100644 src/itp_interface/main/configs/cslib_lean_data_extract.yaml diff --git a/src/itp_interface/main/configs/benchmark/cslib_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/cslib_benchmark_lean_ext.yaml new file mode 100644 index 0000000..f1f2c19 --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/cslib_benchmark_lean_ext.yaml @@ -0,0 +1,20 @@ +name: cslib_benchmark_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/cslib + files: [] + exclude_files: + - src/data/test/cslib/.lake + - src/data/test/cslib/.vscode + - src/data/test/cslib/.github + - src/data/test/cslib/.git + - src/data/test/cslib/lake-manifest.json + - src/data/test/cslib/lakefile.toml + - src/data/test/cslib/scripts + - src/data/test/cslib/CslibTests \ No newline at end of file diff --git a/src/itp_interface/main/configs/benchmark/mathlib_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/mathlib_benchmark_lean_ext.yaml index b2bb43b..363ae42 100644 --- a/src/itp_interface/main/configs/benchmark/mathlib_benchmark_lean_ext.yaml +++ b/src/itp_interface/main/configs/benchmark/mathlib_benchmark_lean_ext.yaml @@ -38,3 +38,8 @@ datasets: - src/data/test/Mathlib/.lake/packages/mathlib/Archive.lean - src/data/test/Mathlib/lakefile.lean - src/data/test/Mathlib/ReplMathlibTests.lean + - src/data/test/Mathlib/.lake/packages/mathlib/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean + - src/data/test/Mathlib/.lake/packages/mathlib/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean + - src/data/test/Mathlib/.lake/packages/mathlib/Mathlib/Combinatorics/Colex.lean + - src/data/test/Mathlib/.lake/packages/mathlib/Mathlib/Data/EReal/Inv.lean + - src/data/test/Mathlib/.lake/packages/mathlib/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean diff --git a/src/itp_interface/main/configs/benchmark/stdlib_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/stdlib_benchmark_lean_ext.yaml index fde9d37..fb0a31d 100644 --- a/src/itp_interface/main/configs/benchmark/stdlib_benchmark_lean_ext.yaml +++ b/src/itp_interface/main/configs/benchmark/stdlib_benchmark_lean_ext.yaml @@ -27,5 +27,5 @@ datasets: - src/data/test/batteries/.github - src/data/test/batteries/lake-manifest.json include_files: - - ~/.elan/toolchains/leanprover--lean4---v4.24.0/src/lean/Init - - ~/.elan/toolchains/leanprover--lean4---v4.24.0/src/lean/Std \ No newline at end of file + - ~/.elan/toolchains/leanprover--lean4---v4.30.0/src/lean/Init + - ~/.elan/toolchains/leanprover--lean4---v4.30.0/src/lean/Std \ No newline at end of file diff --git a/src/itp_interface/main/configs/benchmark/strata_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/strata_benchmark_lean_ext.yaml new file mode 100644 index 0000000..7fbec6f --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/strata_benchmark_lean_ext.yaml @@ -0,0 +1,23 @@ +name: strata_benchmark_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/Strata + files: [] + exclude_files: + - src/data/test/Strata/.lake + - src/data/test/Strata/.vscode + - src/data/test/Strata/docs + - src/data/test/Strata/lake-manifest.toml + - src/data/test/Strata/.docker + - src/data/test/Strata/lakefile.toml + - src/data/test/Strata/.gitpod.yml + - src/data/test/Strata/.github + - src/data/test/Strata/.git + - src/data/test/Strata/lake-manifest.json + - src/data/test/Strata/vcs \ No newline at end of file diff --git a/src/itp_interface/main/configs/cslib_lean_data_extract.yaml b/src/itp_interface/main/configs/cslib_lean_data_extract.yaml new file mode 100644 index 0000000..14cfed8 --- /dev/null +++ b/src/itp_interface/main/configs/cslib_lean_data_extract.yaml @@ -0,0 +1,9 @@ +defaults: + - benchmark: cslib_benchmark_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/cslib_benchmark_lean_ext + pool_size: 12 \ No newline at end of file diff --git a/src/itp_interface/main/configs/mathlib_lean_data_extract.yaml b/src/itp_interface/main/configs/mathlib_lean_data_extract.yaml index 14e39be..5e7c48f 100644 --- a/src/itp_interface/main/configs/mathlib_lean_data_extract.yaml +++ b/src/itp_interface/main/configs/mathlib_lean_data_extract.yaml @@ -10,4 +10,5 @@ defaults: run_settings: output_dir: .log/data_generation/benchmark/mathlib_benchmark_lean_ext - pool_size: 12 \ No newline at end of file + pool_size: 5 + memory_per_task_gb: 70 \ No newline at end of file From 065a029a7b0938e025d8749f9df76ee4f8131253 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 7 Jun 2026 17:48:03 +0000 Subject: [PATCH 10/16] Enhance memory management in data generation pipeline; add memory limit options and monitoring --- src/itp_interface/lean/tactic_parser.py | 86 +++++++++++++++++-- src/itp_interface/main/config.py | 4 +- src/itp_interface/main/run_tool.py | 9 +- src/itp_interface/tools/ray_utils.py | 7 +- .../tools/run_data_generation_transforms.py | 21 +++-- 5 files changed, 110 insertions(+), 17 deletions(-) diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index da990dc..434836b 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -10,10 +10,13 @@ import base64 import json import os +import signal import subprocess import logging import re import shutil +import threading +import time from enum import Enum from pydantic import BaseModel, field_validator from pathlib import Path @@ -376,6 +379,29 @@ def build_tactic_parser_if_needed(logger: Optional[logging.Logger] = None): if not is_tactic_parser_built(): build_lean4_project(get_path_to_tactic_parser_project(), 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.""" + total = 0 + try: + for entry in os.listdir('/proc'): + if not entry.isdigit(): + continue + try: + with open(f'/proc/{entry}/stat', 'r') as f: + stat = f.read().split() + if int(stat[4]) == pgid: + with open(f'/proc/{entry}/status', 'r') as f: + for line in f: + if line.startswith('VmRSS:'): + total += int(line.split()[1]) + break + except (FileNotFoundError, ValueError, IndexError, PermissionError): + continue + except Exception: + pass + return total + + def get_path_to_dependency_parser_executable() -> str: """Get the path to the dependency parser executable.""" abs_path = get_path_to_tactic_parser_project() @@ -386,7 +412,8 @@ def analyze_lean_file_dependencies( full_lean_file_path: str, json_output_path: str, working_dir: Optional[str] = None, - logger: Optional[logging.Logger] = None + logger: Optional[logging.Logger] = None, + memory_limit_fraction: float = 0.30 ) -> tuple[List[FileDependencyAnalysis], List[ErrorInfo]]: """ Analyze dependencies in a Lean file and export to JSON. @@ -432,15 +459,64 @@ def analyze_lean_file_dependencies( logger.debug(f"Running dependency analysis: {' '.join(cmds)}") logger.debug(f"Working directory: {working_dir}") - # Execute the command - result = subprocess.run( + # Read total system memory once + try: + with open('/proc/meminfo', 'r') as _f: + _mem_total_kb = int(next(l for l in _f if l.startswith('MemTotal:')).split()[1]) + except Exception: + _mem_total_kb = 0 + mem_limit_kb = int(_mem_total_kb * memory_limit_fraction) + + proc = subprocess.Popen( cmds, cwd=working_dir, - capture_output=True, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, text=True, - check=False # Don't raise on error, handle it ourselves + preexec_fn=os.setsid # new process group so we can kill the whole tree ) + killed_oom = threading.Event() + + def _memory_monitor(): + try: + pgid = os.getpgid(proc.pid) + except ProcessLookupError: + return + while proc.poll() is None: + time.sleep(2) + rss_kb = _get_process_group_rss_kb(pgid) + if mem_limit_kb > 0 and rss_kb > mem_limit_kb: + logger.warning( + f"dependency-parser for {full_lean_file_path} used " + f"{rss_kb/1024/1024:.1f} GB (>{memory_limit_fraction*100:.0f}% of RAM). Killing." + ) + killed_oom.set() + try: + os.killpg(pgid, signal.SIGKILL) + except ProcessLookupError: + pass + return + + monitor_thread = threading.Thread(target=_memory_monitor, daemon=True) + monitor_thread.start() + stdout, stderr = proc.communicate() + monitor_thread.join(timeout=3) + + if killed_oom.is_set(): + empty = FileDependencyAnalysis( + file_path=full_lean_file_path, + module_name="", + imports=[], + declarations=[] + ) + return [empty], [ErrorInfo( + message=f"Killed: exceeded {memory_limit_fraction*100:.0f}% memory limit", + position=Position(line=0, column=0) + )] + + result = subprocess.CompletedProcess(cmds, proc.returncode, stdout, stderr) + logger.debug(f"Dependency analysis stdout: {result.stdout}") if result.stderr: logger.warning(f"Dependency analysis stderr: {result.stderr}") diff --git a/src/itp_interface/main/config.py b/src/itp_interface/main/config.py index 86e49f2..a7fa287 100644 --- a/src/itp_interface/main/config.py +++ b/src/itp_interface/main/config.py @@ -61,6 +61,7 @@ class RunSettings(object): random_seed: int = 42 random_split: bool = False train_eval_test_split: typing.List[float] = field(default_factory=lambda: [1.0, 0.0, 0.0]) + memory_per_task_gb: typing.Optional[float] = None @dataclass_json @dataclass @@ -163,7 +164,8 @@ def parse_config(cfg): should_checkpoint=run_settings_cfg["should_checkpoint"], random_seed=run_settings_cfg["random_seed"], random_split=run_settings_cfg["random_split"], - train_eval_test_split=run_settings_cfg["train_eval_test_split"]) + train_eval_test_split=run_settings_cfg["train_eval_test_split"], + memory_per_task_gb=run_settings_cfg.get("memory_per_task_gb", None)) benchmark_cfg = cfg["benchmark"] datasets_cfg = benchmark_cfg["datasets"] eval_datasets = [] diff --git a/src/itp_interface/main/run_tool.py b/src/itp_interface/main/run_tool.py index 24c0366..11ec3bd 100644 --- a/src/itp_interface/main/run_tool.py +++ b/src/itp_interface/main/run_tool.py @@ -551,11 +551,12 @@ def run_data_generation_pipeline(experiment: Experiments, log_dir: str, checkpoi try: data_transform.run_all_local_transforms( experiment.run_settings.pool_size, - partition_project_to_theorems, - use_human_readable=experiment.run_settings.use_human_readable, - new_output_dir=new_output_dir, + partition_project_to_theorems, + use_human_readable=experiment.run_settings.use_human_readable, + new_output_dir=new_output_dir, log_error=True, - other_args=other_args) + other_args=other_args, + memory_per_task_gb=experiment.run_settings.memory_per_task_gb) finally: if clone_dir is not None: for project in projects: diff --git a/src/itp_interface/tools/ray_utils.py b/src/itp_interface/tools/ray_utils.py index d462740..0a99f2b 100644 --- a/src/itp_interface/tools/ray_utils.py +++ b/src/itp_interface/tools/ray_utils.py @@ -40,10 +40,13 @@ def connect_to_ray(): return None @staticmethod - def init_ray(num_of_cpus: int = 10, object_store_memory_in_gb: float = 25, memory_in_gb: float = 0.5, runtime_env: typing.Dict[str, str] = None): + def init_ray(num_of_cpus: int = 10, object_store_memory_in_gb: float = 25, memory_in_gb: float = 0.5, total_memory_in_gb: typing.Optional[float] = None, runtime_env: typing.Dict[str, str] = None): gb = 2**30 object_store_memory = int(object_store_memory_in_gb * gb) - memory = int(memory_in_gb * gb) + if total_memory_in_gb is not None: + memory = int(total_memory_in_gb * gb) + else: + memory = int(memory_in_gb * gb) obj = RayUtils.connect_to_ray() if obj is not None: return obj diff --git a/src/itp_interface/tools/run_data_generation_transforms.py b/src/itp_interface/tools/run_data_generation_transforms.py index bacbb25..2a4a797 100644 --- a/src/itp_interface/tools/run_data_generation_transforms.py +++ b/src/itp_interface/tools/run_data_generation_transforms.py @@ -262,7 +262,7 @@ def merge_local_transforms(self, idx += 1 self.logger.info(f"==============================>[{transform.name}] Merged local transforms for all projects<==============================") - def run_local_transform(self, pool_size: int , transform: typing.Union[CoqLocalDataGenerationTransform, LeanLocalDataGenerationTransform, IsabelleLocalDataGenerationTransform], projects: typing.Dict[str, typing.Dict[str, str]], use_human_readable: bool, new_output_dir: str, log_error: bool, save_transform: bool = True, preserve_temp: bool = True, other_args: typing.Dict[str, typing.Dict[str, dict]] = {}): + def run_local_transform(self, pool_size: int , transform: typing.Union[CoqLocalDataGenerationTransform, LeanLocalDataGenerationTransform, IsabelleLocalDataGenerationTransform], projects: typing.Dict[str, typing.Dict[str, str]], use_human_readable: bool, new_output_dir: str, log_error: bool, save_transform: bool = True, preserve_temp: bool = True, other_args: typing.Dict[str, typing.Dict[str, dict]] = {}, memory_per_task_gb: typing.Optional[float] = None): assert pool_size > 0, "pool_size should be greater than 0" assert transform is not None, "transform should not be None" assert projects is not None, "projects should not be None" @@ -280,7 +280,13 @@ def run_local_transform(self, pool_size: int , transform: typing.Union[CoqLocalD object_store_memory_in_gb = 100 memory_in_gb = 5 if not RayUtils.is_ray_initialized(): - ray_dashboard = RayUtils.init_ray(num_of_cpus=pool_size, object_store_memory_in_gb=object_store_memory_in_gb, memory_in_gb=memory_in_gb) + if memory_per_task_gb is not None: + with open('/proc/meminfo', 'r') as _f: + _mem_total_kb = int(next(l for l in _f if l.startswith('MemTotal:')).split()[1]) + total_mem_gb = _mem_total_kb / (1024 * 1024) + ray_dashboard = RayUtils.init_ray(num_of_cpus=pool_size, object_store_memory_in_gb=object_store_memory_in_gb, total_memory_in_gb=total_mem_gb) + else: + ray_dashboard = RayUtils.init_ray(num_of_cpus=pool_size, object_store_memory_in_gb=object_store_memory_in_gb, memory_in_gb=memory_in_gb) else: ray_dashboard = "Ray already initialized" self.logger.info(f"==============================>[{transform.name}] Ray initialized with {transform.max_parallelism} CPUs, Memory=({memory_in_gb} GiB, Object Memory = {object_store_memory_in_gb} GiB)<==============================") @@ -370,11 +376,16 @@ def run_local_transform(self, pool_size: int , transform: typing.Union[CoqLocalD if self._use_ray: # Ray-based execution + _memory_bytes = int(memory_per_task_gb * 2**30) if memory_per_task_gb is not None else None def _create_remotes(job_list): remotes = [] for job in job_list: self.logger.info(f"[{transform.name}] Starting transform for {job[4]}") - remotes.append(RunDataGenerationTransforms.run_local_transform_on_file.remote(*job)) + if _memory_bytes is not None: + remote = RunDataGenerationTransforms.run_local_transform_on_file.options(memory=_memory_bytes).remote(*job) + else: + remote = RunDataGenerationTransforms.run_local_transform_on_file.remote(*job) + remotes.append(remote) return remotes def _prepare_remotes(num: int): @@ -428,14 +439,14 @@ def _transform_output(results): self.logger.warning(f"==============================>[{transform.name}] Removing temp directory {temp_output_dir}<==============================") shutil.rmtree(temp_output_dir) - def run_all_local_transforms(self, pool_size: int, projects: typing.Dict[str, typing.Dict[str, str]], use_human_readable: bool, new_output_dir: str, log_error: bool, other_args: typing.Dict[str, typing.Dict[str, dict]] = {}): + def run_all_local_transforms(self, pool_size: int, projects: typing.Dict[str, typing.Dict[str, str]], use_human_readable: bool, new_output_dir: str, log_error: bool, other_args: typing.Dict[str, typing.Dict[str, dict]] = {}, memory_per_task_gb: typing.Optional[float] = None): os.makedirs(new_output_dir, exist_ok=True) for idx, transform in enumerate(self.transforms): last_transform = idx == len(self.transforms) - 1 save_transform = self.save_intermidiate_transforms or last_transform temp_new_output_dir = str(Path(new_output_dir) / str(idx)) os.makedirs(temp_new_output_dir, exist_ok=True) - self.run_local_transform(pool_size, transform, projects, use_human_readable, temp_new_output_dir, log_error, save_transform, preserve_temp=self.save_intermidiate_transforms, other_args=other_args) + self.run_local_transform(pool_size, transform, projects, use_human_readable, temp_new_output_dir, log_error, save_transform, preserve_temp=self.save_intermidiate_transforms, other_args=other_args, memory_per_task_gb=memory_per_task_gb) pass # Create Ray remote version if Ray is available From 52a6f46ab07d2cade83b5f8750759b5f7bab277e Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Sun, 7 Jun 2026 21:37:27 +0000 Subject: [PATCH 11/16] Add new benchmark configurations and datasets for Clever, MiniF2F, and PutnamBench --- .gitmodules | 9 +++++++++ src/data/test/PutnamBench | 1 + src/data/test/clever | 1 + src/data/test/miniF2F-lean4 | 1 + .../benchmark/clever_benchmark_lean_ext.yaml | 15 +++++++++++++++ .../main/configs/benchmark/miniF2F_lean_ext.yaml | 16 ++++++++++++++++ .../configs/benchmark/putnambench_lean_ext.yaml | 16 ++++++++++++++++ .../main/configs/clever_lean_data_extract.yaml | 9 +++++++++ .../main/configs/minif2f_lean_data_extract.yaml | 9 +++++++++ .../configs/putnambench_lean_data_extract.yaml | 9 +++++++++ 10 files changed, 86 insertions(+) create mode 160000 src/data/test/PutnamBench create mode 160000 src/data/test/clever create mode 160000 src/data/test/miniF2F-lean4 create mode 100644 src/itp_interface/main/configs/benchmark/clever_benchmark_lean_ext.yaml create mode 100644 src/itp_interface/main/configs/benchmark/miniF2F_lean_ext.yaml create mode 100644 src/itp_interface/main/configs/benchmark/putnambench_lean_ext.yaml create mode 100644 src/itp_interface/main/configs/clever_lean_data_extract.yaml create mode 100644 src/itp_interface/main/configs/minif2f_lean_data_extract.yaml create mode 100644 src/itp_interface/main/configs/putnambench_lean_data_extract.yaml diff --git a/.gitmodules b/.gitmodules index 9d9431b..d7a125b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -25,3 +25,12 @@ 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/src/data/test/PutnamBench b/src/data/test/PutnamBench new file mode 160000 index 0000000..c4131a2 --- /dev/null +++ b/src/data/test/PutnamBench @@ -0,0 +1 @@ +Subproject commit c4131a2401d1baedef37df4b02ec8dc2aac24e1a diff --git a/src/data/test/clever b/src/data/test/clever new file mode 160000 index 0000000..7d0e80f --- /dev/null +++ b/src/data/test/clever @@ -0,0 +1 @@ +Subproject commit 7d0e80f5b35383126148267c8bfbbd6fe8ff2309 diff --git a/src/data/test/miniF2F-lean4 b/src/data/test/miniF2F-lean4 new file mode 160000 index 0000000..5746b7d --- /dev/null +++ b/src/data/test/miniF2F-lean4 @@ -0,0 +1 @@ +Subproject commit 5746b7d6c47855ce1294bed87329618ff7f1bc31 diff --git a/src/itp_interface/main/configs/benchmark/clever_benchmark_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/clever_benchmark_lean_ext.yaml new file mode 100644 index 0000000..15ab9ce --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/clever_benchmark_lean_ext.yaml @@ -0,0 +1,15 @@ +name: clever_benchmark_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/clever/src/lean4 + files: [] + exclude_files: + - src/data/test/clever/src/lean4/.lake + - src/data/test/clever/src/lean4/Imports + - src/data/test/clever/src/lean4/sample_examples \ No newline at end of file diff --git a/src/itp_interface/main/configs/benchmark/miniF2F_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/miniF2F_lean_ext.yaml new file mode 100644 index 0000000..5472280 --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/miniF2F_lean_ext.yaml @@ -0,0 +1,16 @@ +name: miniF2F_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/miniF2F-lean4 + files: [] + exclude_files: + - src/data/test/miniF2F-lean4/.lake + - src/data/test/miniF2F-lean4/MiniF2F/Test.lean + - src/data/test/miniF2F-lean4/MiniF2F/Valid.lean + - src/data/test/miniF2F-lean4/MiniF2F/Valid \ No newline at end of file diff --git a/src/itp_interface/main/configs/benchmark/putnambench_lean_ext.yaml b/src/itp_interface/main/configs/benchmark/putnambench_lean_ext.yaml new file mode 100644 index 0000000..0780cc9 --- /dev/null +++ b/src/itp_interface/main/configs/benchmark/putnambench_lean_ext.yaml @@ -0,0 +1,16 @@ +name: putnambench_lean_ext +num_files: 1 +language: LEAN4 +few_shot_data_path_for_retrieval: +few_shot_metadata_filename_for_retrieval: +dfs_data_path_for_retrieval: +dfs_metadata_filename_for_retrieval: +is_extraction_request: true +datasets: + - project: src/data/test/PutnamBench/lean4 + files: [] + exclude_files: + - src/data/test/PutnamBench/lean4/.lake + - src/data/test/PutnamBench/lean4/src + - src/data/test/PutnamBench/lean4/check_docstrings.lean + - src/data/test/PutnamBench/lean4/lakefile.lean \ No newline at end of file diff --git a/src/itp_interface/main/configs/clever_lean_data_extract.yaml b/src/itp_interface/main/configs/clever_lean_data_extract.yaml new file mode 100644 index 0000000..bcfe002 --- /dev/null +++ b/src/itp_interface/main/configs/clever_lean_data_extract.yaml @@ -0,0 +1,9 @@ +defaults: + - benchmark: clever_benchmark_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/clever_benchmark_lean_ext + pool_size: 12 \ No newline at end of file diff --git a/src/itp_interface/main/configs/minif2f_lean_data_extract.yaml b/src/itp_interface/main/configs/minif2f_lean_data_extract.yaml new file mode 100644 index 0000000..2022459 --- /dev/null +++ b/src/itp_interface/main/configs/minif2f_lean_data_extract.yaml @@ -0,0 +1,9 @@ +defaults: + - benchmark: miniF2F_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/miniF2F_lean_ext + pool_size: 12 \ No newline at end of file diff --git a/src/itp_interface/main/configs/putnambench_lean_data_extract.yaml b/src/itp_interface/main/configs/putnambench_lean_data_extract.yaml new file mode 100644 index 0000000..3bb85db --- /dev/null +++ b/src/itp_interface/main/configs/putnambench_lean_data_extract.yaml @@ -0,0 +1,9 @@ +defaults: + - benchmark: putnambench_lean_ext + - run_settings: default_lean4_data_generation_transforms + - env_settings: no_retrieval + - override hydra/job_logging: 'disabled' + +run_settings: + output_dir: .log/data_generation/benchmark/putnambench_lean_ext + pool_size: 12 \ No newline at end of file From 4041b4d974ad6d4f407f5e2569ef28f017126766 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 8 Jun 2026 14:58:07 +0000 Subject: [PATCH 12/16] Update lean-toolchain to version 4.30.0 --- src/data/test/lean4_proj/lake-manifest.json | 31 +++++++++++---------- src/data/test/lean4_proj/lean-toolchain | 2 +- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/src/data/test/lean4_proj/lake-manifest.json b/src/data/test/lean4_proj/lake-manifest.json index a5475ce..da2f424 100644 --- 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 index 58ae245..5a8f161 100644 --- a/src/data/test/lean4_proj/lean-toolchain +++ b/src/data/test/lean4_proj/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.24.0 \ No newline at end of file +leanprover/lean4:v4.30.0 \ No newline at end of file From 9c91ad126d28c8431ed63ac8e55c8127b74ed24b Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 8 Jun 2026 15:10:33 +0000 Subject: [PATCH 13/16] Update default Lean version to 4.30.0 in README and tactic parser --- README.md | 4 ++-- src/itp_interface/lean/tactic_parser.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 1d55d3d..65184bc 100644 --- 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,7 +30,7 @@ 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 ``` diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index 434836b..a73ca65 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -293,7 +293,7 @@ def get_path_to_tactic_parser_executable() -> str: return tactic_parser_bin_path def toolchain_version_and_env_version(): - lean_version_needed = os.getenv("LEAN_VERSION", "4.24.0") + lean_version_needed = os.getenv("LEAN_VERSION", "4.30.0") tactic_parser_project = get_path_to_tactic_parser_project() # Check the version of the built parser toolchain_file = os.path.join(tactic_parser_project, "lean-toolchain") From 4c01a7bbb001dd160eeadc7fcf5bc959e8e77f5f Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 8 Jun 2026 15:39:54 +0000 Subject: [PATCH 14/16] Add memory limit configuration for dependency parser and update documentation --- .../workflows/github-build-actions-python314t.yaml | 1 + .github/workflows/github-build-actions.yaml | 1 + README.md | 10 ++++++++++ .../lean/simple_lean4_sync_executor.py | 13 +++++++------ src/itp_interface/lean/tactic_parser.py | 9 +++++++++ 5 files changed, 28 insertions(+), 6 deletions(-) diff --git a/.github/workflows/github-build-actions-python314t.yaml b/.github/workflows/github-build-actions-python314t.yaml index 178fd43..61959b2 100644 --- 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 index e63b419..494595f 100644 --- 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/README.md b/README.md index 65184bc..9a3bf34 100644 --- a/README.md +++ b/README.md @@ -35,6 +35,16 @@ install-itp-interface 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/src/itp_interface/lean/simple_lean4_sync_executor.py b/src/itp_interface/lean/simple_lean4_sync_executor.py index deb99aa..9f431bd 100644 --- 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: diff --git a/src/itp_interface/lean/tactic_parser.py b/src/itp_interface/lean/tactic_parser.py index a73ca65..2c03f17 100644 --- a/src/itp_interface/lean/tactic_parser.py +++ b/src/itp_interface/lean/tactic_parser.py @@ -423,6 +423,8 @@ def analyze_lean_file_dependencies( json_output_path: Path where JSON output will be written (relative to working_dir) working_dir: Working directory (Lean project root). If None, uses current directory. logger: Optional logger for debugging + memory_limit_fraction: Fraction of total RAM allowed before killing the parser. + Overridden by the ITP_DEP_PARSER_MEM_LIMIT environment variable when set. Returns: tuple: (FileDependencyAnalysis, List[ErrorInfo]) - analysis results and any errors @@ -437,6 +439,13 @@ def analyze_lean_file_dependencies( if working_dir is None: working_dir = os.getcwd() + env_limit = os.environ.get("ITP_DEP_PARSER_MEM_LIMIT") + if env_limit is not None: + try: + memory_limit_fraction = float(env_limit) + except ValueError: + logger.warning(f"ITP_DEP_PARSER_MEM_LIMIT='{env_limit}' is not a valid float; using {memory_limit_fraction}") + # Ensure the dependency parser is built build_tactic_parser_if_needed(logger) From 4670e515ba4a0e2e99821be388f35e3fc1fd3b03 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 8 Jun 2026 16:02:42 +0000 Subject: [PATCH 15/16] Remove deprecated requirements files for project cleanup --- requirements.txt | 26 -------------------------- tacc_requirements.txt | 26 -------------------------- 2 files changed, 52 deletions(-) delete mode 100644 requirements.txt delete mode 100644 tacc_requirements.txt diff --git a/requirements.txt b/requirements.txt deleted file mode 100644 index 0fbd10e..0000000 --- a/requirements.txt +++ /dev/null @@ -1,26 +0,0 @@ -dataclasses-json==0.5.7 -numpy>=1.24.0 -pexpect==4.8.0 -sexpdata==1.0.0 -pampy==0.3.0 -ray==2.4.0 -pydantic==1.10.13 # Bug with ray 2.4.0 where it is not compatible with pydantic >= 2 -faiss-cpu>=1.6.1 -filelock==3.12.4 -regex==2023.10.3 -tqdm>=4.27 -wget==3.2 -hydra-core>=1.0.0 -omegaconf>=2.0.1 -jsonlines==4.0.0 -soundfile==0.12.1 -editdistance==0.8.1 -rank_bm25==0.2.2 -parglare==0.16.1 -psutil==5.9.8 -urllib3>=2.0.7 -mathlibtools==1.3.2 -pyyaml==6.0.1 -pylspclient==0.0.3 -protobuf==3.20.1 -grpcio==1.51.3 \ No newline at end of file diff --git a/tacc_requirements.txt b/tacc_requirements.txt deleted file mode 100644 index a15bea4..0000000 --- a/tacc_requirements.txt +++ /dev/null @@ -1,26 +0,0 @@ -dataclasses-json==0.5.7 -numpy>=1.24.0 -pexpect==4.8.0 -sexpdata==1.0.0 -pampy==0.3.0 -ray==2.36.0 -pydantic==1.10.13 # Bug with ray 2.4.0 where it is not compatible with pydantic >= 2 -faiss-cpu>=1.6.1 -filelock==3.12.4 -regex==2023.10.3 -tqdm>=4.27 -wget==3.2 -hydra-core>=1.0.0 -omegaconf>=2.0.1 -jsonlines==4.0.0 -soundfile==0.12.1 -editdistance==0.8.1 -rank_bm25==0.2.2 -parglare==0.16.1 -psutil==5.9.8 -urllib3>=2.0.7 -mathlibtools==1.3.2 -pyyaml==6.0.1 -pylspclient==0.0.3 -protobuf==3.20.1 -grpcio==1.51.3 \ No newline at end of file From 9c8bb754467853f563e22434c03da294edb2f6a8 Mon Sep 17 00:00:00 2001 From: Amitayush Thakur Date: Mon, 8 Jun 2026 16:02:50 +0000 Subject: [PATCH 16/16] Bump version to 1.7.0 in pyproject.toml --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 0870b99..717571b 100644 --- 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" }, ]