Skip to content

fix: decLevel? should normalize#13352

Draft
kmill wants to merge 3 commits intomasterfrom
kmill_declevel
Draft

fix: decLevel? should normalize#13352
kmill wants to merge 3 commits intomasterfrom
kmill_declevel

Conversation

@kmill
Copy link
Copy Markdown
Collaborator

@kmill kmill commented Apr 9, 2026

No description provided.

@kmill kmill added the changelog-language Language features and metaprograms label Apr 9, 2026
@kmill kmill mentioned this pull request Apr 9, 2026
Closed
@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Apr 9, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 9, 2026 •
edited
Loading

Benchmark results for a0c73b2 against 4f6bcc5 are in. There are no significant changes. @kmill

  • ✅ build//instructions: -1.8G (-0.01%)

Medium changes (2🟥)

  • 🟥 compiled/liasolver//task-clock: +24ms (+12.74%)
  • 🟥 compiled/liasolver//wall-clock: +24ms (+12.62%)

Small changes (2✅, 1🟥)

  • ✅ build/module/Lean.Language.Lean//instructions: -51.0M (-0.69%)
  • 🟥 build/module/Lean.Meta.DecLevel//instructions: +39.9M (+2.87%)
  • ✅ build/module/Lean.Meta.Match.MatchEqs//instructions: -30.5M (-0.44%)

@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 Apr 9, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 9, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-09 19:47:15)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13352
0715737
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 9, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 9, 2026
Update lean-toolchain for testing leanprover/lean4#13352
054d40e
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 9, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 9, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13352
ee1f4e3
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 10, 2026
Update lean-toolchain for leanprover/lean4#13352
f545dfe
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 10, 2026

Mathlib CI status (docs):

@kmill
Copy link
Copy Markdown
Collaborator Author

kmill commented Apr 10, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 10, 2026 •
edited
Loading

Benchmark results for 1839eee against 4f6bcc5 are in. There are no significant changes. @kmill

  • ✅ build//instructions: -1.9G (-0.02%)

Small changes (1✅, 1🟥)

  • ✅ build/module/Lean.Language.Lean//instructions: -49.8M (-0.68%)
  • 🟥 build/module/Lean.Meta.DecLevel//instructions: +54.9M (+3.94%) (reduced significance based on *//lines)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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

@kmill @leanprover-radar @leanprover-bot