From 44f9edff87b0c7935ee699a702eb152419faeaea Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 16 Nov 2021 11:51:44 +0100
Subject: [PATCH] feat: resolve symlinks in LEAN_SRC_PATH

---
 src/Lean/Server/FileWorker/RequestHandling.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 1d04eb5c21..0cd61b7c78 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -69,8 +69,12 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
     let mod? ← findModuleOf? n
     let modUri? ← match mod? with
       | some modName =>
-        let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
-        pure <| modFname?.map toFileUri
+        let some modFname ← rc.srcSearchPath.findWithExt "lean" modName
+          | pure none
+        -- resolve symlinks (such as `src` in the build dir) so that files are opened
+        -- in the right folder
+        let modFname ← IO.FS.realPath modFname
+        pure <| some <| toFileUri modFname
       | none         => pure <| some doc.meta.uri
 
     let ranges? ← findDeclarationRanges? n