Skip to content

Conversation

@mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Oct 15, 2025

This PR revamps the server logging mechanism to allow filtering the log output by LSP method.

@mhuisi mhuisi added the changelog-server Language server, widgets, and IDE extensions label Oct 15, 2025
@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 Oct 15, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 15, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80b8e44072aa9f940c74b71b57386ce22fc9ea2b --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-15 13:28:44)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dec007693a6a0e097623158a95642cc78cdff97f --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-24 15:07:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dec007693a6a0e097623158a95642cc78cdff97f --onto 3a42ee0c3060e2a8365927d205ead5990366053d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-28 11:38:37)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 15, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 80b8e44072aa9f940c74b71b57386ce22fc9ea2b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-15 13:28:46)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dec007693a6a0e097623158a95642cc78cdff97f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-24 15:07:28)

@mhuisi mhuisi added this pull request to the merge queue Oct 24, 2025
mhuisi added a commit to leanprover/vscode-lean4 that referenced this pull request Oct 24, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 24, 2025
@mhuisi mhuisi force-pushed the mhuisi/better-server-logging branch 2 times, most recently from 78e8274 to d55b925 Compare October 24, 2025 22:14
@mhuisi mhuisi force-pushed the mhuisi/better-server-logging branch from d55b925 to 0fecd0c Compare October 24, 2025 23:00
@mhuisi mhuisi added this pull request to the merge queue Oct 28, 2025
Merged via the queue into leanprover:master with commit 19533ab Oct 28, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Development

Successfully merging this pull request may close these issues.

3 participants