feat: bound kernel recursion by maxRecDepth#13956
Open
Kha wants to merge 3 commits into
Open
Conversation
This PR makes the kernel type checker bound its recursion depth using the existing `maxRecDepth` option instead of measuring physical stack space. Previously the kernel relied on a non-deterministic stack-space check that varied by platform, build, and optimization, making `(kernel) deep recursion detected` errors irreproducible. The limit is now deterministic and adjustable with `set_option maxRecDepth`. The `maxRecDepth` value is threaded to the kernel entry points (`lean_add_decl`, `lean_elab_add_decl`) alongside `maxHeartbeats` and tracked via a thread-local recursion-depth counter (`scope_max_rec_depth` / `scope_rec_depth`) checked at the type checker's recursive entry points. The stack-based limit in `expr_eq_fn` is removed, and the `.deepRecursion` message now points at `maxRecDepth`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 183982a against c47a0c7 are in. There are significant results. @Kha
No significant changes detected. |
github-actions
Bot
added
the
toolchain-available
Collaborator
|
Reference manual CI status:
|
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
This PR lets the kernel recurse up to 16 times the configured `maxRecDepth` before reporting deep recursion. The kernel re-checks a fully elaborated term from scratch, without the caching, metavariable assignments, and reducibility shortcuts the elaborator relies on while building it, so it bottoms out substantially deeper than elaboration did for the same term; without this headroom, code that fits within `maxRecDepth` during elaboration -- including stdlib `grind`/`simp` proofs -- could be rejected by the kernel. Adjust the kernel-heavy benchmarks accordingly: `string_simp_ne` needs a higher `maxRecDepth` for its O(n) `String.ofList` verification, while `bv_decide_rewriter` no longer needs its earlier bump. Also fix a stray trailing CRLF in the `identifier_completion` LSP fixture that desynced the message stream. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 62082bb against c47a0c7 are in. There are significant results. @Kha
Large changes (2✅)
Small changes (20✅, 1🟥) Too many entries to display here. View the full report on radar instead. |
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jun 5, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jun 5, 2026
|
Benchmark results for 62082bb against c47a0c7 are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Kha
Large changes (2✅)
Small changes (20✅, 1🟥) Too many entries to display here. View the full report on radar instead. |
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@49f5b1e against leanprover-community/mathlib4-nightly-testing@8a9ccb2 are in. No significant results found. @Kha
Small changes (2🟥)
|
mathlib-lean-pr-testing
Bot
added
builds-mathlib
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR makes the kernel's
(kernel) deep recursion detectederror deterministic by bounding kernel type checking with the existingmaxRecDepthoption instead of the physical stack size. The limit previously depended on the native stack, so it varied across platforms, builds, and optimization levels and could not be reproduced reliably; it is now a function ofmaxRecDepthalone and is raised the usual way withset_option maxRecDepth <num>.To avoid rejecting existing code that already fits within
maxRecDepthduring elaboration, the kernel is allowed to recurse up to a fixed multiple (currently 16×) of the configured value before reporting deep recursion; this is sufficient for lean4/Mathlib to build. Since the absolute value ofmaxRecDepthhas no inherent meaning, this multiplier should not lead to surprising behavior.The value is threaded to the kernel entry points (
lean_add_decl,lean_elab_add_decl) alongsidemaxHeartbeatsand tracked with a thread-local recursion-depth counter checked at the type checker's recursive entry points (infer,whnf,isDefEq). The former physical-stack-based budget in the structuralExprcomparison is removed. The standalone debugging entry pointsKernel.check/Kernel.whnf/Kernel.isDefEqremain unbounded.This PR also improves the
decide +kernelfailure report: when the kernel rejects the proof and the tactic's lazy diagnostic itself exceedsmaxRecDepthwhile re-reducing the instance, the tactic now surfaces the kernel's actual error (usingtryCatchRuntimeEx, sincemaxRecDepthis a runtime exception that ordinarytry/catchre-raises) instead of an opaque[Error pretty printing: …].Finally, a couple of kernel-heavy benchmarks that legitimately recurse deeply gain an explicit
maxRecDepth(string_simp_ne's O(n)String.ofListverification), and a new test pins the deterministic, option-controlled behavior.