Skip to content

perf: restrict nontrivial class projection classification to reducible transparency#12650

Merged
kim-em merged 1 commit intomasterfrom
perf-reducibleClassField-transparency
Feb 23, 2026
Merged

perf: restrict nontrivial class projection classification to reducible transparency#12650
kim-em merged 1 commit intomasterfrom
perf-reducibleClassField-transparency

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Feb 23, 2026

This PR fixes a performance regression introduced by enabling backward.whnf.reducibleClassField (#12538). The isNonTrivialRegular function in ExprDefEq was classifying class projections as nontrivial at all transparency levels, but the extra .instances reduction in unfoldDefault that motivates this classification only applies at .reducible transparency. At higher transparency levels, the nontrivial classification caused unnecessary heuristic comparison attempts in isDefEqDelta that cascaded through BitVec reductions, causing elaboration of Lean.Data.Json.Parser to double from ~3.6G to ~7.2G instructions.

The fix restricts the nontrivial classification to .reducible transparency only, matching the scope of unfoldDefault's extra reduction behavior.

🤖 Prepared with Claude Code

@kim-em kim-em added the changelog-language Language features and metaprograms label Feb 23, 2026
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Feb 23, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Feb 23, 2026 •
edited
Loading

Benchmark results for c3d6274 against 8b04403 are in! @kim-em

  • 🟥 build exited with code -1
  • 🟥 other exited with code -1

No significant changes detected.

@kim-em @claude
perf: restrict nontrivial class projection classification to reducibl…
ef68135 
…e transparency

This PR fixes a performance regression introduced by enabling
`backward.whnf.reducibleClassField` (PR #12538). The `isNonTrivialRegular`
function in `ExprDefEq` was classifying class projections as nontrivial at all
transparency levels, but the extra `.instances` reduction in `unfoldDefault`
that motivates this classification only applies at `.reducible` transparency.
At higher transparency levels, the nontrivial classification caused unnecessary
heuristic comparison attempts in `isDefEqDelta` that cascaded through BitVec
reductions, causing elaboration of `Lean.Data.Json.Parser` to double from
~3.6G to ~7.2G instructions.

The fix restricts the nontrivial classification to `.reducible` transparency
only, matching the scope of `unfoldDefault`'s extra reduction behavior.

Co-Authored-By: Claude Opus 4.6 <[email protected]>
@kim-em kim-em force-pushed the perf-reducibleClassField-transparency branch from c3d6274 to ef68135 Compare February 23, 2026 13:03
@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-lean-pr-testing bot commented Feb 23, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8b0440383037ffbd1e992368277c4da4211b6c88 --onto 2e7fe7e79d151ee91039f086b8036252cdf9b725. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 13:57:06)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Feb 23, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8b0440383037ffbd1e992368277c4da4211b6c88 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 13:57:08)

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 23, 2026
@kim-em
fixes for leanprover/lean4#12650
7aa8334
@kim-em kim-em added this pull request to the merge queue Feb 23, 2026
@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 Feb 23, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Feb 23, 2026

Mathlib CI status (docs):

Merged via the queue into master with commit ed0fd1e Feb 23, 2026
23 checks passed
kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 1, 2026
@mathlib-nightly-testing @kim-em
@Ruben-VandeVelde @claude @joelriou @kmill @Kha @sgraf812
chore: adaptations for nightly-2026-02-25 (#192)
c19e7bb 
* revert changes to GCongr

* fix tests output again

* fix

* maxheartbeats

* fix

* chore: bump to nightly-2026-02-12

* merge lean-pr-testing-12412

* bump toolchain (early today, oops!)

* fix lakefile and lake update

* remove upstreamed

* restore a simp

* remove upstreamed and deprecation

* deprecation

* clarify adaptation note

* lake update

* fix for leanprover/lean4#11744

* fix indentation

* chore: bump to nightly-2026-02-13-rev1

* chore: bump to nightly-2026-02-13-rev2

* fix test

* fix test

* nice, most workarounds not needed with univ_out_params

* chore: bump to nightly-2026-02-14

* chore: update batteries for List.reverse_singleton fix

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* .

* add @[univ_out_params] where universe params are not determined by inputs

Classes like `Category.{v}`, `HasLimitsOfSize.{v₁,u₁}`, `Functor.IsContinuous.{t}`,
and `UCompactlyGeneratedSpace.{u}` have universe parameters that do not appear in
their input parameter types. With the new TC resolution cache (lean4#12286), these
default to output parameters, causing cache collisions when the same class is queried
at different universe levels.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add #adaptation_note for @[univ_out_params] annotations

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* add library note on universe output parameters, update adaptation notes

Adds a library note in Category/Basic.lean explaining how `@[univ_out_params]`
interacts with the TC resolution cache, with concrete examples of when universe
parameters should and should not be treated as outputs.

Updates all adaptation notes to use a shorter form referencing this library note.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* convert #adaptation_note to -- comments for univ_out_params annotations

These are permanent annotations, not temporary workarounds, so
#adaptation_note is the wrong mechanism. Use regular comments placed
after the doc-string and before the @[univ_out_params] attribute.

Also restore the reference to lean4#12423 alongside lean4#12286.

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fix

* fix

* fix

* fix

* empty commit to retrigger CI

* chore: bump to nightly-2026-02-15

* lake update

* chore: bump to nightly-2026-02-15-rev1

* lake update

* chore: bump to nightly-2026-02-16

* Update lean-toolchain for leanprover/lean4#12179

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-15-rev1 (#177)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* fix warning

* fix

* fix properly

* chore: adaptations for nightly-2026-02-16 (#179)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>

* Merge master into nightly-testing

* chore: bump to nightly-2026-02-16-rev1

* move batteries back to nightly-testing

* lake update

* final fixes for leanprover/lean4#1279

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* fix for leanprover/lean4#12179

* chore: adaptations for nightly-2026-02-16-rev1 (#180)

* fix_backward_defeq script

* lake update batteries

* non-local set_option, added manually

* manual fixes, script confused by absence of blank lines

* times out without manual fix

* norm_num tests

* reduce_mod_char

* fix test output

* set_option globally in RingTheory.SimpleModule.Isotypic

* set_option globally in RingTheory.Adjoin.Dimension

* set_option a section of LinearAlgebra.FiniteDimensional.Basic

* set_option globally in Algebra.Homology.BifunctorAssociator

* set_option in section in Algebra.Homology.BifunctorHomotopy

* set_option globally in Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances

* set_option globally in Algebra.Homology.BifunctorShift

* set_option in section in Geometry.Manifold.Riemannian.Basic

* set_option in section in NumberTheoryCyclotomic.Basic

* set_option in section in Analysis.Distribution.SchwartzSpace.Fourier

* global set_option in RingTheory.DedekindDomain.LinearDisjoint

* manual fixes for CategoryTheory.Monoidal.DayConvolution.Closed

* manual fixes for CategoryTheory.Sites.Descent.IsStack

* manual fixes for Algebra.Homology.DifferentialObject

* manual fixes for Geometry.RingedSpace.PresheafedSpace

* manual fixes for CategoryTheory.Triangulated.Opposite.Functor

* manual fixes in Algebra.Homology.HomotopyCategory.ShortExact

* manual fixes for Geometry.RingedSpace.PresheafedSpace.Gluing

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* manual fixes to CategoryTheory.Sites.Descent.DescentData

* manual fixes, script confused by absence of blank lines, and a module-doc that should have been a doc-string

* adaptation_note

* x: ./fix_backward_defeq.py

* x: ./fix_backward_defeq.py

* set_option linter.style.longFile

* remove unused simp args

* remove noop tactic

* lake update

* optimistic linter fixes

* patch and adaptation note

* slightly more care with the linter

* still getting it right

* fix test

* chore: adaptations for nightly-2026-02-16-rev1

* fix lakefile and manifest

* remove fix_backward_defeq.py

---------

Co-authored-by: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-17

* chore: remove fix_backward_defeq.py (no longer needed)

* Update lean-toolchain for testing leanprover/lean4#12538

* Update lean-toolchain for testing leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* fixes for leanprover/lean4#12564

* temporary sorries to get further through the build

* fixes for sorries

* more set_option

* blech

* more fixes

* cleanup

* remove 316 set_options

* fix Algebra.Category.ModuleCat.Differentials.Presheaf

* remove unnecessary set_option

* remove more set_option backward.isDefEq.respectTransparency false

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-19

* chore: adaptations for nightly-2026-02-19

Rename instanceReducible to implicitReducible (lean4#12529).
Update batteries for upstreamed List.scanl/scanr (lean4#12452)
and Nat.Digits (lean4#12445).

* pre-emptively set toolchain

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* Update lean-toolchain for leanprover/lean4#12572

* remove set_option

* remove set_option

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12572

* fixes for leanprover/lean4#12538

* remove more

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* fixes for leanprover/lean4#12538

* fixes for leanprover/lean4#12538

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#12603

* chore: bump to nightly-2026-02-20

* fixes for leanprover/lean4#12538

* fixes

* Update lean-toolchain for testing leanprover/lean4#12625

* fix

* chore: adaptations for nightly-2026-02-20

* Merge master into nightly-testing

* fix

* chore: bump to nightly-2026-02-21

* chore: adaptations for nightly-2026-02-21

* Update lean-toolchain for leanprover/lean4#12625

* fix

* fixes

* fix

* Update lean-toolchain for leanprover/lean4#12538

* fixes

* fixes

* fixes

* chore: bump to nightly-2026-02-22

* fix cexample

* fix test

* Update lean-toolchain for leanprover/lean4#12625

* chore: adapt to mkHole type change from lean4#12459

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: adaptations for nightly-2026-02-22

* lake update

* bump batteries

* fixes

* Update lean-toolchain for leanprover/lean4#12564

* set_option

* set_option

* set_option

* fix(Linter/TextBased): don't flag "see adaptation note" comments

The `adaptationNoteLinter` was matching any line containing the
substring "daptation note", which caused false positives on lines
like `set_option maxHeartbeats 400000 in -- see adaptation note`
that merely reference a nearby `#adaptation_note` command.

Exclude lines containing `#adaptation_note` (correct usage) and
lines containing `see adaptation note` (cross-references).

Co-Authored-By: Claude Opus 4.6 <[email protected]>

* chore: bump to nightly-2026-02-23

* fixes

* adaptation notes

* fixes

* fixes

* fixes

* lint

* fix

* fix

* fix test

* fixes for leanprover/lean4#12650

* chore: adaptations for nightly-2026-02-23

* chore: bump to nightly-2026-02-23-rev1

* merge lean-pr-testing-12650

* chore: bump to nightly-2026-02-23-rev2

* x: scripts/add_set_option.py

* chore: bump to nightly-2026-02-25

* scripts/add_set_option.py

* fixes

* fixes

* fix

* fixes

* chore: bump to nightly-2026-02-25

* merge lean-pr-testing-12603

* bump batteries

* what happened there?

* lake update

* lake update aesop

* fixes

* chore: adaptations for nightly-2026-02-25

---------

Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Claude Opus 4.6 <[email protected]>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>
@kim-em kim-em mentioned this pull request Mar 3, 2026
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 3, 2026
@kim-em @claude
chore: add HACK banner to isNonTrivialRegular transparency check (#12769
9a84112 
)

This PR adds a HACK comment to the transparency restriction in
`isNonTrivialRegular` (from
#12650) so it's not forgotten.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <[email protected]>
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 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

@kim-em @leanprover-radar @leanprover-bot