From 08ff19d9730bb6dab7353e15ee8a6b1908c2e747 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 1 Aug 2025 11:41:41 -0700
Subject: [PATCH] chore: add code action test back in (#9669)

This PR re-adds the code action test that was reverted in
5b18ea15457255a9db8a3c92fde7d55003f0cff9, now with more robustness.
---
 .../lean/interactive/dottedIdentNotation.lean | 14 +++++++
 .../dottedIdentNotation.lean.expected.out     | 42 +++++++++++++++++++
 2 files changed, 56 insertions(+)

diff --git a/tests/lean/interactive/dottedIdentNotation.lean b/tests/lean/interactive/dottedIdentNotation.lean
index 6603c35e8d..82413425e7 100644
--- a/tests/lean/interactive/dottedIdentNotation.lean
+++ b/tests/lean/interactive/dottedIdentNotation.lean
@@ -66,3 +66,17 @@ example : MyNat → MyNat := .succ
                               --^ textDocument/completion
 open MyLib in
 example : MyNat → MyNat := .succ' -- it successfully elaborates
+
+/-!
+The missing import code action works.
+-/
+--^ waitForILeans
+
+example : IO.FS.Stream := .chainLef
+                           --^ codeAction
+
+example : outParam IO.FS.Stream := .chainLef
+                                   --^ codeAction
+
+example : Nat → IO.FS.Stream := .chainLef
+                                --^ codeAction
diff --git a/tests/lean/interactive/dottedIdentNotation.lean.expected.out b/tests/lean/interactive/dottedIdentNotation.lean.expected.out
index 7e7ff3cb12..15117874a2 100644
--- a/tests/lean/interactive/dottedIdentNotation.lean.expected.out
+++ b/tests/lean/interactive/dottedIdentNotation.lean.expected.out
@@ -85,3 +85,45 @@
     "id": {"const": {"declName": "MyNat.succ"}},
     "cPos": 0}}],
  "isIncomplete": false}
+{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 0, "character": 0},
+       "end": {"line": 0, "character": 0}},
+      "newText": "import Lean.Server.Utils\n"},
+     {"range":
+      {"start": {"line": 74, "character": 27},
+       "end": {"line": 74, "character": 35}},
+      "newText": "chainLeft"}]}]}}
+{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 0, "character": 0},
+       "end": {"line": 0, "character": 0}},
+      "newText": "import Lean.Server.Utils\n"},
+     {"range":
+      {"start": {"line": 77, "character": 36},
+       "end": {"line": 77, "character": 44}},
+      "newText": "chainLeft"}]}]}}
+{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
+ "kind": "quickfix",
+ "edit":
+ {"documentChanges":
+  [{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 0, "character": 0},
+       "end": {"line": 0, "character": 0}},
+      "newText": "import Lean.Server.Utils\n"},
+     {"range":
+      {"start": {"line": 80, "character": 33},
+       "end": {"line": 80, "character": 41}},
+      "newText": "chainLeft"}]}]}}