Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
c415fab
Added validation method for Lean 4.
amit9oct Oct 26, 2025
b60f4e8
Added GUI tool for debugging the itp-interface through web app.
amit9oct Oct 26, 2025
d5eb4dd
Added Lean 4 tactic parser.
amit9oct Oct 29, 2025
feb67f4
Fixed tactic parser
amit9oct Oct 29, 2025
47d9a3a
Added partial proof tactic parsing.
amit9oct Oct 29, 2025
94ff5d4
Fixed tactic parser and support for parsing the theorems and lemmas
amit9oct Oct 30, 2025
3284823
Added automatic build requirements for `tactic_parser`
amit9oct Oct 30, 2025
e4f65be
Added error_info and docstring to tactic parsing.
amit9oct Oct 30, 2025
03d0b8e
Fixed declaration parsing.
amit9oct Oct 30, 2025
118f139
Added simple Lean 4 execution v1
amit9oct Oct 30, 2025
70ef1cd
First working version
amit9oct Oct 31, 2025
ab830cd
Upgraded Mathlib `data/test`
amit9oct Oct 31, 2025
7a0e631
Simplified testing code.
amit9oct Oct 31, 2025
208371b
Fixed decl name dection; added namespace detection; added state check…
amit9oct Oct 31, 2025
3748421
Added `namespace`; Fixed Lean State checkpointing bug
amit9oct Oct 31, 2025
9647356
Fixed the line number bug
amit9oct Oct 31, 2025
49502ec
First working draft
amit9oct Oct 31, 2025
33cef00
Added patch for name fixing.
amit9oct Oct 31, 2025
f3d86c2
Fixed line_num bug
amit9oct Oct 31, 2025
8d1548c
Added backward compatibility till v21
amit9oct Oct 31, 2025
b9557f2
Perfected tactic parsing.
amit9oct Nov 1, 2025
52daa20
removed unecessary type dependency
amit9oct Nov 1, 2025
28161ad
Fixed simple_lean4_sync_executor.py
amit9oct Nov 1, 2025
17b79c1
Added done and strong validation.
amit9oct Nov 1, 2025
6e9d403
Fixed the ipt-interface gui app.
amit9oct Nov 1, 2025
448d246
Fixed Lean data generation pipeline
amit9oct Nov 1, 2025
4d9dd0a
Added print logs for run data gen test
amit9oct Nov 1, 2025
0f0811a
Reduced memory footprint for data generation code; improved error mes…
amit9oct Nov 1, 2025
6aa30c7
Added extraction request config
amit9oct Nov 1, 2025
0896ef0
Added extraction request setting.
amit9oct Nov 2, 2025
581f444
Renamed the training data collection to a protocol
amit9oct Nov 2, 2025
2cf5468
Migrated TrainingDataFormat to a Protocol
amit9oct Nov 2, 2025
a3485cf
Converted LeanInfo to TrainingDataFormat
amit9oct Nov 2, 2025
21154cb
Added LeanLineInfo to training data object
amit9oct Nov 2, 2025
793e283
Added extraction transform
amit9oct Nov 2, 2025
537325b
Added full pipeline for data extraction.
amit9oct Nov 2, 2025
aa816e9
Added data extraction test
amit9oct Nov 2, 2025
ceef8b5
Ray initialization and limitation.
amit9oct Nov 2, 2025
6175402
Fixed memory initialization for ray
amit9oct Nov 2, 2025
6e785b5
Added complete dependency parsing.
amit9oct Nov 4, 2025
3dfc2d9
Renamed dependency parser
amit9oct Nov 4, 2025
924fc09
Added dependency extraction
amit9oct Nov 4, 2025
85bc511
Fixed line and column info bugs in dependency parsing.
amit9oct Nov 5, 2025
3a5e76c
Reduced memory for data extraction and data generation tests.
amit9oct Nov 5, 2025
af4d7ec
Added ray cleanup after every step
amit9oct Nov 5, 2025
00513d6
Ray low memory fixes.
amit9oct Nov 6, 2025
d8f2a8c
Added correct ray initialization test.
amit9oct Nov 6, 2025
709ed57
Fixed Lean 4 interface to accept have proofs more easily.
amit9oct Nov 7, 2025
7c76507
triming space only tactics within `have` tactics.
amit9oct Nov 7, 2025
e3f1cef
Fixed last action change possiblity
amit9oct Nov 7, 2025
381f524
Add '_last_tactic_was_modified' state to track modifications in tactics
amit9oct Nov 7, 2025
bec8c9f
Uncomment unittest.main() and comment out specific Lean 4 test calls …
amit9oct Nov 7, 2025
26dd0b4
Bump version to 1.1.15 in pyproject.toml
amit9oct Nov 7, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .github/workflows/github-build-actions-python314t.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -117,3 +117,12 @@ jobs:
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_gen_test.py

- name: Run Data Extraction Test
shell: bash
run: |
export PATH="$HOME/miniconda/bin:$PATH"
source $HOME/miniconda/bin/activate py314-ft
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_extract_test.py
24 changes: 23 additions & 1 deletion .github/workflows/github-build-actions.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,32 @@ jobs:
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_env_test.py

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Run Data Gen Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_gen_test.py
python src/test/simple_data_gen_test.py

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose

- name: Run Data Extraction Test
shell: bash
run: |
eval $(opam env)
source $HOME/.elan/env
python src/test/simple_data_extract_test.py

- name: Ray Cleanup
shell: bash
run: |
rm -rf /tmp/* --verbose
8 changes: 7 additions & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ requires = [
build-backend = "hatchling.build"
[project]
name = "itp_interface"
version = "1.1.14"
version = "1.1.15"
authors = [
{ name="Amitayush Thakur", email="[email protected]" },
]
Expand Down Expand Up @@ -45,6 +45,12 @@ dependencies = [
"grpcio>=1.51.3; python_version<'3.14'"
]

[project.optional-dependencies]
app = [
"flask>=2.3.0",
"flask-cors>=4.0.0"
]

[project.urls]
Homepage = "https://github.com/trishullab/itp-interface"
Issues = "https://github.com/trishullab/itp-interface/issues"
Expand Down
Loading