Skip to content

fix: @[nospecialize] is never template-like#12663

Merged
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-mvmqsvrsqqom
Feb 23, 2026
Merged

fix: @[nospecialize] is never template-like#12663
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-mvmqsvrsqqom

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Feb 23, 2026

This PR avoids false-positive error messages on specialization restrictions under the module system when the declaration is explicitly marked as not specializable. It could also provide some minor public size and rebuild savings.

@Kha
Copy link
Copy Markdown
Member Author

Kha commented Feb 23, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 23, 2026

Benchmark results for a7a4f89 against 8f80881 are in! @Kha

  • build//instructions: -559.9M (-0.00%)

Medium changes (2✅, 2🟥)

  • build/module/Lake.Build.Job.Monad//bytes .olean: -82kiB (-24.88%)
  • 🟥 build/module/Lake.Build.Job.Monad//bytes .olean.private: +84kiB (+24.04%)
  • build/module/Lake.Build.Job.Register//bytes .olean: -32kiB (-32.96%)
  • 🟥 build/module/Lake.Build.Job.Register//bytes .olean.private: +32kiB (+36.53%)

@Kha Kha added the changelog-compiler Compiler, runtime, and FFI label Feb 23, 2026
@Kha Kha enabled auto-merge February 23, 2026 20:00
@Kha Kha added this pull request to the merge queue Feb 23, 2026
Merged via the queue into leanprover:master with commit d0f8eb7 Feb 23, 2026
21 of 23 checks passed
@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 Feb 23, 2026
@mathlib-lean-pr-testing
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 8f80881c2f7611c61d0228dac94b27582b44d5d0 --onto e7e3588c973226e85d79ed0f3154cfca79b61c6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 20:35:50)

@leanprover-bot
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 8f80881c2f7611c61d0228dac94b27582b44d5d0 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 20:35:52)

@Kha Kha deleted the push-mvmqsvrsqqom branch February 24, 2026 10:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI 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.

4 participants