feat: name the functional argument to brecOn in structural recursion by nomeata · Pull Request #12987 · leanprover/lean4

nomeata · 2026-03-19T14:29:28Z

This PR extracts the functional (lambda) passed to brecOn in structural
recursion into a named _f helper definition (e.g. foo._f), similar to
how well-founded recursion uses ._unary. This way the functional shows up
with a helpful name in kernel diagnostics rather than as an anonymous lambda.

The _f definition is added with .regular kernel reducibility hints and
the @[reducible] elaborator attribute. For inductive predicates, the
previous inline lambda behavior is kept.

Using .regular rather than .abbrev kernel hints is important for
performance: with .abbrev, the kernel's lazy_delta_reduction_step
always unfolds _f before other definitions (since .abbrev has the
lowest priority in compare()), and the "compare arguments before
unfolding" optimization (which only fires for .regular heads with the
same definition on both sides of a defeq check) cannot apply. This causes
the kernel to eagerly unfold the _f → brecOn → casesOn chain,
leading to deep recursion errors in tests like bv_decide. With
.regular hints, height-based comparison delays _f unfolding
appropriately, and the argument-comparison optimization avoids unnecessary
unfolding entirely.

This change improves code size (a bit). It may regress kernel reduction times,
especially if a function defined by structural recursion is used in kernel reduction
proofs on the hot path. Functions defined by structural recursion are not particularly
fast to reduce anyways (due to the .brecOn construction), so already now it may be
worth writing a kernel-reduction-friendly function manually (using the recursor directly,
avoiding overloaded operations). This change will guide you in knowing which function to
optimize.

🤖 Generated with Claude Code

This PR extracts the functional (lambda) passed to `brecOn` in structural recursion into a named `_f` helper definition (e.g. `foo._f`), similar to how well-founded recursion uses `._unary`. This way the functional shows up with a helpful name in kernel diagnostics rather than as an anonymous lambda. The `_f` definition is added as a reducible abbreviation. For inductive predicates and nested inductives with unused type formers, we fall back to the previous inline lambda behavior. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

These tests only care about the signature, not the definition body. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-19T14:52:53Z

!radar

leanprover-radar · 2026-03-19T14:53:00Z

Benchmark results for 2602bf2 against 61a3443 are in. Significant changes detected! @nomeata

🟥 build//instructions: +13.9G (+0.11%)
🟥 other exited with code 2

Large changes (2✅)

✅ size/Init/.olean//bytes: -881kiB (-0.97%)
✅ size/all/.olean//bytes: -2MiB (-0.76%)

Medium changes (3🟥)

🟥 build/module/Init.Data.Array.Extract//instructions: +1.0G (+2.53%)
🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +1.3G (+0.94%)
🟥 build/stat/imported consts//amount: +842.1k (+1.23%)

Small changes (8✅, 76🟥)

Too many entries to display here. View the full report on radar instead.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Each function now gets its own `_f` definition from its individual functional argument. For single-function position groups, the `_f` constant is referenced in the packed brecOn argument (showing in kernel diagnostics). For multi-function groups, the packed functional stays inline to preserve FunInd behavior, but individual `_f` defs still exist. This also removes the `positions.all (\!·.isEmpty)` restriction, so `_f` is created even for nested inductives with unused type formers. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

leanprover-bot · 2026-03-19T16:16:39Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-18 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-03-19 16:16:38)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1362cc60415fc461a2a6c61e15d0a8b6d895d120 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 19:18:44)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-19-rev1 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-03-21 18:34:51)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8f6411ad576cc0bec3e9a891c60df223da300a71 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-22 18:30:14)

- Remove try/catch around _f axiom creation (no expected failures) - Use ElimRecResult struct instead of tuple for clarity - Pass function type to mkBRecOnMotive instead of using inferType - Simplify _f axiom creation (use addDecl directly instead of addAsAxiom) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This PR separates the `withoutModifyingEnv` for `preprocess` from the one covering `getFixedParamPerms` through `elimMutualRecursion`, making the axiom requirements of each phase explicit. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This PR splits `tryAllArgs` into two phases: `findRecArgCandidates` precomputes all candidate argument combinations (the part needing function axioms), and `tryCandidates` runs the retry loop using `Meta.saveState`/`restore` for proper environment backtracking instead of `withoutModifyingEnv`. This removes the inner `withoutModifyingEnv` around `elimMutualRecursion`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…hase This PR removes the `tryAllArgs` wrapper, calling `findRecArgCandidates` and `tryCandidates` directly. Each phase that needs function axioms has its own `withoutModifyingEnv` + `addAsAxiom` pair: `preprocess`, `getFixedParamPerms`, `findRecArgCandidates`, and the `tryCandidates` callback. The `withoutModifyingEnv` in `tryCandidates` is moved into the callback alongside the axiom additions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…s callback Move the body of `structuralRecursion` that follows `inferRecArgPos` into a callback that runs inside the `tryCandidates` backtracking loop but outside `withoutModifyingEnv`. This allows `_f` helper definitions and non-recursive definitions to be added directly within the backtracking context. Introduce `TM = StateRefT State TermElabM` alongside the existing `M = StateRefT State MetaM` so the callback can call `TermElabM` functions like `addNonRec` and `addAndCompilePartialRec`. `M` functions lift to `TM` via an explicit `MonadLift` instance. `tryCandidates` moves from `FindRecArg.lean` to `Main.lean` and now also saves/restores `Structural.State` on backtracking. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Extract the repeated `withoutModifyingEnv` + `addAsAxiom` pattern into a `withRecFunsAsAxioms` helper with a docstring explaining its purpose and limitations. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This reverts the callback-style `inferRecArgPos` and `TM` monad (commit d1138cc), restoring the simpler tuple-returning approach where post-processing happens after `run`. The `tryCandidates` function moves back to `FindRecArg.lean`. The `withRecFunsAsAxioms` helper is kept. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This stores the functional types in ElimRecResult (avoiding redundant inferType calls) and uses addDecl directly instead of the heavier addNonRec for _f helper definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…etaM This removes the global M = StateRefT State MetaM monad from structural recursion elaboration. The State was only needed to collect matcher side-effects from mkBelowMatcher in the inductive predicate case. Instead, mkIndPredBRecOnF now returns matchers explicitly as part of its result, and replaceIndPredRecApps uses a local IndPredM monad. All other functions work in plain MetaM. The _f definitions are now added directly in elimMutualRecursion using addDecl, and withRecFunsAsAxioms is scoped narrowly around the functions that need it. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This removes the now-single-field ElimRecResult structure, replacing it with a plain Array PreDefinition return type from elimMutualRecursion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This uses mkForallFVars on the already-computed FTypes to get the closed _f types, avoiding a redundant inferType call on each fValue. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This uses a single recArgInfos.mapIdxM with the isIndPred branch inside the callback, wrapping withRecFunsAsAxioms around each individual mkBRecOnF/mkIndPredBRecOnF call. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This removes the poss.size == 1 check and references _f constants in the packed functionals for all position groups, not just singletons. This ensures _f definitions show up in kernel diagnostics for multi-function position groups as well. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Structural recursion now creates `_f` auxiliary definitions to make the functional arguments visible in kernel diagnostics. FunInd needs to see through these definitions to split induction principles into per-constructor cases. Add a case in `buildInductionBody` that unfolds constant applications taking `oldIH` as an argument, mirroring the existing pattern in `foldAndCollect`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Update `letToHaveCleanup.lean` for `let` vs `have` in `_f` type (inferred type uses `let`, not the user-facing `have`). Update `issue6281.lean` for `_f` proof terms now visible as `sorry` after FunInd unfolds `_f` definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Apply `Meta.letToHave` to the `_f` value and type before adding the declaration, so that `let` bindings in user code are properly displayed as `have` in the `_f` definition. Update `issue6281.lean` test expectations for `_f` proof terms now visible as `sorry` after FunInd unfolds `_f` definitions. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-20T18:21:55Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12987 has successfully built against this PR. (2026-03-20 18:21:53) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1362cc60415fc461a2a6c61e15d0a8b6d895d120 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 19:18:42)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-19-rev1 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-21 18:34:50)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8f6411ad576cc0bec3e9a891c60df223da300a71 --onto 90b5e3185b3b948ce1c75281d3e95f370c8493a6. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-22 18:30:13)

…chim/namedF

This reverts commit 3115752.

This reverts commit 13a67dc.

Use `.regular` reduction hints instead of `.abbrev` for `_f` definitions to prevent the kernel from eagerly unfolding them, which could cause timeouts (e.g. in bv_decide tests where the kernel enters an infinite Nat.brecOn unfolding chain). The `@[reducible]` attribute is kept so the elaborator can still unfold `_f` as needed. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-22T11:43:32Z

!radar

leanprover-radar · 2026-03-22T11:43:39Z

Benchmark results for 2c6049f against 90b5e31 are in. Significant changes detected! @nomeata

🟥 build//instructions: +12.5G (+0.10%)

Large changes (4✅, 2🟥)

✅ elab/big_beq_rec//instructions: -711.0M (-3.77%)
✅ elab/big_deceq_rec//instructions: -192.1M (-2.99%)
🟥 elab/string_simp_ne//instructions: +254.9M (+4.41%)
🟥 misc/leanchecker --fresh Init//instructions: +8.3G (+2.29%)
✅ size/Init/.olean//bytes: -796kiB (-0.87%)
✅ size/all/.olean//bytes: -2MiB (-0.68%)

Medium changes (10🟥)

🟥 build/module/Init.Data.Array.Extract//instructions: +1.1G (+2.66%)
🟥 build/module/Init.Data.BitVec.Lemmas//instructions: +1.2G (+0.92%)
🟥 build/module/Lean.Meta.Tactic.FunInd//instructions: +4.0G (+6.31%) (reduced significance based on absolute threshold)
🟥 build/stat/imported consts//amount: +856.9k (+1.23%)
🟥 elab/big_omega//instructions: +210.9M (+0.88%)
🟥 elab/big_omega_MT//instructions: +208.8M (+0.87%)
🟥 elab/charactersIn//instructions: +204.5M (+0.42%)
🟥 elab/reduceMatch//instructions: +315.7M (+2.25%)
🟥 elab/simp_arith1//instructions: +54.8M (+2.29%)
🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +1.2G (+0.99%)

Small changes (26✅, 64🟥)

Too many entries to display here. View the full report on radar instead.

mathlib-lean-pr-testing · 2026-03-22T13:07:53Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-12987 build failed against this PR. (2026-03-22 13:07:51) View Log

Nat.add._f only exists in stage2. Use a local myAdd definition so the test works in stage1 too. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-22T15:56:03Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12987 has successfully built against this PR. (2026-03-22 15:56:00) View Log

# Conflicts: # tests/elab/1024.lean.out.expected # tests/elab/1237.lean.out.expected # tests/elab/3965_2.lean.out.expected # tests/elab/issue6281.lean.out.expected

Use `.abbrev` reducibility hints for `_f` definitions instead of `.regular`. This ensures the kernel always unfolds `_f` before other definitions in `lazy_delta_reduction_step`, avoiding deep recursion when `_f` (with low height) faces definitions like `Nat.sub` (with higher height) during definitional equality checks on large nat literals. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata · 2026-03-22T22:16:38Z

Analysis of stage2 test failures

With _f definitions referenced in the brecOn term, two tests fail on stage2 with (kernel) deep recursion detected: elab/854.lean and elab/grind_cutsat_omega.lean. Neither .regular nor .abbrev reducibility hints resolve both.

Root cause

Naming the functional as a constant (Nat.add._f) injects it into the kernel's lazy_delta_reduction_step height comparison. With inline lambdas (pre-PR behavior), the functional beta-reduces in whnf_core without entering delta reduction. With a named constant, the kernel must choose an unfolding order via compare on reducibility hints.

`.regular` hints (current)

Nat.add._f gets height 0–1 (its body references only .abbrev definitions like Nat.brecOn.go and constructors). When the kernel checks e.g. Nat.add._f 0 PUnit.unit (Nat.sub a N) =?= Nat.sub a N, it compares heights: Nat.add._f (1) vs Nat.sub (3) → unfolds Nat.sub first → tries to reduce Nat.sub a 100000000 via brecOn → C++ stack overflow.

No height computation helps: the brecOn-based function bodies simply don't reference .regular definitions, so any height derived from the _f value or the main definition value is low. And even artificially high heights cascade to the parent definition (since Nat.add references Nat.add._f), making OTHER functions' parents also high — preserving the relative ordering problem.

`.abbrev` hints

_f always unfolds before .regular definitions → fixes 854/grind_cutsat_omega. But causes deep recursion in elab/6043.lean and elab/bv_llvm.lean (both use bv_decide), where eagerly unfolding _f leads to larger intermediate terms that overflow the stack.

The failing tests in detail

854.lean: User writes apply Nat.succ_le_succ on goal (a - 100000000) + 1 ≤ 1. Nat.succ_le_succ : n ≤ m → n.succ ≤ m.succ, so the kernel must check Nat.succ ?n =?= (a - N) + 1. This is a valid def-eq that works without _f (inline lambda beta-reduces). With _f, the height mismatch sends the kernel down the wrong unfolding path. Writing Nat.succ (a - N) ≤ 1 instead of (a - N) + 1 ≤ 1 avoids the issue, confirming the problem is specifically in the Nat.add unfolding path.

grind_cutsat_omega: grind normalizes 2^64 to literal 18446744073709551615 during its simp phase, then produces a proof term that requires a def-eq check involving Nat.add/Nat.sub on this literal. omega on the same goal works fine — it produces a different proof structure that avoids the problematic def-eq. The grind proof term is valid; the issue is purely in the kernel's unfolding order with _f.

Options

Don't reference _f in brecOn: preserves kernel behavior perfectly, _f exists in env for tooling but isn't in the computation path. Defeats the diagnostic purpose.
Kernel change: add a new hint kind or special-case _f in lazy_delta_reduction_step. Currently considered out of scope.
Fix the tactics: not applicable — the proof terms are valid, the issue is in the kernel's heuristic unfolding order.

nomeata added the changelog-language Language features and metaprograms label Mar 19, 2026

nomeata and others added 5 commits March 19, 2026 14:32

test: use #check instead of #print for Dorais1 and def6 tests

8e2c328

These tests only care about the signature, not the definition body. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: move structuralNamedF tests to tests/elab/

049e324

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: use #guard_msgs throughout structuralNamedF tests

f958971

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: add kernel diagnostics test showing _f in structuralNamedF

f1a99fc

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

test: verify fib._f appears in kernel diagnostics

2602bf2

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

nomeata and others added 2 commits March 19, 2026 15:01

test: remove redundant structuralNamedF_debug test

4524bc0

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

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

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

Update lean-toolchain for testing leanprover/lean4#12987

5cdbbe1

nomeata and others added 16 commits March 19, 2026 16:19

refactor: introduce withRecFunsAsAxioms helper

6cecf3f

Extract the repeated `withoutModifyingEnv` + `addAsAxiom` pattern into a `withRecFunsAsAxioms` helper with a docstring explaining its purpose and limitations. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: remove ElimRecResult wrapper from structural recursion

fa08bc9

This removes the now-single-field ElimRecResult structure, replacing it with a plain Array PreDefinition return type from elimMutualRecursion. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: derive _f types from FTypes instead of re-inferring

af1e239

This uses mkForallFVars on the already-computed FTypes to get the closed _f types, avoiding a redundant inferType call on each fValue. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

refactor: use single mapIdxM for FArgs computation

7473122

This uses a single recArgInfos.mapIdxM with the isIndPred branch inside the callback, wrapping withRecFunsAsAxioms around each individual mkBRecOnF/mkIndPredBRecOnF call. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 20, 2026

nomeata marked this pull request as ready for review March 21, 2026 09:14

nomeata requested a review from leodemoura as a code owner March 21, 2026 09:14

Deprecated funcitons

7f78c99

nomeata added this pull request to the merge queue Mar 21, 2026

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

nomeata and others added 9 commits March 21, 2026 17:05

Trigger stage0 update

365d289

Update test

a72acb3

Merge branch 'master' of https://github.com/leanprover/lean4 into joa…

94c514f

…chim/namedF

More tstack bumps

13a67dc

try irredId (does not help)

3115752

Revert "try irredId (does not help)"

d9cced0

This reverts commit 3115752.

Revert "More tstack bumps"

8a57657

This reverts commit 13a67dc.

Not needed anymore?

2c6049f

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

Update lean-toolchain for leanprover/lean4#12987

0000a55

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

Update lean-toolchain for leanprover/lean4#12987

68191b1

mathlib-lean-pr-testing bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Mar 22, 2026

fix: ppMotives test uses user-defined function for _f printing

1d611c4

Nat.add._f only exists in stage2. Use a local myAdd definition so the test works in stage1 too. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 22, 2026

nomeata and others added 2 commits March 22, 2026 17:00

Merge remote-tracking branch 'origin/master' into joachim/namedF

9607567

# Conflicts: # tests/elab/1024.lean.out.expected # tests/elab/1237.lean.out.expected # tests/elab/3965_2.lean.out.expected # tests/elab/issue6281.lean.out.expected

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: name the functional argument to brecOn in structural recursion#12987

feat: name the functional argument to brecOn in structural recursion#12987
nomeata wants to merge 46 commits intomasterfrom
joachim/namedF

nomeata commented Mar 19, 2026 •

edited

Loading

Uh oh!

nomeata commented Mar 19, 2026

Uh oh!

leanprover-radar commented Mar 19, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Mar 19, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Mar 20, 2026 •

edited

Loading

Uh oh!

Uh oh!

nomeata commented Mar 22, 2026

Uh oh!

leanprover-radar commented Mar 22, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing bot commented Mar 22, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 22, 2026

Uh oh!

nomeata commented Mar 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

nomeata commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nomeata commented Mar 19, 2026

Uh oh!

leanprover-radar commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Mar 19, 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 Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

nomeata commented Mar 22, 2026

Uh oh!

leanprover-radar commented Mar 22, 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 Mar 22, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 22, 2026

Uh oh!

nomeata commented Mar 22, 2026

Analysis of stage2 test failures

Root cause

.regular hints (current)

.abbrev hints

The failing tests in detail

Options

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

nomeata commented Mar 19, 2026 •

edited

Loading

leanprover-radar commented Mar 19, 2026 •

edited

Loading

leanprover-bot commented Mar 19, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Mar 20, 2026 •

edited

Loading

leanprover-radar commented Mar 22, 2026 •

edited

Loading

`.regular` hints (current)

`.abbrev` hints