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

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

This PR reverts `PlausibleIterStep.yield`, `.skip`, and `.done` from
`abbrev` back to `def`. The change to `abbrev` in leanprover#12538 caused a ~32%
compiled performance regression in the iterators benchmark because the
compiler sees through `abbrev` to `Subtype.mk`, which prevents proper
fusion of iterator combinators like `filterMap`. This leads to
unnecessary intermediate `Option` heap allocations in tight loops.

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

This PR removes some spurious comments after #12538.

…12645)

This PR fixes a performance regression from #12538 caused by
`PlausibleIterStep.yield/skip/done` becoming abbreviation, which changes
the inlining behavior.

…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]>

…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]>

…e transparency (#12650)

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

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

* 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]>