perf: amortize check_system via check_heartbeat

Add an amortized check_system call every 256 heartbeats inside
check_heartbeat. This ensures periodic stack, memory, and monitoring
interval checks for any code path that uses heartbeats, including
the kernel type checker.

Also fix backtrace cascade in check_system_interval monitoring by
resetting the timer after printing the warning, and remove the
redundant per-call checkSystem in LCNF simp (keeping only the
amortized one).

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

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -217,6 +217,8 @@ Simplify `code`
 -/
 partial def simp (code : Code .pure) : SimpM (Code .pure) := withIncRecDepth do
   incVisited
+  if (← get).visited % 512 == 0 then
+    checkSystem "LCNF simp"
   match code with
   | .let decl k =>
     let baseDecl := decl

src/Lean/Compiler/LCNF/ToMono.lean

@@ -279,13 +279,13 @@ partial def casesFloatArrayToMono (c : Cases .pure) (_ : c.typeName == ``FloatAr
   let k ← k.toMono
   return .let decl k
 
-/-- Eliminate `cases` for `String`. -/
+/-- Eliminate `cases` for `String. -/
 partial def casesStringToMono (c : Cases .pure) (_ : c.typeName == ``String) : ToMonoM (Code .pure) := do
   assert! c.alts.size == 1
   let .alt _ ps k := c.alts[0]! | unreachable!
   eraseParams ps
   let p := ps[0]!
-  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toByteArray [] #[.fvar c.discr] }
+  let decl := { fvarId := p.fvarId, binderName := p.binderName, type := anyExpr, value := .const ``String.toList [] #[.fvar c.discr] }
   modifyLCtx fun lctx => lctx.addLetDecl decl
   let k ← k.toMono
   return .let decl k

src/Lean/CoreM.lean

@@ -448,6 +448,14 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
+/--
+Record a check-in for the `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring.
+When that env var is set, warns on stderr if too much CPU time has elapsed since
+the last check-in from either the C++ `check_system` or this function.
+-/
+@[extern "lean_check_system_interval"]
+opaque checkSystemInterval (componentName : @& String) : BaseIO Unit
+
 /--
 Throws an internal interrupt exception if cancellation has been requested. The exception is not
 caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
@@ -458,6 +466,7 @@ Like `checkSystem` but without the global heartbeat check, for callers that have
 heartbeat tracking (e.g. `SynthInstance`).
  -/
 @[inline] def checkInterrupted : CoreM Unit := do
+  checkSystemInterval "Lean elaborator"
   if let some tk := (← read).cancelTk? then
     if (← tk.isSet) then
       throwInterruptException

src/Lean/Elab/BuiltinDo/Let.lean

@@ -168,25 +168,12 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         elabDoElem (← `(doElem| $pattern:term := $x)) dec
   | _ => throwUnsupportedSyntax
 
-/-- Backward-compatible index for `doLet`/`doLetArrow`/`doLetElse`: if `letConfig` is present at
-index 2, the decl is at index 3; otherwise (old-shape syntax from stage0 macros), it's at index 2. -/
-private def doLetDeclIdx (stx : Syntax) : Nat :=
-  if stx[2].isOfKind ``Parser.Term.letConfig then 3 else 2
-
-/-- Backward-compatible index for `doHave`: if `letConfig` is present at
-index 1, the decl is at index 2; otherwise (old-shape syntax), it's at index 1. -/
-private def doHaveDeclIdx (stx : Syntax) : Nat :=
-  if stx[1].isOfKind ``Parser.Term.letConfig then 2 else 1
-
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
-  -- "let " >> optional "mut " >> letConfig >> letDecl
-  let mutTk? := stx.raw[1].getOptional?
-  let decl : TSyntax ``letDecl := ⟨stx.raw[doLetDeclIdx stx.raw]⟩
+  let `(doLet| let $[mut%$mutTk?]? $decl:letDecl) := stx | throwUnsupportedSyntax
   elabDoLetOrReassign (.let mutTk?) decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
-  -- "have" >> letConfig >> letDecl
-  let decl : TSyntax ``letDecl := ⟨stx.raw[doHaveDeclIdx stx.raw]⟩
+  let `(doHave| have $decl:letDecl) := stx | throwUnsupportedSyntax
   elabDoLetOrReassign .have decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetRec] def elabDoLetRec : DoElab := fun stx dec => do
@@ -212,14 +199,7 @@ private def doHaveDeclIdx (stx : Syntax) : Nat :=
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
-  -- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >>
-  --   (checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent)
-  let mutTk? := stx.raw[1].getOptional?
-  let offset := doLetDeclIdx stx.raw -- 3 if letConfig present, 2 otherwise
-  let pattern : Term := ⟨stx.raw[offset]⟩
-  let rhs : Term := ⟨stx.raw[offset + 2]⟩
-  let otherwise : TSyntax ``doSeqIndent := ⟨stx.raw[offset + 4]⟩
-  let body? := stx.raw[offset + 5].getOptional?.map fun s => (⟨s⟩ : TSyntax ``doSeqIndent)
+  let `(doLetElse| let $[mut%$mutTk?]? $pattern := $rhs | $otherwise $(body?)?) := stx | throwUnsupportedSyntax
   let letOrReassign := LetOrReassign.let mutTk?
   let vars ← getPatternVarsEx pattern
   letOrReassign.checkMutVars vars
@@ -231,9 +211,7 @@ private def doHaveDeclIdx (stx : Syntax) : Nat :=
   elabDoElem (← `(doElem| match $rhs:term with | $pattern => $body:doSeqIndent | _ => $otherwise:doSeqIndent)) dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetArrow] def elabDoLetArrow : DoElab := fun stx dec => do
-  -- "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
-  let mutTk? := stx.raw[1].getOptional?
-  let decl : TSyntax [``doIdDecl, ``doPatDecl] := ⟨stx.raw[doLetDeclIdx stx.raw]⟩
+  let `(doLetArrow| let $[mut%$mutTk?]? $decl) := stx | throwUnsupportedSyntax
   elabDoArrow (.let mutTk?) decl dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do

src/Lean/Elab/Do/InferControlInfo.lean

@@ -169,29 +169,15 @@ partial def ofElem (stx : TSyntax `doElem) : TermElabM ControlInfo := do
     let bodyInfo ← match body? with | none => pure {} | some body => ofSeq ⟨body⟩
     return otherwiseInfo.alternative bodyInfo
   | _ =>
-    -- Backward compat: quotation patterns above may fail for doLet/doHave/doLetElse/doLetArrow
-    -- when the parser shape includes letConfig (not present in stage0 quotations).
-    let kind := stx.raw.getKind
-    if kind == ``Parser.Term.doLet || kind == ``Parser.Term.doHave || kind == ``Parser.Term.doLetRec then
-      return .pure
-    if kind == ``Parser.Term.doLetElse then
-      let offset := if stx.raw[2].isOfKind ``Parser.Term.letConfig then 3 else 2
-      let otherwise? := stx.raw[offset + 4].getOptional?.map (⟨·⟩ : _ → TSyntax ``doSeqIndent)
-      let body? := stx.raw[offset + 5].getOptional?.map (⟨·⟩ : _ → TSyntax ``doSeqIndent)
-      return ← ofLetOrReassign #[] none otherwise? body?
-    if kind == ``Parser.Term.doLetArrow then
-      let declIdx := if stx.raw[2].isOfKind ``Parser.Term.letConfig then 3 else 2
-      let decl : TSyntax [``doIdDecl, ``doPatDecl] := ⟨stx.raw[declIdx]⟩
-      return ← ofLetOrReassignArrow false decl
-    let handlers := controlInfoElemAttribute.getEntries (← getEnv) kind
+    let handlers := controlInfoElemAttribute.getEntries (← getEnv) stx.raw.getKind
     for handler in handlers do
       let res ← catchInternalId unsupportedSyntaxExceptionId
         (some <$> handler.value stx)
         (fun _ => pure none)
       if let some info := res then return info
     throwError
-      "No `ControlInfo` inference handler found for `{kind}` in syntax {indentD stx}\n\
-       Register a handler with `@[doElem_control_info {kind}]`."
+      "No `ControlInfo` inference handler found for `{stx.raw.getKind}` in syntax {indentD stx}\n\
+       Register a handler with `@[doElem_control_info {stx.raw.getKind}]`."
 
 partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDecl, ``doPatDecl]) : TermElabM ControlInfo := do
   match decl with

src/Lean/Elab/Do/Legacy.lean

@@ -36,18 +36,6 @@ private def getDoSeq (doStx : Syntax) : Syntax :=
 def elabLiftMethod : TermElab := fun stx _ =>
   throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
 
-/-- Backward-compatible index for `doLet`/`doLetArrow`/`doLetElse`: if `letConfig` is present at
-index 2, the decl is at index 3; otherwise (old-shape syntax from stage0 quotations), it's at
-index 2. -/
-private def doLetDeclIdx (stx : Syntax) : Nat :=
-  if stx[2].isOfKind ``Parser.Term.letConfig then 3 else 2
-
-/-- Backward-compatible index for `doHave`: if `letConfig` is present at
-index 1, the decl is at index 2; otherwise (old-shape syntax from stage0 quotations), it's at
-index 1. -/
-private def doHaveDeclIdx (stx : Syntax) : Nat :=
-  if stx[1].isOfKind ``Parser.Term.letConfig then 2 else 1
-
 /-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind. -/
 private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
   k == ``Parser.Term.do ||
@@ -88,9 +76,9 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   else if k == ``Parser.Term.let then
     letDeclHasBinders stx[1]
   else if k == ``Parser.Term.doLet then
-    letDeclHasBinders stx[doLetDeclIdx stx]
+    letDeclHasBinders stx[2]
   else if k == ``Parser.Term.doLetArrow then
-    letDeclArgHasBinders stx[doLetDeclIdx stx]
+    letDeclArgHasBinders stx[2]
   else
     false
 
@@ -713,12 +701,12 @@ def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
     throwError "unexpected kind of let declaration"
 
 def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
-  -- leading_parser "let " >> optional "mut " >> letConfig >> letDecl
-  getLetDeclVars doLet[doLetDeclIdx doLet]
+  -- leading_parser "let " >> optional "mut " >> letDecl
+  getLetDeclVars doLet[2]
 
 def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) :=
-  -- leading_parser "have" >> letConfig >> letDecl
-  getLetDeclVars doHave[doHaveDeclIdx doHave]
+  -- leading_parser "have" >> letDecl
+  getLetDeclVars doHave[1]
 
 def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
   -- letRecDecls is an array of `(group (optional attributes >> letDecl))`
@@ -739,9 +727,9 @@ def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := doPatDecl[0]
   getPatternVarsEx pattern
 
--- leading_parser "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
+-- leading_parser "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
 def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
-  let decl := doLetArrow[doLetDeclIdx doLetArrow]
+  let decl := doLetArrow[2]
   if decl.getKind == ``Parser.Term.doIdDecl then
     return #[getDoIdDeclVar decl]
   else if decl.getKind == ``Parser.Term.doPatDecl then
@@ -1072,14 +1060,14 @@ def seqToTerm (action : Syntax) (k : Syntax) : M Syntax := withRef action <| wit
 def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFreshMacroScope do
   let kind := decl.getKind
   if kind == ``Parser.Term.doLet then
-    let letDecl := decl[doLetDeclIdx decl]
+    let letDecl := decl[2]
     `(let $letDecl:letDecl; $k)
   else if kind == ``Parser.Term.doLetRec then
     let letRecToken := decl[0]
     let letRecDecls := decl[1]
     return mkNode ``Parser.Term.letrec #[letRecToken, letRecDecls, mkNullNode, k]
   else if kind == ``Parser.Term.doLetArrow then
-    let arg := decl[doLetDeclIdx decl]
+    let arg := decl[2]
     if arg.getKind == ``Parser.Term.doIdDecl then
       let id     := arg[0]
       let type   := expandOptType id arg[1]
@@ -1427,7 +1415,7 @@ mutual
   /-- Generate `CodeBlock` for `doLetArrow; doElems`
      `doLetArrow` is of the form
      ```
-     "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
+     "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
      ```
      where
      ```
@@ -1436,7 +1424,7 @@ mutual
      ```
   -/
   partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    let decl    := doLetArrow[doLetDeclIdx doLetArrow]
+    let decl    := doLetArrow[2]
     if decl.getKind == ``Parser.Term.doIdDecl then
       let y := decl[0]
       checkNotShadowingMutable #[y]
@@ -1487,12 +1475,11 @@ mutual
       throwError "unexpected kind of `do` declaration"
 
   partial def doLetElseToCode (doLetElse : Syntax) (doElems : List Syntax) : M CodeBlock := do
-    -- "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
-    let offset := doLetDeclIdx doLetElse
-    let pattern := doLetElse[offset]
-    let val     := doLetElse[offset + 2]
-    let elseSeq := doLetElse[offset + 4]
-    let bodySeq := doLetElse[offset + 5][0]
+    -- "let " >> optional "mut " >> termParser >> " := " >> termParser >> (checkColGt >> " | " >> doSeq) >> optional doSeq
+    let pattern := doLetElse[2]
+    let val     := doLetElse[4]
+    let elseSeq := doLetElse[6]
+    let bodySeq := doLetElse[7][0]
     let contSeq ← if isMutableLet doLetElse then
       let vars ← (← getPatternVarsEx pattern).mapM fun var => `(doElem| let mut $var := $var)
       pure (vars ++ (getDoSeqElems bodySeq).toArray)

src/Lean/Parser/Do.lean

@@ -67,9 +67,9 @@ def notFollowedByRedefinedTermToken :=
     "token at 'do' element"
 
 @[builtin_doElem_parser] def doLet      := leading_parser
-  "let " >> optional "mut " >> letConfig >> letDecl
+  "let " >> optional "mut " >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|
-  "let " >> optional "mut " >> letConfig >> termParser >> " := " >> termParser >>
+  "let " >> optional "mut " >> termParser >> " := " >> termParser >>
   (checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent)
 
 @[builtin_doElem_parser] def doLetExpr  := leading_parser withPosition <|
@@ -89,7 +89,7 @@ def doPatDecl  := leading_parser
   atomic (termParser >> optType >> ppSpace >> leftArrow) >>
   doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent))
 @[builtin_doElem_parser] def doLetArrow      := leading_parser withPosition <|
-  "let " >> optional "mut " >> letConfig >> (doIdDecl <|> doPatDecl)
+  "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)
 
 /-
 We use `letIdDeclNoBinders` to define `doReassign`.
@@ -114,7 +114,7 @@ def letIdDeclNoBinders := leading_parser
 @[builtin_doElem_parser] def doReassignArrow := leading_parser
   notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
 @[builtin_doElem_parser] def doHave     := leading_parser
-  "have" >> Term.letConfig >> Term.letDecl
+  "have" >> Term.letDecl
 /-
 In `do` blocks, we support `if` without an `else`.
 Thus, we use indentation to prevent examples such as

src/runtime/interrupt.cpp

@@ -5,6 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
+#include <cstdlib>
+#include <ctime>
+#include <execinfo.h>
 #include "runtime/thread.h"
 #include "runtime/interrupt.h"
 #include "runtime/exception.h"
@@ -16,6 +19,63 @@ namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
 LEAN_THREAD_VALUE(size_t, g_heartbeat, 0);
 
+// --- check_system interval monitoring ---
+// When LEAN_CHECK_SYSTEM_INTERVAL_MS is set, warn on stderr if check_system
+// is not called within the given interval (in milliseconds of CPU time) on the
+// current thread. Uses CLOCK_THREAD_CPUTIME_ID so that IO waits (sleep, network,
+// disk) do not count towards the interval.
+
+// 0 = disabled
+static unsigned g_check_system_interval_ms = 0;
+static bool g_check_system_interval_initialized = false;
+
+static unsigned get_check_system_interval_ms() {
+    if (!g_check_system_interval_initialized) {
+        g_check_system_interval_initialized = true;
+        if (const char * env = std::getenv("LEAN_CHECK_SYSTEM_INTERVAL_MS")) {
+            g_check_system_interval_ms = std::atoi(env);
+        }
+    }
+    return g_check_system_interval_ms;
+}
+
+static uint64_t thread_cpu_time_ns() {
+    struct timespec ts;
+    clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts);
+    return static_cast<uint64_t>(ts.tv_sec) * 1000000000ULL + static_cast<uint64_t>(ts.tv_nsec);
+}
+
+// Thread-local: last CPU time when check_system was called on this thread.
+LEAN_THREAD_VALUE(uint64_t, g_last_check_system_ns, 0);
+
+static void check_system_interval(char const * component_name) {
+    unsigned interval_ms = get_check_system_interval_ms();
+    if (interval_ms > 0) {
+        uint64_t now_ns = thread_cpu_time_ns();
+        uint64_t last_ns = g_last_check_system_ns;
+        g_last_check_system_ns = now_ns;
+        if (last_ns != 0) {
+            uint64_t elapsed_ms = (now_ns - last_ns) / 1000000;
+            if (elapsed_ms > interval_ms) {
+                fprintf(stderr,
+                    "[check_system] WARNING: %llu ms CPU time since last check_system call "
+                    "(component: %s)\n",
+                    (unsigned long long)elapsed_ms, component_name);
+                // Reset timer after printing to avoid backtrace overhead cascading
+                g_last_check_system_ns = thread_cpu_time_ns();
+                void * bt_buf[64];
+                int nptrs = backtrace(bt_buf, 64);
+                backtrace_symbols_fd(bt_buf, nptrs, 2); // fd 2 = stderr
+            }
+        }
+    }
+}
+
+extern "C" LEAN_EXPORT obj_res lean_check_system_interval(b_lean_obj_arg component_name) {
+    check_system_interval(lean_string_cstr(component_name));
+    return lean_io_result_mk_ok(lean_box(0));
+}
+
 extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat() {
 #ifdef LEAN_DEFAULT_MAX_HEARTBEAT
     return lean_box(LEAN_DEFAULT_MAX_HEARTBEAT);
@@ -51,6 +111,9 @@ void check_heartbeat() {
     inc_heartbeat();
     if (g_max_heartbeat > 0 && g_heartbeat > g_max_heartbeat)
         throw_heartbeat_exception();
+    if (g_heartbeat % 256 == 0) {
+        check_system("heartbeat");
+    }
 }
 
 LEAN_THREAD_VALUE(lean_object *, g_cancel_tk, nullptr);
@@ -71,6 +134,7 @@ void check_interrupted() {
 }
 
 void check_system(char const * component_name, bool do_check_interrupted) {
+    check_system_interval(component_name);
     check_stack(component_name);
     check_memory(component_name);
     if (do_check_interrupted) {

tests/bench/mvcgen/sym/lib/VCGen.lean

@@ -1032,7 +1032,11 @@ private meta def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM G
   let `(tactic| grind $config:optConfig $[only%$only]? $[ [$grindParams:grindParam,*] ]? $[=> $_:grindSeq]?) := grindStx
     | throwUnsupportedSyntax
   let grindConfig ← elabGrindConfig config
-  mkGrindParams grindConfig only.isSome (grindParams.getD {}).getElems goal
+  let params ← mkGrindParams grindConfig only.isSome (grindParams.getD {}).getElems goal
+  -- FIXME: Expose grind's internal simp step limit as a user-facing option instead of hardcoding.
+  -- Grind's `simpCore` uses the default `Simp.Config.maxSteps` (100k) which is too low for large
+  -- unrolled goals (fails around n=400 for GetThrowSet).
+  return { params with norm := ← params.norm.setConfig { params.norm.config with maxSteps := 10000000 } }
 
 /--
 Build `Sym.Simp.Methods` from a variant name and extra theorems.

tests/elab/string_cases.lean

@@ -1,10 +0,0 @@
--- Test that pattern matching on the `String.ofByteArray` constructor works correctly
--- at runtime.
-
-def getBytes (s : String) : ByteArray :=
-  match s with
-  | ⟨bs, _⟩ => bs
-
-#eval getBytes "hello" |>.size
-#eval getBytes "" |>.size
-#eval getBytes "α" |>.size

tests/elab/string_cases.lean.out.expected

@@ -1,3 +0,0 @@
-5
-0
-2