Introduce incremental processing of the commands#109
Open
augustepoiroux wants to merge 13 commits intoleanprover-community:masterfrom
Open
Introduce incremental processing of the commands#109augustepoiroux wants to merge 13 commits intoleanprover-community:masterfrom
augustepoiroux wants to merge 13 commits intoleanprover-community:masterfrom
Conversation
augustepoiroux
force-pushed
the
incremental_processing
branch
4 times, most recently
from
d5b1011 to
cc50ca5
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
cc50ca5 to
92ba30b
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
2 times, most recently
from
c576842 to
7b48365
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
7b48365 to
8de3d74
Compare
augustepoiroux
added a commit
to augustepoiroux/LeanInteract
that referenced
this pull request
Oct 13, 2025
Add the following features: - Fine-grained data extraction for Lean declarations leanprover-community/repl#119 - Incremental elaboration leanprover-community/repl#110 - also fixes #6 - Parallel elaboration (through `set_option` support) - `set_option` support leanprover-community/repl#119 A few fixes: - leanprover-community/repl#108 - leanprover-community/repl#109 Add py.typed - #32 Breaking changes: - Support for Lean v4.7.0 is dropped
augustepoiroux
force-pushed
the
incremental_processing
branch
from
8de3d74 to
62f7f6f
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
62f7f6f to
30e8799
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
3 times, most recently
from
8290a60 to
bb76fa6
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
bb76fa6 to
4d97344
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
4d97344 to
4e84023
Compare
augustepoiroux
force-pushed
the
incremental_processing
branch
from
4e84023 to
5cf9d51
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Partially fix #66
The second problem mentioned in #66 is solved by this PR: all declarations preceding the sorries within a same REPL command are now correctly collected in the environment for ProofSnapshots. This issue is a major bottleneck when using the tactic mode on files where proofs depend on lemmas introduced in the same file (i.e. submitted in the same command in the REPL)
However, the initial problem in #66 is still not solved. Auxiliary declarations within the declaration itself are still not captured correctly. I attempted to replay these auxiliary declarations with limited success. Ideas to fix this are welcome.
Note: depends on #108