From fa3cf4d613b0df0617821e99397704e28858ce9f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 10 Oct 2023 17:26:54 +0200
Subject: [PATCH] feat: translate `interrupted` kernel exception

---
 src/Lean/Environment.lean     |  1 +
 src/Lean/Message.lean         |  1 +
 src/kernel/kernel_exception.h | 19 ++++---------------
 3 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8fb7da9258..c81573aa63 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -230,6 +230,7 @@ inductive KernelException where
   | deterministicTimeout
   | excessiveMemory
   | deepRecursion
+  | interrupted
 
 namespace Environment
 
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index cfb3508279..459873e4d2 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -370,6 +370,7 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"
   | deepRecursion                       => "(kernel) deep recursion detected"
+  | interrupted                         => "(kernel) interrupted"
 
 end KernelException
 end Lean
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index f5d66133ee..930185828f 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
+#include "runtime/interrupt.h"
 
 namespace lean {
 /** \brief Base class for all kernel exceptions. */
@@ -145,21 +146,6 @@ an `kernel_exception` or `exception`. Then, convert result into `Except KernelEx
 where `T` is the type of the lean objected represented by `A`.
 We use the constructor `KernelException.other <msg>` to handle C++ `exception` objects which
 are not `kernel_exception`.
-```
-inductive KernelException
-0  | unknownConstant  (env : Environment) (name : Name)
-1  | alreadyDeclared  (env : Environment) (name : Name)
-2  | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
-3  | declHasMVars     (env : Environment) (name : Name) (expr : Expr)
-4  | declHasFVars     (env : Environment) (name : Name) (expr : Expr)
-5  | funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
-6  | typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
-7  | letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
-8  | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
-9  | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
-10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
-11 | other            (msg : String)
-```
 */
 template<typename A>
 object * catch_kernel_exceptions(std::function<A()> const & f) {
@@ -211,6 +197,9 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (stack_space_exception & ex) {
         // 14 | deepRecursion
         return mk_cnstr(0, box(14)).steal();
+    } catch (interrupted & ex) {
+        // 15 | interrupted
+        return mk_cnstr(0, box(15)).steal();
     }
 }
 }