max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: avoid max heartbeat error in completion (#5996)

Browse source 
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.
This commit is contained in:
Marc Huisinga 2024-11-08 14:47:10 +01:00 • committed by GitHub
parent fc0529b020
commit cb40ddad69
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Server/Completion.lean
View file

@ -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