From 1b50183d6ec0a55d619415bd45e55c11486e4d6f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 3 Jun 2026 13:42:34 +0000 Subject: [PATCH 1/3] feat: bound kernel recursion by the `maxRecDepth` option 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 --- src/Lean/AddDecl.lean | 6 ++- src/Lean/Environment.lean | 16 +++---- src/Lean/Message.lean | 2 +- src/Lean/Replay.lean | 2 +- src/kernel/environment.cpp | 9 ++-- src/kernel/expr_eq_fn.cpp | 43 ++++++------------- src/kernel/type_checker.cpp | 3 ++ src/library/elab_environment.cpp | 7 +-- src/runtime/interrupt.cpp | 19 ++++++++ src/runtime/interrupt.h | 23 ++++++++++ .../didOpen.log | 4 +- .../identifier_completion.lean.dir/file.lean | 2 +- tests/elab/10577.lean | 2 +- tests/elab/bvarcrash.lean | 4 +- tests/elab/kernelInterrupt.lean | 2 +- tests/elab/lean_nat_bitwise.lean | 2 +- tests/elab_bench/bv_decide_rewriter.lean | 2 +- .../LeanCheckerTests/AddFalse.lean | 2 +- 18 files changed, 91 insertions(+), 59 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index 7e42c1e684bd..e302ee1d4e73 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -12,6 +12,7 @@ public import Lean.OriginalConstKind public import Lean.AutoDecl import Lean.Linter.Init import Lean.Compiler.MetaAttr +import Lean.Util.RecDepth import all Lean.OriginalConstKind -- for accessing `privateConstKindsExt` public section @@ -24,11 +25,12 @@ def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Decl if debug.skipKernelTC.get opts then addDeclWithoutChecking env decl else - addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk? + addDeclCore env (Core.getMaxHeartbeats opts).toUSize (maxRecDepth.get opts).toUSize decl cancelTk? private def Environment.addDeclAux (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment := - env.addDeclCore (Core.getMaxHeartbeats opts).toUSize decl cancelTk? (!debug.skipKernelTC.get opts) + env.addDeclCore (Core.getMaxHeartbeats opts).toUSize (maxRecDepth.get opts).toUSize decl cancelTk? + (!debug.skipKernelTC.get opts) open Linter in /-- diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 67a5dba7b9c6..51b3bc8c9f7d 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -294,8 +294,8 @@ private def isQuotInit (env : Environment) : Bool := /-- Type check given declaration and add it to the environment -/ @[extern "lean_add_decl"] -opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) - (cancelTk? : @& Option IO.CancelToken) : Except Exception Environment +opaque addDeclCore (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize) + (decl : @& Declaration) (cancelTk? : @& Option IO.CancelToken) : Except Exception Environment /-- Add declaration to kernel without type checking it. @@ -685,8 +685,8 @@ def unlockAsync (env : Environment) : Environment := { env with asyncCtx? := none } @[extern "lean_elab_add_decl"] -private opaque addDeclCheck (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) - (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment +private opaque addDeclCheck (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize) + (decl : @& Declaration) (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment @[extern "lean_elab_add_decl_without_checking"] private opaque addDeclWithoutChecking (env : Environment) (decl : @& Declaration) : @@ -698,15 +698,15 @@ Adds given declaration to the environment, type checking it unless `doCheck` is This is a plumbing function for the implementation of `Lean.addDecl`, most users should use it instead. -/ -def addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) - (cancelTk? : @& Option IO.CancelToken) (doCheck := true) : +def addDeclCore (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize) + (decl : @& Declaration) (cancelTk? : @& Option IO.CancelToken) (doCheck := true) : Except Kernel.Exception Environment := do if let some ctx := env.asyncCtx? then if let some n := decl.getTopLevelNames.find? (!ctx.mayContain ·) then throw <| .other s!"cannot add declaration {n} to environment as it is restricted to the \ prefix {ctx.declPrefix}" let mut env ← if doCheck then - addDeclCheck env maxHeartbeats decl cancelTk? + addDeclCheck env maxHeartbeats maxRecDepth decl cancelTk? else addDeclWithoutChecking env decl @@ -2612,7 +2612,7 @@ where return panic! s!"{c.constInfo.name} must be definition/theorem" -- realized kernel additions cannot be interrupted - which would be bad anyway as they can be -- reused between snapshots - kenv ← ofExcept <| kenv.addDeclCore 0 decl none + kenv ← ofExcept <| kenv.addDeclCore 0 0 decl none return kenv /-- Like `evalConst`, but first check that `constName` indeed is a declaration of type `typeName`. diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 983cafd96ef3..5e2281389fe2 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -889,7 +889,7 @@ def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData := | other msg => m!"(kernel) {msg}" | deterministicTimeout => "(kernel) deterministic timeout" | excessiveMemory => "(kernel) excessive memory consumption detected" - | deepRecursion => "(kernel) deep recursion detected" + | deepRecursion => "(kernel) deep recursion detected, use `set_option maxRecDepth ` to increase the limit" | interrupted => "(kernel) interrupted" end Kernel.Exception diff --git a/src/Lean/Replay.lean b/src/Lean/Replay.lean index 065a8ca2e80b..c2995c85888a 100644 --- a/src/Lean/Replay.lean +++ b/src/Lean/Replay.lean @@ -57,7 +57,7 @@ def throwKernelException (ex : Kernel.Exception) : M Unit := do /-- Add a declaration, possibly throwing a `Kernel.Exception`. -/ def addDecl (d : Declaration) : M Unit := do - match (← get).env.addDeclCore 0 d (cancelTk? := none) with + match (← get).env.addDeclCore 0 0 d (cancelTk? := none) with | .ok env => modify fun s => { s with env := env } | .error ex => throwKernelException ex diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 8c5d2b1a79b3..b86c1367d775 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -269,13 +269,14 @@ environment environment::add(declaration const & d, bool check) const { lean_unreachable(); } /* -addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declaration) +addDeclCore (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize) (decl : @& Declaration) (cancelTk? : @& Option IO.CancelToken) : Except Kernel.Exception Environment */ -extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat, object * decl, - object * opt_cancel_tk) { +extern "C" LEAN_EXPORT object * lean_add_decl(object * env, size_t max_heartbeat, size_t max_rec_depth, + object * decl, object * opt_cancel_tk) { scope_max_heartbeat s(max_heartbeat); - scope_cancel_tk s2(is_scalar(opt_cancel_tk) ? nullptr : cnstr_get(opt_cancel_tk, 0)); + scope_max_rec_depth s2(max_rec_depth); + scope_cancel_tk s3(is_scalar(opt_cancel_tk) ? nullptr : cnstr_get(opt_cancel_tk, 0)); return catch_kernel_exceptions([&]() { return environment(env).add(declaration(decl, true)); }); diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 74dd69ed4b74..fc157a34de8f 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -29,7 +29,6 @@ class expr_eq_fn { }; typedef lean::unordered_set, key_hasher> cache; cache * m_cache = nullptr; - size_t m_max_stack_depth = 0; size_t m_counter = 0; bool check_cache(expr const & a, expr const & b) { if (!is_shared(a) || !is_shared(b)) @@ -42,17 +41,7 @@ class expr_eq_fn { m_cache->insert(key); return false; } - void check_system(unsigned depth) { - /* - We used to use `lean::check_system` here. We claim it is ok to not check memory consumption here. - Note that `do_check_interrupted` was set to `false`. Thus, `check_interrupted` and `check_heartbeat` were not being used. - */ - if (depth > m_max_stack_depth) { - if (m_max_stack_depth > 0) - throw stack_space_exception("expression equality test"); - } - } - bool apply(expr const & a, expr const & b, unsigned depth, bool root = false) { + bool apply(expr const & a, expr const & b, bool root = false) { if (is_eqp(a, b)) return true; if (hash(a) != hash(b)) return false; if (a.kind() != b.kind()) return false; @@ -64,9 +53,7 @@ class expr_eq_fn { case expr_kind::Sort: return sort_level(a) == sort_level(b); default: break; } - if (root) { - m_max_stack_depth = get_available_stack_size() / 256; - } else if (check_cache(a, b)) { + if (!root && check_cache(a, b)) { return true; } /* @@ -75,7 +62,6 @@ class expr_eq_fn { We use the counter to invoke `add_heartbeats` later. Reason: heartbeat is a thread local storage, and morexpensive to update. */ m_counter++; - depth++; switch (a.kind()) { case expr_kind::BVar: case expr_kind::Lit: @@ -85,11 +71,11 @@ class expr_eq_fn { lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::MData: return - apply(mdata_expr(a), mdata_expr(b), depth) && + apply(mdata_expr(a), mdata_expr(b)) && mdata_data(a) == mdata_data(b); case expr_kind::Proj: return - apply(proj_expr(a), proj_expr(b), depth) && + apply(proj_expr(a), proj_expr(b)) && proj_sname(a) == proj_sname(b) && proj_idx(a) == proj_idx(b); case expr_kind::Const: @@ -97,32 +83,29 @@ class expr_eq_fn { const_name(a) == const_name(b) && compare(const_levels(a), const_levels(b), [](level const & l1, level const & l2) { return l1 == l2; }); case expr_kind::App: { - check_system(depth); - if (!apply(app_arg(a), app_arg(b), depth)) return false; + if (!apply(app_arg(a), app_arg(b))) return false; expr const * curr_a = &app_fn(a); expr const * curr_b = &app_fn(b); while (true) { if (!is_app(*curr_a)) break; if (!is_app(*curr_b)) return false; - if (!apply(app_arg(*curr_a), app_arg(*curr_b), depth)) return false; + if (!apply(app_arg(*curr_a), app_arg(*curr_b))) return false; curr_a = &app_fn(*curr_a); curr_b = &app_fn(*curr_b); } - return apply(*curr_a, *curr_b, depth); + return apply(*curr_a, *curr_b); } case expr_kind::Lambda: case expr_kind::Pi: - check_system(depth); return - apply(binding_domain(a), binding_domain(b), depth) && - apply(binding_body(a), binding_body(b), depth) && + apply(binding_domain(a), binding_domain(b)) && + apply(binding_body(a), binding_body(b)) && (!CompareBinderInfo || binding_name(a) == binding_name(b)) && (!CompareBinderInfo || binding_info(a) == binding_info(b)); case expr_kind::Let: - check_system(depth); return - apply(let_type(a), let_type(b), depth) && - apply(let_value(a), let_value(b), depth) && - apply(let_body(a), let_body(b), depth) && + apply(let_type(a), let_type(b)) && + apply(let_value(a), let_value(b)) && + apply(let_body(a), let_body(b)) && let_nondep(a) == let_nondep(b) && (!CompareBinderInfo || let_name(a) == let_name(b)); } @@ -134,7 +117,7 @@ class expr_eq_fn { if (m_cache) delete m_cache; if (m_counter > 0) add_heartbeats(m_counter); } - bool operator()(expr const & a, expr const & b) { return apply(a, b, 0, true); } + bool operator()(expr const & a, expr const & b) { return apply(a, b, true); } }; bool is_equal(expr const & a, expr const & b) { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index e8b1ff56105c..76e4372a75fa 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -271,6 +271,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { if (has_loose_bvars(e)) throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it"); + scope_rec_depth guard; check_system("type checker", /* do_check_interrupted */ true); auto it = m_st->m_infer_type[infer_only].find(e); @@ -399,6 +400,7 @@ static bool is_let_fvar(local_ctx const & lctx, expr const & e) { If `cheap == true`, then we don't perform delta-reduction when reducing major premise of recursors and projections. We also do not cache results. */ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) { + scope_rec_depth guard; check_system("type checker: whnf", /* do_check_interrupted */ true); // handle easy cases @@ -1054,6 +1056,7 @@ bool type_checker::is_def_eq_unit_like(expr const & t, expr const & s) { } bool type_checker::is_def_eq_core(expr const & t, expr const & s) { + scope_rec_depth guard; check_system("is_definitionally_equal", /* do_check_interrupted */ true); bool use_hash = true; lbool r = quick_is_def_eq(t, s, use_hash); diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp index 95d368025459..7d2814eed315 100644 --- a/src/library/elab_environment.cpp +++ b/src/library/elab_environment.cpp @@ -24,10 +24,11 @@ elab_environment elab_environment::add(declaration const & d, bool check) const return elab_environment(lean_elab_environment_update_base_after_kernel_add(this->to_obj_arg(), kenv.to_obj_arg(), d.to_obj_arg())); } -extern "C" LEAN_EXPORT object * lean_elab_add_decl(object * env, size_t max_heartbeat, object * decl, - object * opt_cancel_tk) { +extern "C" LEAN_EXPORT object * lean_elab_add_decl(object * env, size_t max_heartbeat, size_t max_rec_depth, + object * decl, object * opt_cancel_tk) { scope_max_heartbeat s(max_heartbeat); - scope_cancel_tk s2(is_scalar(opt_cancel_tk) ? nullptr : cnstr_get(opt_cancel_tk, 0)); + scope_max_rec_depth s2(max_rec_depth); + scope_cancel_tk s3(is_scalar(opt_cancel_tk) ? nullptr : cnstr_get(opt_cancel_tk, 0)); return catch_kernel_exceptions([&]() { return elab_environment(env).add(declaration(decl, true)); }); diff --git a/src/runtime/interrupt.cpp b/src/runtime/interrupt.cpp index 3e34dd588636..8de2d85e9f54 100644 --- a/src/runtime/interrupt.cpp +++ b/src/runtime/interrupt.cpp @@ -54,6 +54,25 @@ void check_heartbeat() { throw_heartbeat_exception(); } +LEAN_THREAD_VALUE(size_t, g_max_rec_depth, 0); +LEAN_THREAD_VALUE(size_t, g_rec_depth, 0); + +void set_max_rec_depth(size_t max) { g_max_rec_depth = max; } +size_t get_max_rec_depth() { return g_max_rec_depth; } + +LEAN_EXPORT scope_max_rec_depth::scope_max_rec_depth(size_t max) : + m_max(g_max_rec_depth, max), m_curr(g_rec_depth, 0) {} + +LEAN_EXPORT scope_rec_depth::scope_rec_depth() { + g_rec_depth++; + if (g_max_rec_depth > 0 && g_rec_depth > g_max_rec_depth) { + g_rec_depth--; + throw stack_space_exception("type checker"); + } +} + +LEAN_EXPORT scope_rec_depth::~scope_rec_depth() { g_rec_depth--; } + LEAN_THREAD_VALUE(lean_object *, g_cancel_tk, nullptr); LEAN_EXPORT scope_cancel_tk::scope_cancel_tk(lean_object * o):flet(g_cancel_tk, o) {} diff --git a/src/runtime/interrupt.h b/src/runtime/interrupt.h index 14cf99385beb..3f8b4859042f 100644 --- a/src/runtime/interrupt.h +++ b/src/runtime/interrupt.h @@ -42,6 +42,29 @@ class LEAN_EXPORT scope_max_heartbeat : flet { LEAN_EXPORT void check_heartbeat(); +/** \brief Threshold on the kernel type checker's recursion depth. `scope_rec_depth` throws a + `stack_space_exception` when a thread exceeds the limit. `0` means unlimited (the default). + + This is a thread local value, set from the `maxRecDepth` option at the kernel entry points. */ +LEAN_EXPORT void set_max_rec_depth(size_t max); +LEAN_EXPORT size_t get_max_rec_depth(); + +/* Set the thread local max recursion depth and reset the current depth to 0. */ +class LEAN_EXPORT scope_max_rec_depth { + flet m_max; + flet m_curr; +public: + LEAN_EXPORT scope_max_rec_depth(size_t max); +}; + +/* RAII guard that increments the thread local recursion depth for the duration of its scope, + throwing a `stack_space_exception` if the configured maximum is exceeded. */ +class LEAN_EXPORT scope_rec_depth { +public: + LEAN_EXPORT scope_rec_depth(); + LEAN_EXPORT ~scope_rec_depth(); +}; + /* Update the thread local `IO.CancelToken` (`nullptr` if unset) */ class LEAN_EXPORT scope_cancel_tk : flet { public: diff --git a/tests/compile_bench/identifier_completion.lean.dir/didOpen.log b/tests/compile_bench/identifier_completion.lean.dir/didOpen.log index d10da13660f9..d99f3e7a4a03 100644 --- a/tests/compile_bench/identifier_completion.lean.dir/didOpen.log +++ b/tests/compile_bench/identifier_completion.lean.dir/didOpen.log @@ -1,3 +1,3 @@ -Content-Length: 1041 +Content-Length: 1043 -{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n setEnv env'\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} \ No newline at end of file +{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 0 <| .opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n setEnv env'\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} diff --git a/tests/compile_bench/identifier_completion.lean.dir/file.lean b/tests/compile_bench/identifier_completion.lean.dir/file.lean index 722a2087fff7..ea759ee64bda 100644 --- a/tests/compile_bench/identifier_completion.lean.dir/file.lean +++ b/tests/compile_bench/identifier_completion.lean.dir/file.lean @@ -6,7 +6,7 @@ open Lean def buildSyntheticEnv : Lean.CoreM Unit := do for i in [0:100000] do let name := s!"Long.And.Hopefully.Unique.Name.foo{i}".toName - let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 <| .opaqueDecl { + let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 0 <| .opaqueDecl { name := name levelParams := [] type := .const `Nat [] diff --git a/tests/elab/10577.lean b/tests/elab/10577.lean index b5420ea4fd3f..c9cccc13672e 100644 --- a/tests/elab/10577.lean +++ b/tests/elab/10577.lean @@ -45,4 +45,4 @@ open Lean /-- error: (kernel) let-declaration type mismatch 'a' -/ #guard_msgs in run_meta - setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_0 none) + setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 0 decl_0 none) diff --git a/tests/elab/bvarcrash.lean b/tests/elab/bvarcrash.lean index 7abb31c58dc2..da8b6a9fd609 100644 --- a/tests/elab/bvarcrash.lean +++ b/tests/elab/bvarcrash.lean @@ -635,9 +635,9 @@ open Lean -- We avoid `Lean.addDecl` as it may be doing additional checks that hide the expected error. run_meta do for decl in [decl_0, decl_1, decl_2, decl_3, decl_4, decl_5, decl_6, decl_7, decl_8] do - setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl none) + setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 0 decl none) /-- error: (kernel) constant has already been declared '«term_+_»' -/ #guard_msgs in run_meta - setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_9 none) + setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 0 decl_9 none) diff --git a/tests/elab/kernelInterrupt.lean b/tests/elab/kernelInterrupt.lean index 59d961a689e1..1b752f21a091 100644 --- a/tests/elab/kernelInterrupt.lean +++ b/tests/elab/kernelInterrupt.lean @@ -20,7 +20,7 @@ open Lean type := mkConst `Nat isUnsafe := false } - env.addDeclCore 1000 decl tk + env.addDeclCore 1000 0 decl tk tk.set envPromise.resolve env assert! t.get matches .error .interrupted diff --git a/tests/elab/lean_nat_bitwise.lean b/tests/elab/lean_nat_bitwise.lean index 7b76a768bf65..63975ba76ebf 100644 --- a/tests/elab/lean_nat_bitwise.lean +++ b/tests/elab/lean_nat_bitwise.lean @@ -2,7 +2,7 @@ -- and performs a few basic tests. -- Without kernel support the tests containing the 2^20 constant will --- fail with "error: (kernel) deep recursion detected" +-- fail with "error: (kernel) deep recursion detected, use `set_option maxRecDepth ` to increase the limit" example : 0 &&& 0 = 0 := rfl example : 0 &&& 0b1111 = 0 := rfl diff --git a/tests/elab_bench/bv_decide_rewriter.lean b/tests/elab_bench/bv_decide_rewriter.lean index c921dc5bc3af..ef8257f24390 100644 --- a/tests/elab_bench/bv_decide_rewriter.lean +++ b/tests/elab_bench/bv_decide_rewriter.lean @@ -7,7 +7,7 @@ second to solve at the time of adding this. Bitwuzla is capable of solving it in the same machine that these numbers were measured on. -/ -set_option maxRecDepth 2048 in +set_option maxRecDepth 4096 in example: ∀ (T1_114127 T1_114128 T1_114129 : BitVec 8), (!have v_3 := BitVec.setWidth 32 1#8; diff --git a/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean index 6092c4eb441d..158722259a00 100644 --- a/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean +++ b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean @@ -4,7 +4,7 @@ open Lean in run_elab modifyEnv fun env => Id.run do let decl := .thmDecl { name := `false, levelParams := [], type := .const ``False [], value := .const ``False [] } - let .ok env := env.addDeclCore (doCheck := false) 0 decl none | + let .ok env := env.addDeclCore (doCheck := false) 0 0 decl none | let _ : Inhabited Environment := ⟨env⟩ unreachable! env From 9d0e6e770c66d61ed45c3b32b26d7fa1be18cd0f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 4 Jun 2026 10:04:51 +0000 Subject: [PATCH 2/3] fix: `decide +kernel` error when elab fails as well --- src/Lean/Elab/Tactic/Decide.lean | 18 +++++++++++------- tests/elab/kernelMaxRecDepth.lean | 28 ++++++++++++++++++++++++++++ 2 files changed, 39 insertions(+), 7 deletions(-) create mode 100644 tests/elab/kernelMaxRecDepth.lean diff --git a/src/Lean/Elab/Tactic/Decide.lean b/src/Lean/Elab/Tactic/Decide.lean index aa99499ca91f..929dd0a01dc1 100644 --- a/src/Lean/Elab/Tactic/Decide.lean +++ b/src/Lean/Elab/Tactic/Decide.lean @@ -119,13 +119,17 @@ where catch ex => -- Diagnose the failure, lazily so that there is no performance impact if `decide` isn't being used interactively. throwError MessageData.ofLazyM (es := #[expectedType]) do - let r ← withAtLeastTransparency .default <| whnf s - if r.isAppOf ``isTrue then - return m!"\ - Tactic `{tacticName}` failed. The elaborator is able to reduce the \ - `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\ - {indentD ex.toMessageData}" - diagnose expectedType s r + -- Report original kernel exception if elab fails as well + tryCatchRuntimeEx + (do + let r ← withAtLeastTransparency .default <| whnf s + if r.isAppOf ``isTrue then + return m!"\ + Tactic `{tacticName}` failed. The elaborator is able to reduce the \ + `{.ofConstName ``Decidable}` instance, but the kernel fails with:\n\ + {indentD ex.toMessageData}" + diagnose expectedType s r) + (fun _ => return ex.toMessageData) diagnose (expectedType s : Expr) (r : Expr) : MetaM MessageData := do if r.isAppOf ``isFalse then diff --git a/tests/elab/kernelMaxRecDepth.lean b/tests/elab/kernelMaxRecDepth.lean new file mode 100644 index 000000000000..00602b9ef825 --- /dev/null +++ b/tests/elab/kernelMaxRecDepth.lean @@ -0,0 +1,28 @@ +import Lean + +/-! +The kernel bounds its recursion depth by the `maxRecDepth` option. Checking a sufficiently +deeply nested declaration fails deterministically with `(kernel) deep recursion detected` when +`maxRecDepth` is small, and succeeds once the limit is raised. +-/ + +open Lean + +/-- `Nat.succ (Nat.succ ... Nat.zero)` nested `n` deep. -/ +private partial def mkDeepNat : Nat → Expr + | 0 => .const ``Nat.zero [] + | n + 1 => .app (.const ``Nat.succ []) (mkDeepNat n) + +private def addDeepDef (name : Name) : MetaM Unit := + Lean.addDecl <| .defnDecl { + name, levelParams := [], type := .const ``Nat [], + value := mkDeepNat 3000, hints := .opaque, safety := .safe + } + +/-- error: (kernel) deep recursion detected, use `set_option maxRecDepth ` to increase the limit -/ +#guard_msgs in +set_option maxRecDepth 256 in +run_meta addDeepDef `tooDeep + +set_option maxRecDepth 100000 in +run_meta addDeepDef `deepEnough From 6baff0579943c1f349b2c6f806ae326c8abf4996 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 4 Jun 2026 12:08:28 +0000 Subject: [PATCH 3/3] fix: give the kernel recursion limit headroom over `maxRecDepth` 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 --- src/runtime/interrupt.cpp | 10 +++++++++- .../identifier_completion.lean.dir/didOpen.log | 2 +- tests/elab/kernelMaxRecDepth.lean | 4 +++- tests/elab_bench/bv_decide_rewriter.lean | 2 +- tests/elab_bench/string_simp_ne.lean | 3 +++ 5 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/runtime/interrupt.cpp b/src/runtime/interrupt.cpp index 8de2d85e9f54..4cc6fac15430 100644 --- a/src/runtime/interrupt.cpp +++ b/src/runtime/interrupt.cpp @@ -57,6 +57,14 @@ void check_heartbeat() { LEAN_THREAD_VALUE(size_t, g_max_rec_depth, 0); LEAN_THREAD_VALUE(size_t, g_rec_depth, 0); +/* The kernel re-checks a fully elaborated term from scratch, without the caching, metavariable + assignments, and reducibility shortcuts the elaborator uses while building it incrementally. As a + result the kernel recurses substantially deeper than the elaborator did for the same term (stdlib + `grind`/`simp` proofs check several thousand levels deep). We therefore let the kernel reach a + generous multiple of the configured `maxRecDepth` before bailing out, so that code which fits + within `maxRecDepth` during elaboration is not rejected by the kernel. */ +static constexpr size_t g_kernel_rec_depth_factor = 16; + void set_max_rec_depth(size_t max) { g_max_rec_depth = max; } size_t get_max_rec_depth() { return g_max_rec_depth; } @@ -65,7 +73,7 @@ LEAN_EXPORT scope_max_rec_depth::scope_max_rec_depth(size_t max) : LEAN_EXPORT scope_rec_depth::scope_rec_depth() { g_rec_depth++; - if (g_max_rec_depth > 0 && g_rec_depth > g_max_rec_depth) { + if (g_max_rec_depth > 0 && g_rec_depth > g_max_rec_depth * g_kernel_rec_depth_factor) { g_rec_depth--; throw stack_space_exception("type checker"); } diff --git a/tests/compile_bench/identifier_completion.lean.dir/didOpen.log b/tests/compile_bench/identifier_completion.lean.dir/didOpen.log index d99f3e7a4a03..d5198d157c45 100644 --- a/tests/compile_bench/identifier_completion.lean.dir/didOpen.log +++ b/tests/compile_bench/identifier_completion.lean.dir/didOpen.log @@ -1,3 +1,3 @@ Content-Length: 1043 -{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 0 <| .opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n setEnv env'\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} +{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/sebastian/lean4/tests/bench/identifier_completion.lean","languageId":"lean4","version":129,"text":"prelude\nimport Lean.AddDecl\n\nopen Lean\n\ndef buildSyntheticEnv : Lean.CoreM Unit := do\n for i in [0:100000] do\n let name := s!\"Long.And.Hopefully.Unique.Name.foo{i}\".toName\n let env' ← ofExceptKernelException <| (← getEnv).addDeclCore (cancelTk? := none) 0 0 <| .opaqueDecl {\n name := name\n levelParams := []\n type := .const `Nat []\n value := .const `Nat.zero []\n isUnsafe := false\n all := [name]\n }\n setEnv env'\n addDocStringCore name \"A synthetic doc-string\"\n\n#eval buildSyntheticEnv\n\n-- This will be quite a bit slower than the equivalent in a file that imports all of these decls,\n-- since we can pre-compute information about those imports.\n-- It still serves as a useful benchmark, though.\n#eval Long.And.Hopefully.Unique.Name.foo\n"},"dependencyBuildMode":"never"}} \ No newline at end of file diff --git a/tests/elab/kernelMaxRecDepth.lean b/tests/elab/kernelMaxRecDepth.lean index 00602b9ef825..e6573ce9f691 100644 --- a/tests/elab/kernelMaxRecDepth.lean +++ b/tests/elab/kernelMaxRecDepth.lean @@ -13,10 +13,12 @@ private partial def mkDeepNat : Nat → Expr | 0 => .const ``Nat.zero [] | n + 1 => .app (.const ``Nat.succ []) (mkDeepNat n) +-- The kernel allows a multiple of `maxRecDepth` before bailing out, so the term has to be nested +-- deeper than that multiple times the `maxRecDepth` of 256 used below. private def addDeepDef (name : Name) : MetaM Unit := Lean.addDecl <| .defnDecl { name, levelParams := [], type := .const ``Nat [], - value := mkDeepNat 3000, hints := .opaque, safety := .safe + value := mkDeepNat 8000, hints := .opaque, safety := .safe } /-- error: (kernel) deep recursion detected, use `set_option maxRecDepth ` to increase the limit -/ diff --git a/tests/elab_bench/bv_decide_rewriter.lean b/tests/elab_bench/bv_decide_rewriter.lean index ef8257f24390..c921dc5bc3af 100644 --- a/tests/elab_bench/bv_decide_rewriter.lean +++ b/tests/elab_bench/bv_decide_rewriter.lean @@ -7,7 +7,7 @@ second to solve at the time of adding this. Bitwuzla is capable of solving it in the same machine that these numbers were measured on. -/ -set_option maxRecDepth 4096 in +set_option maxRecDepth 2048 in example: ∀ (T1_114127 T1_114128 T1_114129 : BitVec 8), (!have v_3 := BitVec.setWidth 32 1#8; diff --git a/tests/elab_bench/string_simp_ne.lean b/tests/elab_bench/string_simp_ne.lean index e4926a666dae..2913e43029e6 100644 --- a/tests/elab_bench/string_simp_ne.lean +++ b/tests/elab_bench/string_simp_ne.lean @@ -14,6 +14,9 @@ Key variables: set_option Elab.async false set_option maxHeartbeats 8000000 +-- The kernel verifies `String.ofList` by recursion that is O(string length), running far deeper +-- than elaboration, so checking the longest strings below needs a `maxRecDepth` above the default. +set_option maxRecDepth 8000 open Lean Elab Command in /-- Generate `example : s₁ ≠ s₂ := by simp` where s₁ = n×'a'++"x" and s₂ = n×'a'++"y". -/