Skip to content
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

feat: snapshot trees and language processors #3014

Merged
merged 69 commits into from
Mar 14, 2024
Merged

feat: snapshot trees and language processors #3014

merged 69 commits into from
Mar 14, 2024

Conversation

Kha
Copy link
Member

@Kha Kha commented Dec 2, 2023 •
edited
Loading

This is the foundation for work on making processing in the language server both more fine-grained (incremental tactics) as well as parallel.

Kha added 28 commits October 24, 2023 12:07
@Kha
feat: start integrating new snapshot types into cmdline driver
ceeaff7
@Kha
feat: switch Language to bundled, integrate into cmdline driver in …
d0fd3d7 
…full
@Kha
fix: do not duplicate output
152d594
@Kha
fix: more output fixes
a68d1c6
@Kha
foo
f2f6016
@Kha
fix: run_task/deactivate_task race condition on m_imp->m_closure
986d1c1
@Kha
fix: re-read HTTP header when skipping notification in `Ipc.readRespo…
d2bf996 
…nseAs`
@Kha
fix: debounce server status reporting
23da22e
@Kha
fix: create snapshot for header in legacy adapter
7932c0d
@Kha
fix: memoize cmdSnaps legacy adapter so getFinishedPrefix works a…
00e976c 
…s expected
@Kha
fix: waitForDiagnostics must wait on reporter task
7c0ad9c
@Kha
doc: Language
89383cf
@Kha
chore: rely on auto cancellation of reporter
58c19d7
@Kha
doc: more
22aa0dc
@Kha
Merge remote-tracking branch 'upstream/master' into het-snaps
1d547d3
@Kha
import at most once per worker process
0ce8fee
@Kha
fix test outputs
4c9b70b
@Kha
File worker: synchronize output messages
0282d1c
@Kha
fix: incremental parsing
8fff2e2
@Kha
polish Lean.Language.Lean
ca75ce2
@Kha
better naming
44cb1cc
@Kha
feat: synchronous execution of task continuations
057184b
@Kha
synchronous fast forwarding in Lean processor
0688e22
@Kha
Bring back trust level
d0e9409
@Kha
Merge remote-tracking branch 'upstream/master' into het-snaps
85a151b
@Kha
Try a shortcut
3930e40
@Kha
Remove redundant fields
3b14598
@Kha
doc
daf6fde
@Kha Kha changed the title Het snaps feat: snapshot trees and language processors Dec 2, 2023
@Kha
Copy link
Member Author

Kha commented Dec 2, 2023

!bench

@Kha
Copy link
Member Author

Kha commented Mar 7, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 959fa55.
There were no significant changes against commit 6af7a01.

tydeu pushed a commit to tydeu/lean4 that referenced this pull request Mar 11, 2024
@mhuisi @tydeu
feat: partial words import completion (leanprover#3602)
1c64a16 
This PR enables import auto-completion to complete partial words in
imports.

Other inconsistencies that I've found in import completion already seem
to be fixed by leanprover#3014. Since it will be merged soon, there is no need to
invest time to fix these issues on master.
@Kha
Copy link
Member Author

Kha commented Mar 14, 2024

Saving original PR description -

TODOs before merging:

Cleanup TODOs for further PRs:

@Kha Kha added this pull request to the merge queue Mar 14, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 14, 2024
@Kha Kha enabled auto-merge March 14, 2024 13:25
@Kha Kha added this pull request to the merge queue Mar 14, 2024
Merged via the queue into leanprover:master with commit 68eaf33 Mar 14, 2024
10 checks passed
@Kha Kha deleted the het-snaps branch March 14, 2024 15:24
github-merge-queue bot pushed a commit that referenced this pull request Mar 14, 2024
@mhuisi
feat: server -> client requests (#3271)
795e332 
This PR adds support for requests from the server to the client in the
language server. It is based on #3014 and was developed during an
experiment for #3247 that unfortunately did not go anywhere.
github-merge-queue bot pushed a commit that referenced this pull request Mar 18, 2024
@mhuisi
feat: diagnostics for stale dependencies (#3247)
3c82f9a 
Sends a diagnostic informing the user to run Restart File when a file
dependency is saved.

Based on #3014 because this feature was easier to implement with the new
architecture.

ToDo:
- [x] Adjust vscode-lean4 to display a notification when this diagnostic
appears in a non-annoying way
(leanprover/vscode-lean4#393)
- [x] Use a file watcher to identify changes to files not tracked by VS
Code
- [x] Rebase onto master when #3014 is merged
Kha added a commit that referenced this pull request Mar 21, 2024
@Kha
fix: restore default of stderrAsMessages
2b8dac8 
Puts trace.compiler back in the info view. Apparently an unintended change in #3014.
@Kha Kha mentioned this pull request Mar 21, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 21, 2024
@Kha
fix: restore default of stderrAsMessages (#3733)
085d019 
Puts trace.compiler back in the info view. Apparently an unintended
change in #3014.
@MithicSpirit MithicSpirit mentioned this pull request Jun 21, 2024
Open
@Kha Kha mentioned this pull request Jun 28, 2024
Merged
nomeata pushed a commit that referenced this pull request Jul 1, 2024
@Kha
fix: adapt kernel interruption to new cancellation system (#4584)
7f00767 
Kernel checks were not canceled on edit after #3014
github-merge-queue bot pushed a commit that referenced this pull request Aug 5, 2024
@Kha
feat: new snapshot architecture on the cmdline (#3106)
a3d144a 
This is #3014 with cad5cce reverted for testing.
@Kha Kha restored the het-snaps branch September 27, 2024 14:54
@Kha Kha deleted the het-snaps branch September 27, 2024 15:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tydeu tydeu tydeu left review comments

@mhuisi mhuisi mhuisi approved these changes

@joehendrix joehendrix Awaiting requested review from joehendrix

@Vtec234 Vtec234 Awaiting requested review from Vtec234 Vtec234 is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@Kha @leanprover-community-mathlib4-bot @leanprover-bot @tydeu @mhuisi