From 34d619bf9324e1835a3e9471b40d00a7520ada8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 18 Dec 2025 15:24:50 +0100 Subject: [PATCH] perf: use lean::unordered_set for expr_eq_fn (#11731) This PR makes the cache in expr_eq_fn use mimalloc for a small performance win across the board. --- src/kernel/expr_eq_fn.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index a5cf5cdcfe..74dd69ed4b 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "runtime/thread.h" #include "kernel/expr.h" #include "kernel/expr_sets.h" +#include "util/alloc.h" namespace lean { /** @@ -26,7 +27,7 @@ class expr_eq_fn { return hash((size_t)p.first >> 3, (size_t)p.second >> 3); } }; - typedef std::unordered_set, key_hasher> cache; + typedef lean::unordered_set, key_hasher> cache; cache * m_cache = nullptr; size_t m_max_stack_depth = 0; size_t m_counter = 0;