Skip to content

Revampped the Lean 4 execution framework; Removed REPL dependency #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 53 commits into from
Nov 7, 2025
Merged

Revampped the Lean 4 execution framework; Removed REPL dependency #61

merged 53 commits into from
Nov 7, 2025

Conversation

@amit9oct
Copy link
Collaborator

@amit9oct amit9oct commented Oct 31, 2025

No description provided.

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

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@amit9oct