From 67aa823ae22ec4b79ce03fd38b94a1fa7d69c485 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Fri, 17 Dec 2021 23:17:42 +0100
Subject: [PATCH] fix: resolve symlinks for the LSP client

---
 src/Lean/Server/References.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index 343f6570ae..5174276c19 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -250,7 +250,9 @@ def referingTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPat
   for (module, refs) in self.allRefs.toList do
     if let some info := refs.find? ident then
       if let some path ← srcSearchPath.findWithExt "lean" module then
-        let uri := DocumentUri.ofPath path
+        -- Resolve symlinks (such as `src` in the build dir) so that files are
+        -- opened in the right folder
+        let uri := DocumentUri.ofPath <| ← IO.FS.realPath path
         if includeDefinition then
           if let some range := info.definition then
             result := result.push ⟨uri, range⟩