feat: bound kernel recursion by maxRecDepth

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
 /--

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

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`.

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 <num>` to increase the limit"
   | interrupted                         => "(kernel) interrupted"
 
 end Kernel.Exception

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
 

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<environment>([&]() {
             return environment(env).add(declaration(decl, true));
         });

src/kernel/expr_eq_fn.cpp

@@ -29,7 +29,6 @@ class expr_eq_fn {
     };
     typedef lean::unordered_set<std::pair<lean_object *, lean_object *>, 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,44 +71,41 @@ 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:
             return
                 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) {

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);

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<elab_environment>([&]() {
             return elab_environment(env).add(declaration(decl, true));
         });

src/runtime/interrupt.cpp

@@ -54,6 +54,33 @@ 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);
+
+/* 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; }
+
+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_kernel_rec_depth_factor) {
+        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<lean_object *>(g_cancel_tk, o) {}

src/runtime/interrupt.h

@@ -42,6 +42,29 @@ class LEAN_EXPORT scope_max_heartbeat : flet<size_t> {
 
 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<size_t> m_max;
+    flet<size_t> 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<lean_object *> {
 public:

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"}}
+{"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"}}

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

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)