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.
2025-01-27 22:15:09 +01:00 · 2025-01-27 22:15:09 +01:00 · f64bce6ef1
commit f64bce6ef1
parent 0160aa1a89
8 changed files with 33 additions and 101 deletions
--- 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
--- 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
--- 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"},
--- 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"},
--- a/tests/lean/interactive/completionDocString.lean
+++ b/tests/lean/interactive/completionDocString.lean
@ -1,2 +0,0 @@
-#eval Array.insertIdx
-                   --^ textDocument/completion
--- a/tests/lean/interactive/completionDocString.lean.expected.out
+++ b/tests/lean/interactive/completionDocString.lean.expected.out
@ -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}
--- 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"},
--- 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"},