chore: put throws in separate function for debugger

src/Lean/Environment.lean

@@ -222,6 +222,9 @@ inductive KernelException where
   | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
   | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
   | other            (msg : String)
+  | deterministicTimeout
+  | excessiveMemory
+  | deepRecursion
 
 namespace Environment
 

src/Lean/Message.lean

@@ -361,6 +361,9 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
     mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}"
   | invalidProj env lctx e              => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}"
   | other msg                           => m!"(kernel) {msg}"
+  | deterministicTimeout                => "(kernel) deterministic timeout"
+  | excessiveMemory                     => "(kernel) excessive memory consumption detected"
+  | deepRecursion                       => "(kernel) deep recursion detected"
 
 end KernelException
 end Lean

src/kernel/kernel_exception.h

@@ -202,6 +202,15 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (exception & ex) {
         // 11 | other            (msg : String)
         return mk_cnstr(0, mk_cnstr(11, string_ref(ex.what()))).steal();
+    } catch (heartbeat_exception & ex) {
+        // 12 | deterministicTimeout
+        return mk_cnstr(0, box(12)).steal();
+    } catch (memory_exception & ex) {
+        // 13 | excessiveMemory
+        return mk_cnstr(0, box(13)).steal();
+    } catch (stack_space_exception & ex) {
+        // 14 | deepRecursion
+        return mk_cnstr(0, box(14)).steal();
     }
 }
 }

src/runtime/interrupt.cpp

@@ -27,10 +27,15 @@ void set_max_heartbeat_thousands(unsigned max) { g_max_heartbeat = static_cast<s
 scope_heartbeat::scope_heartbeat(size_t max):flet<size_t>(g_heartbeat, max) {}
 scope_max_heartbeat::scope_max_heartbeat(size_t max):flet<size_t>(g_max_heartbeat, max) {}
 
+// separate definition to allow breakpoint in debugger
+void throw_heartbeat_exception() {
+    throw heartbeat_exception();
+}
+
 void check_heartbeat() {
     inc_heartbeat();
     if (g_max_heartbeat > 0 && g_heartbeat > g_max_heartbeat)
-        throw heartbeat_exception();
+        throw_heartbeat_exception();
 }
 
 LEAN_THREAD_VALUE(atomic_bool *, g_interrupt_flag, nullptr);

src/runtime/memory.cpp

@@ -124,6 +124,11 @@ void set_max_memory_megabyte(unsigned max) {
     set_max_memory(m);
 }
 
+// separate definition to allow breakpoint in debugger
+void throw_memory_exception(char const * component_name) {
+    throw memory_exception(component_name);
+}
+
 void check_memory(char const * component_name) {
     if (g_max_memory == 0) return;
     g_counter++;
@@ -135,7 +140,7 @@ void check_memory(char const * component_name) {
         if (r > 0 && r < g_max_memory) return;
         r = get_current_rss();
         if (r == 0 || r < g_max_memory) return;
-        throw memory_exception(component_name);
+        throw_memory_exception(component_name);
     }
 }
 

src/runtime/stackinfo.cpp

@@ -92,13 +92,18 @@ size_t get_available_stack_size() {
         return g_stack_size - sz;
 }
 
+// separate definition to allow breakpoint in debugger
+void throw_stack_space_exception(char const * component_name) {
+    throw stack_space_exception(component_name);
+}
+
 void check_stack(char const * component_name) {
     if (!g_stack_info_init)
         save_stack_info(false);
     char y;
     size_t curr_stack = reinterpret_cast<size_t>(&y);
     if (curr_stack < g_stack_threshold)
-        throw stack_space_exception(component_name);
+        throw_stack_space_exception(component_name);
 }
 }
 #endif