From 51adfa2e0ca426d2662074bd761946b397aad4af Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 17 Dec 2021 10:49:24 +0100
Subject: [PATCH] fix: do not call `lake print-paths` for `lakefile.lean`

Fixes #873
---
 src/Lean/Server/FileWorker.lean               | 10 +++---
 .../Server/FileWorker/RequestHandling.lean    |  2 +-
 src/Lean/Server/Utils.lean                    | 35 +++++++++++++------
 3 files changed, 31 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index aa8bb94641..869c188ab3 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -173,10 +173,12 @@ section Initialization
     -- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
     let mut srcSearchPath := [srcPath / "lake", srcPath]
     let (headerEnv, msgLog) ← try
-      -- NOTE: lake does not exist in stage 0 (yet?)
-      if (← System.FilePath.pathExists lakePath) then
-        let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
-        srcSearchPath := pkgSearchPath ++ srcSearchPath
+      if let some path := m.uri.toPath? then
+        -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps
+        -- NOTE: lake does not exist in stage 0 (yet?)
+        if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then
+          let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
+          srcSearchPath := pkgSearchPath ++ srcSearchPath
       Elab.processHeader headerStx opts msgLog inputCtx
     catch e =>  -- should be from `lake print-paths`
       let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index b51efe616f..b713c70e70 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -76,7 +76,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
         -- 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
+        pure <| some <| Lsp.DocumentUri.ofPath modFname
       | none         => pure <| some doc.meta.uri
 
     let ranges? ← findDeclarationRanges? n
diff --git a/src/Lean/Server/Utils.lean b/src/Lean/Server/Utils.lean
index 819436976d..cc68564dbe 100644
--- a/src/Lean/Server/Utils.lean
+++ b/src/Lean/Server/Utils.lean
@@ -61,6 +61,30 @@ def withPrefix (a : Stream) (pre : String) : Stream :=
 end FS.Stream
 end IO
 
+namespace Lean.Lsp.DocumentUri
+
+/-- Transform the given path to a file:// URI. -/
+def ofPath (fname : System.FilePath) : DocumentUri :=
+  let fname := fname.normalize.toString
+  let fname := if System.Platform.isWindows then
+    fname.map fun c => if c == '\\' then '/' else c
+  else
+    fname
+  -- TODO(WN): URL-encode special characters
+  -- Three slashes denote localhost.
+  "file:///" ++ fname.dropWhile (· == '/')
+
+/-- Return local path from file:// URI, if any. -/
+def toPath? (uri : DocumentUri) : Option System.FilePath := Id.run do
+  if !uri.startsWith "file:///" then
+    return none
+  let mut p := uri.drop "file://".length
+  if System.Platform.isWindows then
+    p := p.map fun c => if c == '/' then '\\' else c
+  some ⟨p⟩
+
+end Lean.Lsp.DocumentUri
+
 namespace Lean.Server
 
 structure DocumentMeta where
@@ -92,17 +116,6 @@ def maybeTee (fName : String) (isOut : Bool) (h : FS.Stream) : IO FS.Stream := d
     else
       h.chainRight hTee true
 
-/-- Transform the given path to a file:// URI. -/
-def toFileUri (fname : System.FilePath) : Lsp.DocumentUri :=
-  let fname := fname.normalize.toString
-  let fname := if System.Platform.isWindows then
-    fname.map fun c => if c == '\\' then '/' else c
-  else
-    fname
-  -- TODO(WN): URL-encode special characters
-  -- Three slashes denote localhost.
-  "file:///" ++ fname.dropWhile (· == '/')
-
 open Lsp
 
 /-- Returns the document contents with the change applied. -/