From 30e23eae2be62356a8a3fb4fa4a60ba6a03975b2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 18 Jan 2026 20:33:48 +0100 Subject: [PATCH] perf: avoid allocation on `lean_trace` use in interpreter (#12036) After #12001, it was no longer true that `lean_trace(name(...), ...)` would only perform the name allocation if no trace option was set. This PR instead avoids the allocation in any case by avoiding this pattern. --- .github/workflows/ci.yml | 4 ++-- src/library/ir_interpreter.cpp | 21 ++++++++++++++------- src/util/options.cpp | 4 ++-- 3 files changed, 18 insertions(+), 11 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index de1cc73d87..0e960459a0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -275,9 +275,9 @@ jobs: // * `bv_` sometimes times out calling into cadical even though we should be using // the standard compile flags for it. // * `grind_guide` always times out. - // * `pkg/` tests sometimes time out (likely even hang), related to Lake CI + // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI // failures? - "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/'" + "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'" }, { "name": "macOS", diff --git a/src/library/ir_interpreter.cpp b/src/library/ir_interpreter.cpp index 321e630f04..9766c2dd79 100644 --- a/src/library/ir_interpreter.cpp +++ b/src/library/ir_interpreter.cpp @@ -202,6 +202,8 @@ extern "C" float lean_float32_of_nat(lean_obj_arg a); static string_ref * g_boxed_mangled_suffix = nullptr; static name * g_interpreter_prefer_native = nullptr; +DEBUG_CODE(static name * g_interpreter_step = nullptr;) +DEBUG_CODE(static name * g_interpreter_call = nullptr;) // constants (lacking native declarations) initialized by `lean_run_init` // We can assume this variable is never written to and read from in parallel; see `enableInitializersExecution`. @@ -638,7 +640,7 @@ private: // make reference reassignable... std::reference_wrapper b(b0); while (true) { - DEBUG_CODE(lean_trace(name({"interpreter", "step"}), + DEBUG_CODE(lean_trace(*g_interpreter_step, tout() << std::string(m_call_stack.size(), ' ') << format_fn_body_head(b) << "\n";);) switch (fn_body_tag(b)) { case fn_body_kind::VDecl: { // variable declaration @@ -668,7 +670,7 @@ private: // NOTE: `var` must be called *after* `eval_expr` because the stack may get resized and invalidate // the pointer var(fn_body_vdecl_var(b)) = v; - DEBUG_CODE(lean_trace(name({"interpreter", "step"}), + DEBUG_CODE(lean_trace(*g_interpreter_step, tout() << std::string(m_call_stack.size(), ' ') << "=> x_"; tout() << fn_body_vdecl_var(b).get_small_value() << " = "; print_value(tout(), var(fn_body_vdecl_var(b)), fn_body_vdecl_type(b)); @@ -793,7 +795,7 @@ private: // specify argument base pointer explicitly because we've usually already pushed some function arguments void push_frame(decl const & d, size_t arg_bp) { DEBUG_CODE({ - lean_trace(name({"interpreter", "call"}), + lean_trace(*g_interpreter_call, tout() << std::string(m_call_stack.size(), ' ') << decl_fun_id(d); for (size_t i = arg_bp; i < m_arg_stack.size(); i++) { @@ -809,7 +811,7 @@ private: m_jp_stack.resize(get_frame().m_jp_bp); m_call_stack.pop_back(); DEBUG_CODE({ - lean_trace(name({"interpreter", "call"}), + lean_trace(*g_interpreter_call, tout() << std::string(m_call_stack.size(), ' ') << "=> "; print_value(tout(), r, t); @@ -1216,9 +1218,10 @@ void initialize_ir_interpreter() { ir::g_init_globals = new name_hash_map(); register_bool_option(*ir::g_interpreter_prefer_native, LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE, "(interpreter) whether to use precompiled code where available"); DEBUG_CODE({ - register_trace_class({"interpreter"}); - register_trace_class({"interpreter", "call"}); - register_trace_class({"interpreter", "step"}); + ir::g_interpreter_call = new name({"interpreter", "call"}); + register_trace_class(*ir::g_interpreter_call); + ir::g_interpreter_step = new name({"interpreter", "step"}); + register_trace_class(*ir::g_interpreter_step); }); ir::g_native_symbol_cache = new name_hash_map(); ir::g_native_symbol_cache_mutex = new std::shared_timed_mutex(); @@ -1227,6 +1230,10 @@ void initialize_ir_interpreter() { void finalize_ir_interpreter() { delete ir::g_native_symbol_cache_mutex; delete ir::g_native_symbol_cache; + DEBUG_CODE({ + delete ir::g_interpreter_call; + delete ir::g_interpreter_step; + }); delete ir::g_init_globals; delete ir::g_interpreter_prefer_native; delete ir::g_boxed_mangled_suffix; diff --git a/src/util/options.cpp b/src/util/options.cpp index 3d4200e4f2..8c307e0c1c 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -61,8 +61,8 @@ extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) { return get_default_options().steal(); } -extern "C" LEAN_EXPORT obj_res lean_options_get_empty(); -options::options(): object_ref(lean_options_get_empty()) {} +extern "C" LEAN_EXPORT obj_res lean_options_get_empty(obj_arg u); +options::options(): object_ref(lean_options_get_empty(box(0))) {} extern "C" LEAN_EXPORT bool lean_options_get_bool(obj_arg opts, obj_arg n, bool default_value); bool options::get_bool(name const & n, bool default_value) const {