From cb40ddad69cada36940844e538ddf09a304b007b Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 8 Nov 2024 14:47:10 +0100 Subject: [PATCH] fix: avoid max heartbeat error in completion (#5996) This now occurs for some large completions downstream of `import Mathlib`. I'd like to get rid of this `whnf` call entirely in the future, but this is a decent quick mitigation. --- src/Lean/Server/Completion.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 75623140c2..0312a11714 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -211,10 +211,13 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt return CompletionItemKind.event else if (← isProjectionFn constInfo.name) then return CompletionItemKind.field - else if (← whnf constInfo.type).isForall then - return CompletionItemKind.function else - return CompletionItemKind.constant + let isFunction : Bool ← withTheReader Core.Context ({ · with maxHeartbeats := 0 }) do + return (← whnf constInfo.type).isForall + if isFunction then + return CompletionItemKind.function + else + return CompletionItemKind.constant private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do if let some c := (← getEnv).find? declName then