Skip to content

feat: persist logLintExt data at server level - #14387

Merged
wkrozowski merged 3 commits into
leanprover:masterfrom
wkrozowski:wojciech/logLintExt
Jul 15, 2026
Merged

feat: persist logLintExt data at server level#14387
wkrozowski merged 3 commits into
leanprover:masterfrom
wkrozowski:wojciech/logLintExt

Conversation

@wkrozowski

@wkrozowski wkrozowski commented Jul 14, 2026

Copy link
Copy Markdown
Contributor

This PR changes the level at which logLintExt data is persisted to server. Previously, it was all persisted at public level, thus causing negative performance regression.

@wkrozowski
wkrozowski requested a review from Kha July 14, 2026 15:04
@wkrozowski
wkrozowski requested a review from tydeu as a code owner July 14, 2026 15:04
@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Jul 14, 2026
@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 Jul 14, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 14, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto 12c859a4d735fbcdb3ebbddb42dcc8619bcc7a7d. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-14 15:55:21)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-15 11:15:30)

@leanprover-bot

leanprover-bot commented Jul 14, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto 7847ce51363794755252279e6732240bd4f27ca8. You can force reference manual CI using the force-manual-ci label. (2026-07-14 15:55:23)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 46cf2b9ead5df46fbb91e45cf58e5764717767d5 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-15 11:15:32)

@wkrozowski
wkrozowski added this pull request to the merge queue Jul 15, 2026
Merged via the queue into leanprover:master with commit 3c8321c Jul 15, 2026
17 checks passed
wrenna-robson pushed a commit to wrenna-robson/lean4 that referenced this pull request Jul 17, 2026
@wkrozowski @wrenna-robson
feat: persist logLintExt data at server level (leanprover#14387)
5f6cd49 
This PR changes the level at which `logLintExt` data is persisted to
`server`. Previously, it was all persisted at `public` level, thus
causing negative performance regression.
robsimmons pushed a commit that referenced this pull request Jul 29, 2026
@wkrozowski @robsimmons
feat: persist logLintExt data at server level (#14387)
25459eb 
This PR changes the level at which `logLintExt` data is persisted to
`server`. Previously, it was all persisted at `public` level, thus
causing negative performance regression.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Kha Kha Kha approved these changes
@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms 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

@wkrozowski @leanprover-bot @Kha