fix: detect stuck mvars through auxiliary parent projections by leodemoura · Pull Request #12564 · leanprover/lean4

leodemoura · 2026-02-18T19:09:50Z

This PR fixes getStuckMVar? to detect stuck metavariables through auxiliary parent projections created for diamond inheritance. These coercions (e.g., AddMonoid'.toAddZero') are not registered as regular projections because they construct the parent value from individual fields rather than extracting a single field. Previously, getStuckMVar? would give up when encountering them, preventing TC synthesis from being triggered.

Add AuxParentProjectionInfo environment extension to ProjFns.lean recording numParams and fromClass for these coercions
Register the info during structure elaboration in mkCoercionToCopiedParent
Consult the new extension in getStuckMVar? as a fallback when getProjectionFnInfo? returns none

🤖 Generated with Claude Code

leanprover-bot · 2026-02-18T21:25:14Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-17 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-02-18 21:25:13)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-22 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-02-23 01:11:34)

mathlib-lean-pr-testing · 2026-02-18T21:32:00Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-18 21:31:58) View Log

mathlib-lean-pr-testing · 2026-02-18T23:33:08Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-18 23:33:07) View Log

mathlib-lean-pr-testing · 2026-02-19T00:30:12Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 00:30:10) View Log

Replace temporary sorries with working proofs. Most fixes use `set_option backward.isDefEq.respectTransparency false in` to restore the pre-PR behavior for specific declarations. Co-Authored-By: Claude Opus 4.6 <[email protected]>

mathlib-lean-pr-testing · 2026-02-19T03:17:48Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 03:17:46) View Log

mathlib-lean-pr-testing · 2026-02-19T03:45:26Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 03:45:24) View Log

mathlib-lean-pr-testing · 2026-02-19T04:21:24Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 04:21:23) View Log

eric-wieser · 2026-02-19T05:32:14Z

Does this change mean that synthetic parent projections like Algebra.toModule (which are written manually) will not get the special treatment needed to fix this issue? Or is it the converse, that somehow the special treatment of auxiliary projections was the cause of the trouble in the first place?

kim-em · 2026-02-19T07:33:32Z

Does this change mean that synthetic parent projections like Algebra.toModule (which are written manually) will not get the special treatment needed to fix this issue? Or is it the converse, that somehow the special treatment of auxiliary projections was the cause of the trouble in the first place?

I think the answer here is just that these "manual projections" should be labelled @[instance_reducible], if they are initially set up as defs, and if they are defined as instance in the first place they should be fine.

mathlib-lean-pr-testing · 2026-02-19T07:49:21Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 07:49:19) View Log

mathlib-lean-pr-testing · 2026-02-19T07:59:32Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 07:59:30) View Log

JovanGerb · 2026-02-19T09:01:14Z

I agree with Eric's comment, that is seems like a bad idea to give different behaviour to manual projection instances compared to the non-direct projection instances generated by extends.

Rather, to maintain the previous behaviour, getStuckMVar? could make use of whnf (we would want this to be in at least the .instances transparency) in order to reduce the instances to actual projections. It already did this when encountering a previous .proj expression, but I think it should also be done when recursing into the major of e.g. Zero.zero.

mathlib-lean-pr-testing · 2026-02-19T11:21:05Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-19 11:21:03) View Log

This PR fixes `getStuckMVar?` to detect stuck metavariables through auxiliary parent projections created for diamond inheritance. These coercions (e.g., `AddMonoid'.toAddZero'`) are not registered as regular projections because they construct the parent value from individual fields rather than extracting a single field. Previously, `getStuckMVar?` would give up when encountering them, preventing TC synthesis from being triggered. The fix introduces `AuxParentProjectionInfo`, a new environment extension that records the `numParams` and `fromClass` information for these coercions. This information is registered during structure elaboration and consulted by `getStuckMVar?` as a fallback when `getProjectionFnInfo?` returns `none`. Co-Authored-By: Claude Opus 4.6 <[email protected]>

mathlib-lean-pr-testing · 2026-02-23T00:37:36Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-12564 build against this PR was cancelled. (2026-02-23 00:37:35) View Log

mathlib-lean-pr-testing · 2026-02-23T00:41:49Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-23 00:41:47) View Log

mathlib-lean-pr-testing · 2026-02-23T00:45:18Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-23 00:45:16) View Log

mathlib-lean-pr-testing · 2026-02-23T01:06:14Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12564 build failed against this PR. (2026-02-23 01:06:12) View Log

mathlib-lean-pr-testing · 2026-02-23T01:58:53Z

Mathlib CI status (docs):

🟡 Mathlib branch lean-pr-testing-12564 build against this PR was cancelled. (2026-02-23 01:58:52) View Log

kim-em · 2026-02-23T02:45:55Z

(Acknowledging @JovanGerb's unanswered comment above, which we will follow up with separately, but I am merging now as is.)

mathlib-lean-pr-testing · 2026-02-23T02:52:46Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-12564 built against this PR, but linting failed. (2026-02-23 02:52:44) View Log

mathlib-lean-pr-testing · 2026-02-23T14:13:13Z

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-12564 built against this PR, but linting failed. (2026-02-23 14:13:11) View Log

) This PR fixes the `adaptationNoteLinter` which was matching any line containing the substring `"daptation note"`, causing false positives on lines like: ```lean #adaptation_note /-- The maxHeartbeats bump is required after leanprover/lean4#12564. -/ set_option maxHeartbeats 400000 in -- see adaptation note ``` The linter now excludes lines containing `#adaptation_note` (correct usage) and `see adaptation note` (cross-references to a nearby `#adaptation_note` command). See https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22289522784/job/64474181031 for all 8 false positives, all of this form. 🤖 Prepared with Claude Code

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

…nprover-community#35668) This PR fixes the `adaptationNoteLinter` which was matching any line containing the substring `"daptation note"`, causing false positives on lines like: ```lean #adaptation_note /-- The maxHeartbeats bump is required after leanprover/lean4#12564. -/ set_option maxHeartbeats 400000 in -- see adaptation note ``` The linter now excludes lines containing `#adaptation_note` (correct usage) and `see adaptation note` (cross-references to a nearby `#adaptation_note` command). See https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/22289522784/job/64474181031 for all 8 false positives, all of this form. 🤖 Prepared with Claude Code

leodemoura added the changelog-language Language features and metaprograms label Feb 18, 2026

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 18, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 18, 2026

Update lean-toolchain for testing leanprover/lean4#12564

aa85353

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 Feb 18, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

Update lean-toolchain for testing leanprover/lean4#12564

22094a4

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 18, 2026

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

fixes for leanprover/lean4#12564

65bc770

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

fixes for leanprover/lean4#12564

d76b578

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

fixes for leanprover/lean4#12564

ef21e0e

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

fixes for leanprover/lean4#12564

9d6c6f8

kim-em added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026

fixes for leanprover/lean4#12564

84afd73

This was referenced Feb 19, 2026

Fix Mathlib.LinearAlgebra.SymplecticGroup leanprover-community/mathlib4-nightly-testing#182

Closed

Fix Mathlib.LinearAlgebra.SymplecticGroup leanprover-community/mathlib4-nightly-testing#183

Open

kim-em mentioned this pull request Feb 19, 2026

set_option ... in after decreasing_by with focused · tactic causes parse error #12573

Open

kim-em force-pushed the fix_aux_parent_proj branch from d50f0c4 to bfb9ec8 Compare February 22, 2026 23:26

kim-em force-pushed the fix_aux_parent_proj branch from bfb9ec8 to 47225ea Compare February 22, 2026 23:33

kim-em removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Feb 23, 2026

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

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-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 23, 2026

Update lean-toolchain for leanprover/lean4#12564

00225b0

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 23, 2026

Update lean-toolchain for leanprover/lean4#12564

8ceca61

kim-em changed the base branch from nightly-with-mathlib to master February 23, 2026 02:44

kim-em added this pull request to the merge queue Feb 23, 2026

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Feb 23, 2026

Merge branch 'master' into fix_aux_parent_proj

92a62a3

kim-em enabled auto-merge February 23, 2026 03:23

maxHeartbeats

0159139

kim-em added this pull request to the merge queue Feb 23, 2026

Merged via the queue into master with commit 70aa6bc Feb 23, 2026
15 checks passed

Conversation

leodemoura commented Feb 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Feb 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

eric-wieser commented Feb 19, 2026

Uh oh!

kim-em commented Feb 19, 2026

Uh oh!

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

Uh oh!

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

Uh oh!

JovanGerb commented Feb 19, 2026

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

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

Uh oh!

kim-em commented Feb 23, 2026

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

leodemoura commented Feb 18, 2026 •

edited

Loading

leanprover-bot commented Feb 18, 2026 •

edited

Loading