max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: switch to C++ interruption whitelist

Browse source
This commit is contained in:
Sebastian Ullrich 2023-10-12 10:02:10 +02:00
parent c0e3b9568e
commit 5aae74199b
4 changed files with 8 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/expr_eq_fn.cpp
View file

@ -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) {

4
src/kernel/replace_fn.cpp
View file

@ -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);

6
src/kernel/type_checker.cpp
View file

@ -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;

6
src/runtime/interrupt.h
View file

@ -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;