From a38566693b7e10abaeb3a65b34ea690877cd158a Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Tue, 19 Nov 2024 11:13:51 +0100
Subject: [PATCH] test: fix brittle structure instance completion test (#6127)

#5835 contains a brittle test that uses an FVar ID, which caused a
failure on master. This PR changes that test to use a declaration
instead.
---
 tests/lean/interactive/completionStructureInstance.lean   | 6 ++++--
 .../completionStructureInstance.lean.expected.out         | 8 ++++----
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/tests/lean/interactive/completionStructureInstance.lean b/tests/lean/interactive/completionStructureInstance.lean
index ff79f641c6..a9a084fbf5 100644
--- a/tests/lean/interactive/completionStructureInstance.lean
+++ b/tests/lean/interactive/completionStructureInstance.lean
@@ -92,5 +92,7 @@ example (s : S) : S := { s with   : S } -- All field completions expected
 example (s : S) : S := { s with f  } -- All field completions matching `f` expected
                                --^ textDocument/completion
 
-example (aLongUniqueIdentifier : Nat) : Std.HashSet Nat := { aLongUniqueIdentifier } -- Identifier completion matching `aLongUniqueIdentifier`
-                                                                                --^ textDocument/completion
+def aLongUniqueIdentifier := 0
+
+example : Std.HashSet Nat := { aLongUniqueIdentifier } -- Identifier completion matching `aLongUniqueIdentifier`
+                                                  --^ textDocument/completion
diff --git a/tests/lean/interactive/completionStructureInstance.lean.expected.out b/tests/lean/interactive/completionStructureInstance.lean.expected.out
index aab84e36c0..230c804b64 100644
--- a/tests/lean/interactive/completionStructureInstance.lean.expected.out
+++ b/tests/lean/interactive/completionStructureInstance.lean.expected.out
@@ -598,15 +598,15 @@
     "cPos": 0}}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
- "position": {"line": 94, "character": 82}}
+ "position": {"line": 96, "character": 52}}
 {"items":
  [{"sortText": "0",
    "label": "aLongUniqueIdentifier",
-   "kind": 6,
+   "kind": 21,
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 94, "character": 82}},
-    "id": {"fvar": {"id": "_uniq.1028"}},
+     "position": {"line": 96, "character": 52}},
+    "id": {"const": {"declName": "aLongUniqueIdentifier"}},
     "cPos": 0}}],
  "isIncomplete": true}