feat: per-package server options

nix/lake-dev.in

@@ -10,7 +10,7 @@ function pebkac() {
 [[ $# -gt 0 ]] || pebkac
 case $1 in
     --version)
-        # minimum version for `lake server` with fallback
+        # minimum version for `lake serve` with fallback
         echo 3.1.0
         ;;
     print-paths)

src/Lean/Data/KVMap.lean

@@ -190,6 +190,16 @@ def subsetAux : List (Name × DataValue) → KVMap → Bool
 def subset : KVMap → KVMap → Bool
   | ⟨m₁⟩, m₂ => subsetAux m₁ m₂
 
+def mergeBy (mergeFn : Name → DataValue → DataValue → DataValue) (l r : KVMap)
+    : KVMap := Id.run do
+  let mut result := l
+  for ⟨k, vᵣ⟩ in r do
+    if let some vₗ := result.find k then
+      result := result.insert k (mergeFn k vₗ vᵣ)
+    else
+      result := result.insert k vᵣ
+  return result
+
 def eqv (m₁ m₂ : KVMap) : Bool :=
   subset m₁ m₂ && subset m₂ m₁
 

src/Lean/Server/FileWorker.lean

@@ -11,7 +11,7 @@ import Lean.Environment
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
 
-import Lean.Util.Paths
+import Lean.Util.FileSetupInfo
 import Lean.LoadDynlib
 
 import Lean.Server.Utils
@@ -22,6 +22,7 @@ import Lean.Server.References
 import Lean.Server.FileWorker.Utils
 import Lean.Server.FileWorker.RequestHandling
 import Lean.Server.FileWorker.WidgetRequests
+import Lean.Server.FileWorker.SetupFile
 import Lean.Server.Rpc.Basic
 import Lean.Widget.InteractiveDiagnostic
 import Lean.Server.ImportCompletion
@@ -163,84 +164,16 @@ abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO
 
 /- Worker initialization sequence. -/
 section Initialization
-
-  structure LakePrintPathsResult where
-    spawnArgs : Process.SpawnArgs
-    exitCode  : UInt32
-    stdout    : String
-    stderr    : String
-
-  partial def runLakePrintPaths (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO LakePrintPathsResult := do
-    let mut args := #["print-paths"] ++ imports.map (toString ·.module)
-    if m.dependencyBuildMode matches .never then
-      args := args.push "--no-build"
-    let spawnArgs : Process.SpawnArgs := {
-      stdin  := Process.Stdio.null
-      stdout := Process.Stdio.piped
-      stderr := Process.Stdio.piped
-      cmd    := lakePath.toString
-      args
-    }
-    let lakeProc ← Process.spawn spawnArgs
-    -- progress notification: reports latest stderr line
-    let rec processStderr (acc : String) : IO String := do
-      let line ← lakeProc.stderr.getLine
-      if line == "" then
-        return acc
-      else
-        publishDiagnostics m #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.information, message := line }] hOut
-        processStderr (acc ++ line)
-    let stderr ← IO.asTask (processStderr "") Task.Priority.dedicated
-    let stdout := String.trim (← lakeProc.stdout.readToEnd)
-    let stderr ← IO.ofExcept stderr.get
-    let exitCode ← lakeProc.wait
-    return ⟨spawnArgs, exitCode, stdout, stderr⟩
-
-  /-- Uses `lake print-paths` to compile dependencies on the fly and adds them to `LEAN_PATH`.
-  Compilation progress is reported to `hOut` via LSP notifications. Returns the search path for
-  source files. -/
-  partial def lakeSetupSearchPath (lakePath : System.FilePath) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do
-    let result ← runLakePrintPaths lakePath m imports hOut
-    let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList)
-    match result.exitCode with
-    | 0 =>
-      let Except.ok (paths : LeanPaths) ← pure (Json.parse result.stdout >>= fromJson?)
-        | throwServerError s!"invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}"
-      initSearchPath (← getBuildDir) paths.oleanPath
-      paths.loadDynlibPaths.forM loadDynlib
-      paths.srcPath.mapM realPathNormalized
-    | 2 => pure []  -- no lakefile.lean
-    -- error from `--no-build`
-    | 3 => throwServerError s!"Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor.\n\n{result.stdout}"
-    | _ => throwServerError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"
-
-  def setupSrcSearchPath (m : DocumentMeta) (hOut : FS.Stream) (headerStx : Syntax) : IO SearchPath := do
-    let some path := System.Uri.fileUriToPath? m.uri
-      | return ← initSrcSearchPath
-
-    -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps
-    -- NOTE: lake does not exist in stage 0 (yet?)
-    if path.fileName == "lakefile.lean" then
-      return ← initSrcSearchPath
-
-    let lakePath ← determineLakePath
-    if !(← System.FilePath.pathExists lakePath) then
-      return ← initSrcSearchPath
-
-    let imports := Lean.Elab.headerToImports headerStx
-    let pkgSearchPath ← lakeSetupSearchPath lakePath m imports hOut
-    return ← initSrcSearchPath pkgSearchPath
-
-  def buildHeaderEnv (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (headerStx : Syntax) : IO (Environment × MessageLog × SearchPath) := do
-    let (headerEnv, msgLog, srcSearchPath) ←
-      match ← EIO.toIO' <| setupSrcSearchPath m hOut headerStx with
-      | .ok srcSearchPath =>
+  def buildHeaderEnv (m : DocumentMeta) (headerStx : Syntax) (fileSetupResult : FileSetupResult) : IO (Environment × MessageLog) := do
+    let (headerEnv, msgLog) ←
+      match fileSetupResult.kind with
+      | .success | .noLakefile =>
         -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
-        let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true) headerStx opts MessageLog.empty m.mkInputContext
-        pure (headerEnv, msgLog, srcSearchPath)
-      | .error e =>
-        let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
-        pure (← mkEmptyEnvironment, msgs, ← initSrcSearchPath)
+        Elab.processHeader (leakEnv := true) headerStx fileSetupResult.fileOptions MessageLog.empty m.mkInputContext
+      | .importsOutOfDate =>
+        mkErrorEnvironment "Imports are out of date and must be rebuilt; use the \"Restart File\" command in your editor."
+      | .error msg =>
+        mkErrorEnvironment msg
 
     let mut headerEnv := headerEnv
     try
@@ -249,7 +182,12 @@ section Initialization
     catch _ =>
       pure ()
 
-    return (headerEnv, msgLog, srcSearchPath)
+    return (headerEnv, msgLog)
+
+  where
+    mkErrorEnvironment (errorMsg : String) : IO (Environment × MessageLog) := do
+      let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := errorMsg }
+      return (← mkEmptyEnvironment, msgs)
 
   def buildCommandState
       (m : DocumentMeta)
@@ -276,24 +214,33 @@ section Initialization
     }
     { Elab.Command.mkState headerEnv headerMsgLog opts with infoState := headerInfoState }
 
-  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
+  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (globalOptions : Options) (hasWidgets : Bool)
       : IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
     -- parsing should not take long, do synchronously
     let (headerStx, headerParserState, parseMsgLog) ← Parser.parseHeader m.mkInputContext
     (headerStx, ·) <$> EIO.asTask do
-      let (headerEnv, envMsgLog, srcSearchPath) ← buildHeaderEnv m hOut opts headerStx
+      let imports := Lean.Elab.headerToImports headerStx
+      let fileSetupResult ← setupFile m imports fun stderrLine =>
+        let progressDiagnostic := {
+          range     := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩
+          severity? := DiagnosticSeverity.information
+          message   := stderrLine
+        }
+        publishDiagnostics m #[progressDiagnostic] hOut
+      let fileSetupResult := fileSetupResult.addGlobalOptions globalOptions
+      let (headerEnv, envMsgLog) ← buildHeaderEnv m headerStx fileSetupResult
       let headerMsgLog := parseMsgLog.append envMsgLog
-      let cmdState := buildCommandState m headerStx headerEnv headerMsgLog opts
+      let cmdState := buildCommandState m headerStx headerEnv headerMsgLog fileSetupResult.fileOptions
       let headerSnap := {
-        beginPos := 0
-        stx := headerStx
-        mpState := headerParserState
-        cmdState := cmdState
+        beginPos         := 0
+        stx              := headerStx
+        mpState          := headerParserState
+        cmdState         := cmdState
         interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
-        tacticCache := (← IO.mkRef {})
+        tacticCache      := (← IO.mkRef {})
       }
       publishDiagnostics m headerSnap.diagnostics.toArray hOut
-      return (headerSnap, srcSearchPath)
+      return (headerSnap, fileSetupResult.srcSearchPath)
 
   def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
       : IO (WorkerContext × WorkerState) := do

src/Lean/Server/FileWorker/SetupFile.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich, Marc Huisinga
+-/
+import Init.System.IO
+import Lean.Server.Utils
+import Lean.Util.FileSetupInfo
+import Lean.Util.LakePath
+import Lean.LoadDynlib
+
+namespace Lean.Server.FileWorker
+
+open IO
+
+structure LakeSetupFileOutput where
+    spawnArgs : Process.SpawnArgs
+    exitCode  : UInt32
+    stdout    : String
+    stderr    : String
+
+partial def runLakeSetupFile
+    (m                 : DocumentMeta)
+    (lakePath filePath : System.FilePath)
+    (imports           : Array Import)
+    (handleStderr      : String → IO Unit)
+    : IO LakeSetupFileOutput := do
+  let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module)
+  if m.dependencyBuildMode matches .never then
+    args := args.push "--no-build"
+  let spawnArgs : Process.SpawnArgs := {
+    stdin  := Process.Stdio.null
+    stdout := Process.Stdio.piped
+    stderr := Process.Stdio.piped
+    cmd    := lakePath.toString
+    args
+  }
+  let lakeProc ← Process.spawn spawnArgs
+
+  let rec processStderr (acc : String) : IO String := do
+    let line ← lakeProc.stderr.getLine
+    if line == "" then
+      return acc
+    else
+      handleStderr line
+      processStderr (acc ++ line)
+  let stderr ← IO.asTask (processStderr "") Task.Priority.dedicated
+
+  let stdout := String.trim (← lakeProc.stdout.readToEnd)
+  let stderr ← IO.ofExcept stderr.get
+  let exitCode ← lakeProc.wait
+  return ⟨spawnArgs, exitCode, stdout, stderr⟩
+
+inductive FileSetupResultKind where
+  | success
+  | noLakefile
+  | importsOutOfDate
+  | error (msg : String)
+
+structure FileSetupResult where
+  kind          : FileSetupResultKind
+  srcSearchPath : SearchPath
+  fileOptions   : Options
+
+def FileSetupResult.ofSuccess (pkgSearchPath : SearchPath) (fileOptions : Options)
+    : IO FileSetupResult := do return {
+  kind          := FileSetupResultKind.success
+  srcSearchPath := ← initSrcSearchPath pkgSearchPath,
+  fileOptions
+}
+
+def FileSetupResult.ofNoLakefile : IO FileSetupResult := do return {
+  kind          := FileSetupResultKind.noLakefile
+  srcSearchPath := ← initSrcSearchPath
+  fileOptions   := Options.empty
+}
+
+def FileSetupResult.ofImportsOutOfDate : IO FileSetupResult := do return {
+  kind          := FileSetupResultKind.importsOutOfDate
+  srcSearchPath := ← initSrcSearchPath
+  fileOptions   := Options.empty
+}
+
+def FileSetupResult.ofError (msg : String) : IO FileSetupResult := do return {
+  kind          := FileSetupResultKind.error msg
+  srcSearchPath := ← initSrcSearchPath
+  fileOptions   := Options.empty
+}
+
+def FileSetupResult.addGlobalOptions (result : FileSetupResult) (globalOptions : Options)
+    : FileSetupResult :=
+  let fileOptions := globalOptions.mergeBy (fun _ _ fileOpt => fileOpt) result.fileOptions
+  { result with fileOptions := fileOptions }
+
+/-- Uses `lake setup-file` to compile dependencies on the fly and add them to `LEAN_PATH`.
+Compilation progress is reported to `handleStderr`. Returns the search path for
+source files and the options for the file. -/
+partial def setupFile (m : DocumentMeta) (imports : Array Import) (handleStderr : String → IO Unit) : IO FileSetupResult := do
+  let some filePath := System.Uri.fileUriToPath? m.uri
+    | return ← FileSetupResult.ofNoLakefile -- untitled files have no lakefile
+
+  -- NOTE: we assume for now that `lakefile.lean` does not have any non-core-Lean deps
+  -- NOTE: lake does not exist in stage 0 (yet?)
+  if filePath.fileName == "lakefile.lean" then
+    return ← FileSetupResult.ofNoLakefile -- the lakefile itself has no lakefile
+
+  let lakePath ← determineLakePath
+  if !(← System.FilePath.pathExists lakePath) then
+    return ← FileSetupResult.ofNoLakefile
+
+  let result ← runLakeSetupFile m lakePath filePath imports handleStderr
+
+  let cmdStr := " ".intercalate (toString result.spawnArgs.cmd :: result.spawnArgs.args.toList)
+
+  match result.exitCode with
+  | 0 =>
+    let Except.ok (info : FileSetupInfo) := Json.parse result.stdout >>= fromJson?
+      | return ← FileSetupResult.ofError s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}"
+    initSearchPath (← getBuildDir) info.paths.oleanPath
+    info.paths.loadDynlibPaths.forM loadDynlib
+    let pkgSearchPath ← info.paths.srcPath.mapM realPathNormalized
+    FileSetupResult.ofSuccess pkgSearchPath info.setupOptions.toOptions
+  | 2 => -- exit code for lake reporting that there is no lakefile
+    FileSetupResult.ofNoLakefile
+  | 3 => -- exit code for `--no-build`
+    FileSetupResult.ofImportsOutOfDate
+  | _ =>
+    FileSetupResult.ofError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"

src/Lean/Server/ImportCompletion.lean

@@ -97,7 +97,7 @@ def collectAvailableImportsFromLake : IO (Option AvailableImports) := do
   let exitCode ← lakeProc.wait
   match exitCode with
   | 0 =>
-    let Except.ok (availableImports : AvailableImports) ← pure (Json.parse stdout >>= fromJson?)
+    let Except.ok (availableImports : AvailableImports) := Json.parse stdout >>= fromJson?
       | throw <| IO.userError  s!"invalid output from `lake available-imports`:\n{stdout}"
     return availableImports
   | _ =>

src/Lean/Server/README.md

@@ -39,7 +39,7 @@ Another important consideration is the *compacted region* memory used by importe
 
 When the user has two or more files in a single dependency chain open, it is desirable for changes in imports to propagate to modules importing them. That is, when `B.lean` depends on `A.lean` and both are open, changes to `A` should eventually be observable in `B`. But a major problem with Lean 3 is how it does this much too eagerly. Often `B` will be recompiled needlessly as soon as `A` is opened, even if no changes have been made to `A`. For heavyweight modules which take up to several minutes to compile, this causes frustration when `A` is opened merely for inspection e.g. via go-to-definition.
 
-In Lean 4, the situation is different as `.olean` artifacts are required to exist for all imported modules -- one cannot import a `.lean` file without compiling it first. In the running example, when a user opens and edits `A`, nothing is going to happen to `B`. They can continue to interact with it as if `A` kept its previous contents. But when `A` is saved with changes, users can then issue the "refresh file dependencies" command in their editor, which will restart the respective worker and use `lake print-paths` to rebuild and locate its dependencies. This being a conscious action, users will be aware of having to then wait for compilation.
+In Lean 4, the situation is different as `.olean` artifacts are required to exist for all imported modules -- one cannot import a `.lean` file without compiling it first. In the running example, when a user opens and edits `A`, nothing is going to happen to `B`. They can continue to interact with it as if `A` kept its previous contents. But when `A` is saved with changes, users can then issue the "refresh file dependencies" command in their editor, which will restart the respective worker and use `lake setup-file` to rebuild and locate its dependencies. This being a conscious action, users will be aware of having to then wait for compilation.
 
 ### Worker architecture
 

src/Lean/Util.lean

@@ -24,5 +24,5 @@ import Lean.Util.ReplaceLevel
 import Lean.Util.FoldConsts
 import Lean.Util.SCC
 import Lean.Util.OccursCheck
-import Lean.Util.Paths
 import Lean.Util.HasConstCache
+import Lean.Util.FileSetupInfo

src/Lean/Util/FileSetupInfo.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marc Huisinga
+-/
+import Lean.Util.LeanOptions
+
+/--
+Information shared between Lake and Lean when calling `lake setup-file`.
+-/
+structure Lean.FileSetupInfo where
+  paths        : LeanPaths
+  setupOptions : LeanOptions
+  deriving FromJson, ToJson