From 2d3dec41ca8c1fe670dba2afc2147904e4854409 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Dec 2025 18:24:01 +0100 Subject: [PATCH] perf: avoid blocking on proof elaboration in `Environment.hasUnsafe` (#11606) --- src/Lean/Environment.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index d77fdafce4..74a318d31b 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -2503,6 +2503,10 @@ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName : | _ => throwUnexpectedType typeName constName def hasUnsafe (env : Environment) (e : Expr) : Bool := + -- This line should not affect the result value but it avoids potential blocking in `isUnsafe` as + -- there is a fast path for theorems, so we want to make sure we do not perceive them merely as + -- axioms (for imported theorems this does not matter as there is nothing to block on). + let env := env.setExporting false let c? := e.find? fun e => match e with | Expr.const c _ => match env.findAsync? c with