From 5aae74199b6cc2eb01619f0eaa04285c76cd388d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 12 Oct 2023 10:02:10 +0200
Subject: [PATCH] fix: switch to C++ interruption whitelist

---
 src/kernel/expr_eq_fn.cpp   | 4 +---
 src/kernel/replace_fn.cpp   | 4 +---
 src/kernel/type_checker.cpp | 6 +++---
 src/runtime/interrupt.h     | 6 +++---
 4 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 814faa018b..647bbec2d3 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -61,9 +61,7 @@ class expr_eq_fn {
     eq_cache & m_cache;
 
     static void check_system() {
-        // as this function is used by the pure `Expr.equal`,
-        // we cannot throw a non-fatal exception here
-        ::lean::check_system("expression equality test", /* do_check_interrupted */ false);
+        ::lean::check_system("expression equality test");
     }
 
     bool apply(expr const & a, expr const & b) {
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index b4fc06b0e5..f0b995d6d1 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -73,9 +73,7 @@ class replace_rec_fn {
                 return *r;
             shared = true;
         }
-        // as this function is used by pure functions such as `lean_expr_instantiate`,
-        // we cannot throw a non-fatal exception here
-        check_system("replace", /* do_check_interrupted */ false);
+        check_system("replace");
 
         if (optional<expr> r = m_f(e, offset)) {
             return save_result(e, offset, *r, shared);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 281a17a6d1..6ba0b00dbf 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -286,7 +286,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
         throw kernel_exception(env(), "type checker does not support loose bound variables, replace them with free variables before invoking it");
 
     lean_assert(!has_loose_bvars(e));
-    check_system("type checker");
+    check_system("type checker", /* do_check_interrupted */ true);
 
     auto it = m_st->m_infer_type[infer_only].find(e);
     if (it != m_st->m_infer_type[infer_only].end())
@@ -409,7 +409,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) {
-    check_system("type checker: whnf");
+    check_system("type checker: whnf", /* do_check_interrupted */ true);
 
     // handle easy cases
     switch (e.kind()) {
@@ -1000,7 +1000,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) {
-    check_system("is_definitionally_equal");
+    check_system("is_definitionally_equal", /* do_check_interrupted */ true);
     bool use_hash = true;
     lbool r = quick_is_def_eq(t, s, use_hash);
     if (r != l_undef) return r == l_true;
diff --git a/src/runtime/interrupt.h b/src/runtime/interrupt.h
index ace464cc89..4e628fb511 100644
--- a/src/runtime/interrupt.h
+++ b/src/runtime/interrupt.h
@@ -50,11 +50,11 @@ void check_interrupted();
 /**
    \brief Check system resources: stack, memory, heartbeat, interrupt flag.
 
-   `do_check_interrupted` should be set to `false` in places where a C++ exception
-   is not caught and would bring down the entire process as interruption
+   `do_check_interrupted` should only be set to `true` in places where a C++ exception
+   is caught and would not bring down the entire process as interruption
    should not be a fatal error.
 */
-void check_system(char const * component_name, bool do_check_interrupted = true);
+void check_system(char const * component_name, bool do_check_interrupted = false);
 
 constexpr unsigned g_small_sleep = 10;