feat: delay elab of full file - #15222
Draft
AugustDeer wants to merge 3 commits into
Draft
AugustDeer wants to merge 3 commits into
AugustDeer wants to merge 3 commits into
Conversation
Delays the elaboration of future commands to avoid repeated recompilation of an entire file while typing. Fixes (leanprover#15013)
Adds an cmdline option to change the delay for elaborating a file. Also reduces the delay during testing.
3 tasks
github-actions
Bot
added
the
toolchain-available
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.
This PR delays the elaboration of future commands to avoid repeated recompilation of an entire file while typing. The delay defaults to 100ms, and can be customized with a cmdline option.
Closes #15013
AI Usage Notice: This PR was developed with the help of Deepseek Flash 4.1 running through the Opencode harness. All AI-written code was reviewed and verified by the author. Communication regarding this PR (including this description and the commit descriptions) were and will continue to be entirely human. I take full responsibility for my work.