fix: set data? field in eager code actions (#12332)

This PR fixes an issue on new NeoVim versions that would cause the language server to display an error when using certain code actions. (For some reason, NeoVim recently decided to diverge from VS Code in terms of when it emits code action resolution requests, which means that not setting the `data?` field won't preclude NeoVim from emitting a request anymore, which in turn means that the server can't resolve the code action.)
2026-02-06 09:57:27 +01:00 · 2026-02-06 09:57:27 +01:00 · f4c5f8e422
commit f4c5f8e422
parent 6cf632bef2
7 changed files with 1570 additions and 51 deletions
--- a/src/Lean/Server/CodeActions/Basic.lean
+++ b/src/Lean/Server/CodeActions/Basic.lean
@ -134,7 +134,6 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array
        RequestM.checkCancelled
        let cas ← cap params snap
        cas.mapIdxM fun i lca => do
-          if lca.lazy?.isNone then return lca.eager
          let data : CodeActionResolveData := {
            params, providerName, providerResultIndex := i
          }
@ -165,7 +164,8 @@ def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAct
      let some ca := cas[data.providerResultIndex]?
        | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}."
      let some lazy := ca.lazy?
-        | throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve."
+        -- Eager code action - return unchanged
+        | return param
      let r ← liftM lazy
      return r

--- a/tests/lean/interactive/builtinCodeactions.lean.expected.out
+++ b/tests/lean/interactive/builtinCodeactions.lean.expected.out
@ -13,4 +13,36 @@
       {"start": {"line": 5, "character": 2},
        "end": {"line": 5, "character": 97}},
       "newText":
-       "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}}]
+       "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///builtinCodeactions.lean"},
+    "range":
+    {"start": {"line": 5, "character": 4}, "end": {"line": 5, "character": 4}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,
+    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h:
+{"title":
+ "Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///builtinCodeactions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 5, "character": 2},
+       "end": {"line": 5, "character": 97}},
+      "newText":
+      "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///builtinCodeactions.lean"},
+   "range":
+   {"start": {"line": 5, "character": 4}, "end": {"line": 5, "character": 4}},
+   "context": {"diagnostics": []}}}}
--- a/tests/lean/interactive/codeActions.lean.expected.out
+++ b/tests/lean/interactive/codeActions.lean.expected.out
@ -11,7 +11,35 @@
     [{"range":
       {"start": {"line": 56, "character": 0},
        "end": {"line": 56, "character": 16}},
-       "newText": "foo"}]}]}}]
+       "newText": "foo"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "foo",
+   "params":
+   {"textDocument": {"uri": "file:///codeActions.lean"},
+    "range":
+    {"start": {"line": 56, "character": 4},
+     "end": {"line": 56, "character": 4}},
+    "context": {"diagnostics": []}}}}]
+Resolution of foo:
+{"title": "foo",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 56, "character": 0},
+       "end": {"line": 56, "character": 16}},
+      "newText": "foo"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "foo",
+  "params":
+  {"textDocument": {"uri": "file:///codeActions.lean"},
+   "range":
+   {"start": {"line": 56, "character": 4}, "end": {"line": 56, "character": 4}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///codeActions.lean"},
 "range":
 {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}},
@ -25,7 +53,16 @@
     [{"range":
       {"start": {"line": 59, "character": 0},
        "end": {"line": 59, "character": 4}},
-       "newText": "#eval 0"}]}]}},
+       "newText": "#eval 0"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "Lean.CodeAction.cmdCodeActionProvider",
+   "params":
+   {"textDocument": {"uri": "file:///codeActions.lean"},
+    "range":
+    {"start": {"line": 59, "character": 2},
+     "end": {"line": 59, "character": 2}},
+    "context": {"diagnostics": []}}}},
 {"title": "foo",
  "kind": "quickfix",
  "edit":
@ -35,7 +72,54 @@
     [{"range":
       {"start": {"line": 59, "character": 0},
        "end": {"line": 59, "character": 4}},
-       "newText": "foo"}]}]}}]
+       "newText": "foo"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "foo",
+   "params":
+   {"textDocument": {"uri": "file:///codeActions.lean"},
+    "range":
+    {"start": {"line": 59, "character": 2},
+     "end": {"line": 59, "character": 2}},
+    "context": {"diagnostics": []}}}}]
+Resolution of bar:
+{"title": "bar",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 59, "character": 0},
+       "end": {"line": 59, "character": 4}},
+      "newText": "#eval 0"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "Lean.CodeAction.cmdCodeActionProvider",
+  "params":
+  {"textDocument": {"uri": "file:///codeActions.lean"},
+   "range":
+   {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}},
+   "context": {"diagnostics": []}}}}
+Resolution of foo:
+{"title": "foo",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 59, "character": 0},
+       "end": {"line": 59, "character": 4}},
+      "newText": "foo"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "foo",
+  "params":
+  {"textDocument": {"uri": "file:///codeActions.lean"},
+   "range":
+   {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///codeActions.lean"},
 "range":
 {"start": {"line": 62, "character": 18}, "end": {"line": 62, "character": 18}},
@ -49,7 +133,16 @@
     [{"range":
       {"start": {"line": 62, "character": 17},
        "end": {"line": 62, "character": 18}},
-       "newText": "\"foobar\""}]}]}},
+       "newText": "\"foobar\""}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "Lean.CodeAction.holeCodeActionProvider",
+   "params":
+   {"textDocument": {"uri": "file:///codeActions.lean"},
+    "range":
+    {"start": {"line": 62, "character": 18},
+     "end": {"line": 62, "character": 18}},
+    "context": {"diagnostics": []}}}},
 {"title": "foo",
  "kind": "quickfix",
  "edit":
@ -59,4 +152,53 @@
     [{"range":
       {"start": {"line": 62, "character": 0},
        "end": {"line": 62, "character": 18}},
-       "newText": "foo"}]}]}}]
+       "newText": "foo"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "foo",
+   "params":
+   {"textDocument": {"uri": "file:///codeActions.lean"},
+    "range":
+    {"start": {"line": 62, "character": 18},
+     "end": {"line": 62, "character": 18}},
+    "context": {"diagnostics": []}}}}]
+Resolution of foobar:
+{"title": "foobar",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 62, "character": 17},
+       "end": {"line": 62, "character": 18}},
+      "newText": "\"foobar\""}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "Lean.CodeAction.holeCodeActionProvider",
+  "params":
+  {"textDocument": {"uri": "file:///codeActions.lean"},
+   "range":
+   {"start": {"line": 62, "character": 18},
+    "end": {"line": 62, "character": 18}},
+   "context": {"diagnostics": []}}}}
+Resolution of foo:
+{"title": "foo",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 62, "character": 0},
+       "end": {"line": 62, "character": 18}},
+      "newText": "foo"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "foo",
+  "params":
+  {"textDocument": {"uri": "file:///codeActions.lean"},
+   "range":
+   {"start": {"line": 62, "character": 18},
+    "end": {"line": 62, "character": 18}},
+   "context": {"diagnostics": []}}}}
--- a/tests/lean/interactive/codeaction.lean.expected.out
+++ b/tests/lean/interactive/codeaction.lean.expected.out
@ -11,7 +11,16 @@
     [{"range":
       {"start": {"line": 28, "character": 4},
        "end": {"line": 28, "character": 4}},
-       "newText": "hello!!!"}]}]}},
+       "newText": "hello!!!"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName": "helloProvider",
+   "params":
+   {"textDocument": {"uri": "file:///codeaction.lean"},
+    "range":
+    {"start": {"line": 28, "character": 4},
+     "end": {"line": 28, "character": 4}},
+    "context": {"diagnostics": []}}}},
 {"title": "a long-running action",
  "kind": "refactor",
  "data":
@ -23,6 +32,25 @@
    {"start": {"line": 28, "character": 4},
     "end": {"line": 28, "character": 4}},
    "context": {"diagnostics": []}}}}]
+Resolution of hello world:
+{"title": "hello world",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///codeaction.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 28, "character": 4},
+       "end": {"line": 28, "character": 4}},
+      "newText": "hello!!!"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName": "helloProvider",
+  "params":
+  {"textDocument": {"uri": "file:///codeaction.lean"},
+   "range":
+   {"start": {"line": 28, "character": 4}, "end": {"line": 28, "character": 4}},
+   "context": {"diagnostics": []}}}}
 Resolution of a long-running action:
 {"title": "a long-running action",
 "kind": "refactor",
--- a/tests/lean/interactive/structInstFieldHints.lean.expected.out
+++ b/tests/lean/interactive/structInstFieldHints.lean.expected.out
--- a/tests/lean/interactive/terminationBySuggestion.lean.expected.out
+++ b/tests/lean/interactive/terminationBySuggestion.lean.expected.out
@ -12,7 +12,37 @@
     [{"range":
       {"start": {"line": 4, "character": 0},
        "end": {"line": 4, "character": 15}},
-       "newText": "termination_by (n, m)"}]}]}}]
+       "newText": "termination_by (n, m)"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+    "range":
+    {"start": {"line": 4, "character": 5}, "end": {"line": 4, "character": 5}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: termination_by (n, m):
+{"title": "Try this: termination_by (n, m)",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 4, "character": 0},
+       "end": {"line": 4, "character": 15}},
+      "newText": "termination_by (n, m)"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+   "range":
+   {"start": {"line": 4, "character": 5}, "end": {"line": 4, "character": 5}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
 "range":
 {"start": {"line": 11, "character": 5}, "end": {"line": 11, "character": 5}},
@ -27,7 +57,38 @@
     [{"range":
       {"start": {"line": 11, "character": 0},
        "end": {"line": 11, "character": 15}},
-       "newText": "termination_by structural n"}]}]}}]
+       "newText": "termination_by structural n"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+    "range":
+    {"start": {"line": 11, "character": 5},
+     "end": {"line": 11, "character": 5}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: termination_by structural n:
+{"title": "Try this: termination_by structural n",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 11, "character": 0},
+       "end": {"line": 11, "character": 15}},
+      "newText": "termination_by structural n"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+   "range":
+   {"start": {"line": 11, "character": 5}, "end": {"line": 11, "character": 5}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
 "range":
 {"start": {"line": 17, "character": 5}, "end": {"line": 17, "character": 5}},
@ -42,7 +103,38 @@
     [{"range":
       {"start": {"line": 17, "character": 0},
        "end": {"line": 17, "character": 15}},
-       "newText": "termination_by structural x => x"}]}]}}]
+       "newText": "termination_by structural x => x"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+    "range":
+    {"start": {"line": 17, "character": 5},
+     "end": {"line": 17, "character": 5}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: termination_by structural x => x:
+{"title": "Try this: termination_by structural x => x",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 17, "character": 0},
+       "end": {"line": 17, "character": 15}},
+      "newText": "termination_by structural x => x"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+   "range":
+   {"start": {"line": 17, "character": 5}, "end": {"line": 17, "character": 5}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
 "range":
 {"start": {"line": 24, "character": 5}, "end": {"line": 24, "character": 5}},
@ -57,7 +149,38 @@
     [{"range":
       {"start": {"line": 24, "character": 0},
        "end": {"line": 24, "character": 15}},
-       "newText": "termination_by n"}]}]}}]
+       "newText": "termination_by n"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+    "range":
+    {"start": {"line": 24, "character": 5},
+     "end": {"line": 24, "character": 5}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: termination_by n:
+{"title": "Try this: termination_by n",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 24, "character": 0},
+       "end": {"line": 24, "character": 15}},
+      "newText": "termination_by n"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+   "range":
+   {"start": {"line": 24, "character": 5}, "end": {"line": 24, "character": 5}},
+   "context": {"diagnostics": []}}}}
 {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
 "range":
 {"start": {"line": 31, "character": 5}, "end": {"line": 31, "character": 5}},
@ -72,4 +195,35 @@
     [{"range":
       {"start": {"line": 31, "character": 0},
        "end": {"line": 31, "character": 15}},
-       "newText": "termination_by x1 => x1"}]}]}}]
+       "newText": "termination_by x1 => x1"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+    "range":
+    {"start": {"line": 31, "character": 5},
+     "end": {"line": 31, "character": 5}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: termination_by x1 => x1:
+{"title": "Try this: termination_by x1 => x1",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument":
+    {"version": 1, "uri": "file:///terminationBySuggestion.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 31, "character": 0},
+       "end": {"line": 31, "character": 15}},
+      "newText": "termination_by x1 => x1"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///terminationBySuggestion.lean"},
+   "range":
+   {"start": {"line": 31, "character": 5}, "end": {"line": 31, "character": 5}},
+   "context": {"diagnostics": []}}}}
--- a/tests/lean/interactive/tryThisCodeAction.lean.expected.out
+++ b/tests/lean/interactive/tryThisCodeAction.lean.expected.out
@ -11,4 +11,34 @@
     [{"range":
       {"start": {"line": 0, "character": 21},
        "end": {"line": 0, "character": 26}},
-       "newText": "simp only"}]}]}}]
+       "newText": "simp only"}]}]},
+  "data":
+  {"providerResultIndex": 0,
+   "providerName":
+   "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+   "params":
+   {"textDocument": {"uri": "file:///tryThisCodeAction.lean"},
+    "range":
+    {"start": {"line": 0, "character": 22},
+     "end": {"line": 0, "character": 22}},
+    "context": {"diagnostics": []}}}}]
+Resolution of Try this: simp only:
+{"title": "Try this: simp only",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///tryThisCodeAction.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 0, "character": 21},
+       "end": {"line": 0, "character": 26}},
+      "newText": "simp only"}]}]},
+ "data":
+ {"providerResultIndex": 0,
+  "providerName":
+  "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider",
+  "params":
+  {"textDocument": {"uri": "file:///tryThisCodeAction.lean"},
+   "range":
+   {"start": {"line": 0, "character": 22}, "end": {"line": 0, "character": 22}},
+   "context": {"diagnostics": []}}}}