From f64bce6ef178c111f113647de131535db19ef096 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 27 Jan 2025 22:15:09 +0100 Subject: [PATCH] fix: auto-completion performance regression (#6794) This PR fixes a significant auto-completion performance regression that was introduced in #5666, i.e. v4.14.0. #5666 introduced tactic docstrings, which were attempted to be collected for every single completion item. This is slow for hundreds of thousands of completion items. To fix this, this PR moves the docstring computation into the completion item resolution, which is only called when users select a specific completion item in the UI. A downside of this approach is that we currently can't test completion item resolution, so we lose a few tests that cover docstrings in completions in this PR. --- .../Completion/CompletionCollectors.lean | 30 +++----------- .../Completion/CompletionResolution.lean | 28 +++++++++++++ tests/lean/interactive/1265.lean.expected.out | 4 -- .../completionDeprecation.lean.expected.out | 22 ---------- .../lean/interactive/completionDocString.lean | 2 - .../completionDocString.lean.expected.out | 41 ------------------- .../completionPrv.lean.expected.out | 3 -- .../travellingCompletions.lean.expected.out | 4 -- 8 files changed, 33 insertions(+), 101 deletions(-) delete mode 100644 tests/lean/interactive/completionDocString.lean delete mode 100644 tests/lean/interactive/completionDocString.lean.expected.out diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 8fb4cffc03..97ff51ce9d 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -65,32 +65,12 @@ section Infrastructure (score : Float) : M Unit := do let env ← getEnv - let (docStringPrefix?, tags?) := Id.run do + let tags? := do let .const declName := id - | (none, none) - let some param := Linter.deprecatedAttr.getParam? env declName - | (none, none) - let docstringPrefix := - if let some text := param.text? then - text - else if let some newName := param.newName? then - s!"`{declName}` has been deprecated, use `{newName}` instead." - else - s!"`{declName}` has been deprecated." - (some docstringPrefix, some #[CompletionItemTag.deprecated]) - let docString? ← do - let .const declName := id - | pure none - findDocString? env declName - let doc? := do - let docValue ← - match docStringPrefix?, docString? with - | none, none => none - | some docStringPrefix, none => docStringPrefix - | none, docString => docString - | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}" - pure { value := docValue , kind := MarkupKind.markdown : MarkupContent } - let item := { label := label.toString, kind? := kind, documentation? := doc?, tags?} + | none + guard <| Linter.isDeprecated env declName + some #[CompletionItemTag.deprecated] + let item := { label := label.toString, kind? := kind, tags? } addItem item score id private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do diff --git a/src/Lean/Server/Completion/CompletionResolution.lean b/src/Lean/Server/Completion/CompletionResolution.lean index 48e4302c3d..c071840192 100644 --- a/src/Lean/Server/Completion/CompletionResolution.lean +++ b/src/Lean/Server/Completion/CompletionResolution.lean @@ -62,6 +62,34 @@ def CompletionItem.resolve return toString (← Meta.ppExpr typeWithoutImplicits) item := { item with detail? := detail? } + if item.documentation?.isNone then + let docStringPrefix? := Id.run do + let .const declName := id + | none + let some param := Linter.deprecatedAttr.getParam? env declName + | none + let docstringPrefix := + if let some text := param.text? then + text + else if let some newName := param.newName? then + s!"`{declName}` has been deprecated, use `{newName}` instead." + else + s!"`{declName}` has been deprecated." + some docstringPrefix + let docString? ← do + let .const declName := id + | pure none + findDocString? env declName + let doc? := do + let docValue ← + match docStringPrefix?, docString? with + | none, none => none + | some docStringPrefix, none => docStringPrefix + | none, docString => docString + | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}" + pure { value := docValue , kind := MarkupKind.markdown : MarkupContent } + item := { item with documentation? := doc? } + return item end Lean.Lsp diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out index 0f91b29507..92cc3b8184 100644 --- a/tests/lean/interactive/1265.lean.expected.out +++ b/tests/lean/interactive/1265.lean.expected.out @@ -85,8 +85,6 @@ {"sortText": "9", "label": "raw", "kind": 5, - "documentation": - {"value": "The underlying `Syntax` value. ", "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///1265.lean"}, @@ -181,8 +179,6 @@ {"sortText": "9", "label": "raw", "kind": 5, - "documentation": - {"value": "The underlying `Syntax` value. ", "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///1265.lean"}, diff --git a/tests/lean/interactive/completionDeprecation.lean.expected.out b/tests/lean/interactive/completionDeprecation.lean.expected.out index 1550a8f6ea..e32f3a19ff 100644 --- a/tests/lean/interactive/completionDeprecation.lean.expected.out +++ b/tests/lean/interactive/completionDeprecation.lean.expected.out @@ -13,7 +13,6 @@ {"sortText": "1", "label": "foo2", "kind": 3, - "documentation": {"value": "A docstring. ", "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -24,8 +23,6 @@ "sortText": "2", "label": "foo3", "kind": 3, - "documentation": - {"value": "`SomeStructure.foo3` has been deprecated.", "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -36,9 +33,6 @@ "sortText": "3", "label": "foo4", "kind": 3, - "documentation": - {"value": "`SomeStructure.foo4` has been deprecated.\n\nA docstring. ", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -49,10 +43,6 @@ "sortText": "4", "label": "foo5", "kind": 3, - "documentation": - {"value": - "`SomeStructure.foo5` has been deprecated, use `SomeStructure.foo1` instead.", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -63,10 +53,6 @@ "sortText": "5", "label": "foo6", "kind": 3, - "documentation": - {"value": - "`SomeStructure.foo6` has been deprecated, use `SomeStructure.foo1` instead.\n\nA docstring. ", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -77,10 +63,6 @@ "sortText": "6", "label": "foo7", "kind": 3, - "documentation": - {"value": - "`SomeStructure.foo7` has been deprecated; please use `SomeStructure.foo1` instead.", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, @@ -91,10 +73,6 @@ "sortText": "7", "label": "foo8", "kind": 3, - "documentation": - {"value": - "`SomeStructure.foo8` has been deprecated; please use `SomeStructure.foo1` instead.\n\nA docstring. ", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionDeprecation.lean"}, diff --git a/tests/lean/interactive/completionDocString.lean b/tests/lean/interactive/completionDocString.lean deleted file mode 100644 index 4711f7e99f..0000000000 --- a/tests/lean/interactive/completionDocString.lean +++ /dev/null @@ -1,2 +0,0 @@ -#eval Array.insertIdx - --^ textDocument/completion diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out deleted file mode 100644 index 5e16bdbe37..0000000000 --- a/tests/lean/interactive/completionDocString.lean.expected.out +++ /dev/null @@ -1,41 +0,0 @@ -{"textDocument": {"uri": "file:///completionDocString.lean"}, - "position": {"line": 0, "character": 21}} -{"items": - [{"sortText": "0", - "label": "insertIdx", - "kind": 3, - "documentation": - {"value": "Insert element `a` at position `i`. ", "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionDocString.lean"}, - "position": {"line": 0, "character": 21}}, - "id": {"const": {"declName": "Array.insertIdx"}}, - "cPos": 0}}, - {"sortText": "1", - "label": "insertIdxIfInBounds", - "kind": 3, - "documentation": - {"value": - "Insert element `a` at position `i`, or do nothing if `as.size < i`. ", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionDocString.lean"}, - "position": {"line": 0, "character": 21}}, - "id": {"const": {"declName": "Array.insertIdxIfInBounds"}}, - "cPos": 0}}, - {"sortText": "2", - "label": "insertIdx!", - "kind": 3, - "documentation": - {"value": - "Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. ", - "kind": "markdown"}, - "data": - {"params": - {"textDocument": {"uri": "file:///completionDocString.lean"}, - "position": {"line": 0, "character": 21}}, - "id": {"const": {"declName": "Array.insertIdx!"}}, - "cPos": 0}}], - "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index 319c5da1fd..a81d2fa8b2 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -89,9 +89,6 @@ {"sortText": "8", "label": "BitVec.ofBoolListBE", "kind": 3, - "documentation": - {"value": "Converts a list of `Bool`s to a big-endian `BitVec`. ", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, diff --git a/tests/lean/interactive/travellingCompletions.lean.expected.out b/tests/lean/interactive/travellingCompletions.lean.expected.out index b04e4b81cd..412c2bf6a1 100644 --- a/tests/lean/interactive/travellingCompletions.lean.expected.out +++ b/tests/lean/interactive/travellingCompletions.lean.expected.out @@ -65,10 +65,6 @@ [{"sortText": "0", "label": "intro", "kind": 4, - "documentation": - {"value": - "`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ", - "kind": "markdown"}, "data": {"params": {"textDocument": {"uri": "file:///travellingCompletions.lean"},