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: parallel progress notifications #6329

Merged
merged 3 commits into from
Feb 7, 2025
Merged

feat: parallel progress notifications #6329

merged 3 commits into from
Feb 7, 2025

Conversation

Kha
Copy link
Member

@Kha Kha commented Dec 6, 2024

This PR enables the language server to present multiple disjoint line ranges as being worked on. Even before parallelism lands, we make use of this feature to show post-elaboration tasks such as kernel checking on the first line of a declaration to distinguish them from the final tactic step.

image

@Kha Kha requested a review from mhuisi as a code owner December 6, 2024 16:59
@Kha Kha added server Affects the Lean server code changelog-server Language server, widgets, and IDE extensions and removed server Affects the Lean server code labels Dec 6, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 6, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 6, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6329
1fd3e25
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 6, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6329
79213a7
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 6, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 6, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-6329 has successfully built against this PR. (2024-12-06 18:27:04) View Log
  • ✅ Mathlib branch lean-pr-testing-6329 has successfully built against this PR. (2025-01-14 13:51:25) View Log
  • ✅ Mathlib branch lean-pr-testing-6329 has successfully built against this PR. (2025-01-28 13:53:40) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c6cb2f52f028882ff821394f447d569898546803 --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-05 13:52:44)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7c79f05cd404a83973eb613eb10c3445405e53a0 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 16:54:38)

mhuisi
mhuisi reviewed Jan 9, 2025
View reviewed changes
src/Lean/Server/FileWorker.lean Show resolved Hide resolved
src/Lean/Server/FileWorker.lean Outdated Show resolved Hide resolved
src/Lean/Server/FileWorker.lean Outdated Show resolved Hide resolved
src/Lean/Server/FileWorker.lean Show resolved Hide resolved
src/Lean/Server/FileWorker.lean Outdated Show resolved Hide resolved
@Kha Kha force-pushed the push-vorkpouuxruv branch 3 times, most recently from e60b4a7 to b7e5478 Compare January 14, 2025 12:39
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6329
3d37878
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 14, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6329
1247ea8
@Kha Kha force-pushed the push-vorkpouuxruv branch from b7e5478 to 4381b6c Compare January 28, 2025 12:44
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 28, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6329
d0d659f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 28, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6329
29a8587
@mhuisi mhuisi mentioned this pull request Jan 31, 2025
Open
@Kha Kha force-pushed the push-vorkpouuxruv branch from 4381b6c to efec3d6 Compare February 5, 2025 13:26
@Kha Kha enabled auto-merge February 5, 2025 13:26
@Kha Kha force-pushed the push-vorkpouuxruv branch from efec3d6 to 2681068 Compare February 5, 2025 13:27
@Kha Kha added this pull request to the merge queue Feb 5, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 5, 2025
@Kha Kha force-pushed the push-vorkpouuxruv branch from 2681068 to 7769118 Compare February 6, 2025 16:47
@Kha Kha requested review from TwoFX and kim-em as code owners February 6, 2025 16:47
@Kha Kha force-pushed the push-vorkpouuxruv branch from 7769118 to 7a1929a Compare February 6, 2025 16:52
@Kha Kha added the release-ci Enable all CI checks for a PR, like is done for releases label Feb 6, 2025
@Kha Kha force-pushed the push-vorkpouuxruv branch 6 times, most recently from 2a152af to 4619576 Compare February 7, 2025 12:25
@Kha Kha removed the release-ci Enable all CI checks for a PR, like is done for releases label Feb 7, 2025
@Kha Kha force-pushed the push-vorkpouuxruv branch from 4619576 to 7153ebf Compare February 7, 2025 15:35
@Kha Kha enabled auto-merge February 7, 2025 15:35
@Kha Kha force-pushed the push-vorkpouuxruv branch from 7153ebf to 3b8f56d Compare February 7, 2025 16:27
@Kha Kha added this pull request to the merge queue Feb 7, 2025
Merged via the queue into leanprover:master with commit 0d1907c Feb 7, 2025
15 checks passed
@Kha Kha deleted the push-vorkpouuxruv branch February 10, 2025 08:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@mhuisi mhuisi mhuisi approved these changes

@TwoFX TwoFX Awaiting requested review from TwoFX

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-server Language server, widgets, and IDE extensions 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.
3 participants
@Kha @leanprover-community-bot @mhuisi