perf: eliminate checkSystemInterval overhead when disabled

Skip the FFI call to lean_check_system_interval entirely when
LEAN_CHECK_SYSTEM_INTERVAL_MS is unset by checking a builtin_initialize'd
Bool flag inline.

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

src/Lean/CoreM.lean

@@ -446,6 +446,24 @@ Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.get
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
+/--
+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"]
+private opaque checkSystemIntervalImpl (componentName : @& String) : BaseIO Unit
+
+@[extern "lean_check_system_interval_is_enabled"]
+private opaque checkSystemIntervalIsEnabled : Unit → Bool
+
+private builtin_initialize checkSystemIntervalEnabled : Bool ←
+  pure (checkSystemIntervalIsEnabled ())
+
+@[inline] def checkSystemInterval (componentName : @& String) : BaseIO Unit := do
+  if checkSystemIntervalEnabled then
+    checkSystemIntervalImpl componentName
+
 /--
 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
@@ -456,6 +474,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/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,68 @@ 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=N is set, warn on stderr if check_system
+// is not called within N milliseconds of CPU time on the current thread.
+// Uses CLOCK_THREAD_CPUTIME_ID so that IO waits do not count towards the interval.
+// Zero overhead when env var is unset.
+
+// 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);
+                void * bt_buf[64];
+                int nptrs = backtrace(bt_buf, 64);
+                backtrace_symbols_fd(bt_buf, nptrs, 2); // fd 2 = stderr
+                // Reset timer after printing to avoid backtrace overhead cascading
+                g_last_check_system_ns = thread_cpu_time_ns();
+            }
+        }
+    }
+}
+
+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 uint8_t lean_check_system_interval_is_enabled(lean_obj_arg /* unit */) {
+    return get_check_system_interval_ms() > 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);
@@ -71,6 +136,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) {