From f42a28f7182141ebd7646e23dc0f391b669ebed2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 20 Mar 2025 08:04:50 +0100 Subject: [PATCH] chore: revert "perf: avoid taking mutex on task deactivation" (#7590) Likely introduced segfaults. Reverts leanprover/lean4#7572 --- src/runtime/object.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index eb0e32bb3d..f03f0de521 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -926,12 +926,6 @@ public: } void deactivate_task(lean_task_object * t) { - if (object * v = t->m_value) { - lean_assert(t->m_imp == nullptr); - lean_dec(v); - free_task(t); - return; - } unique_lock lock(m_mutex); if (object * v = t->m_value) { lean_assert(t->m_imp == nullptr);