fix: mainModuleName should use srcSearchPath

leanprover · May 5, 2024 · 2717292 · 2717292
1 parent e362b50
commit 2717292
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 9 deletions.
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
@@ -154,7 +154,7 @@ def runFrontend
 
     return (s.commandState.env, !s.commandState.messages.hasErrors)
 
-  let ctx := { inputCtx with mainModuleName, opts, trustLevel }
+  let ctx := { inputCtx with mainModuleName := .pure mainModuleName, opts, trustLevel }
   let processor := Language.Lean.process
   let snap ← processor none ctx
   let snaps := Language.toSnapshotTree snap

diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean
@@ -248,7 +248,7 @@ def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot :=
 /-- Metadata that does not change during the lifetime of the language processing process. -/
 structure ModuleProcessingContext where
   /-- Module name of the file being processed. -/
-  mainModuleName : Name
+  mainModuleName : Task Name
   /-- Options provided outside of the file content, e.g. on the cmdline or in the lakefile. -/
   opts : Options
   /-- Kernel trust level. -/

diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
@@ -366,7 +366,7 @@ where
       if msgLog.hasErrors then
         return { diagnostics, result? := none }
 
-      let headerEnv := headerEnv.setMainModule ctx.mainModuleName
+      let headerEnv := headerEnv.setMainModule ctx.mainModuleName.get
       let cmdState := Elab.Command.mkState headerEnv msgLog opts
       let cmdState := { cmdState with infoState := {
         enabled := true

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
@@ -313,18 +313,22 @@ section Initialization
   def initializeWorker (meta : DocumentMeta) (o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
       : IO (WorkerContext × WorkerState) := do
     let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-    let mut mainModuleName := Name.anonymous
-    try
-      if let some path := System.Uri.fileUriToPath? meta.uri then
-        mainModuleName ← moduleNameOfFileName path none
-    catch _ => pure ()
     let maxDocVersionRef ← IO.mkRef 0
-    let freshRequestIdRef ← IO.mkRef 0
+    let freshRequestIdRef ← IO.mkRef (0 : Int)
     let chanIsProcessing ← IO.Channel.new
     let stickyDiagnosticsRef ← IO.mkRef ∅
     let chanOut ← mkLspOutputChannel maxDocVersionRef chanIsProcessing
     let srcSearchPathPromise ← IO.Promise.new
 
+    let mainModuleName ← if let some path := System.Uri.fileUriToPath? meta.uri then
+      BaseIO.mapTask (t := srcSearchPathPromise.result) fun srcSearchPath =>
+        EIO.catchExceptions (h := fun _ => pure Name.anonymous) do
+          if let some mod ← searchModuleNameOfFileName path srcSearchPath then
+            pure mod
+          else
+            moduleNameOfFileName path none
+    else
+      pure (.pure Name.anonymous)
     let processor := Language.Lean.process (setupImports meta chanOut srcSearchPathPromise)
     let processor ← Language.mkIncrementalProcessor processor { opts, mainModuleName }
     let initSnap ← processor meta.mkInputContext