feat: lake: use lean --setup (#8447)

This PR makes use of `lean --setup` in Lake builds of Lean modules and
adds Lake support for the new `.olean` artifacts produced by the module
system.

Lake now computes the entire transitive import graph of a module for
Lean, allowing it eagerly provide the artifacts managed by Lake to Lean
via the `modules` field of `lean --setup`.

`lake setup-file` no longer respects the imports passed to it and
instead just parses the file's header for imports. This is necessary
because import statements are now more complex than a simple module
name.

src/Lean/Elab/ParseImportsFast.lean

@@ -189,7 +189,7 @@ partial def moduleIdent : Parser := fun input s =>
   let s := p input s
   match s.error? with
   | none => many p input s
-  | some _ => { pos, error? := none, imports := s.imports.shrink size }
+  | some _ => { s with pos, error? := none, imports := s.imports.shrink size }
 
 def setIsMeta (isMeta : Bool) : Parser := fun _ s =>
   { s with isMeta }
@@ -201,7 +201,7 @@ def setImportAll (importAll : Bool) : Parser := fun _ s =>
   { s with importAll }
 
 def main : Parser :=
-  keywordCore "module" (fun _ s => { s with isModule := true }) (fun _ s => s) >>
+  keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >>
   keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
   many (keywordCore "private" (setIsExported true) (setIsExported false) >>
     keywordCore "meta" (setIsMeta true) (setIsMeta false) >>
@@ -211,24 +211,17 @@ def main : Parser :=
 
 end ParseImports
 
-deriving instance ToJson for Import
-
-structure ParseImportsResult where
-  imports  : Array Import
-  isModule : Bool
-  deriving ToJson
-
 /--
 Simpler and faster version of `parseImports`. We use it to implement Lake.
 -/
-def parseImports' (input : String) (fileName : String) : IO ParseImportsResult := do
+def parseImports' (input : String) (fileName : String) : IO ModuleHeader := do
   let s := ParseImports.main input (ParseImports.whitespace input {})
   match s.error? with
   | none => return { s with }
   | some err => throw <| IO.userError s!"{fileName}: {err}"
 
 structure PrintImportResult where
-  result?  : Option ParseImportsResult := none
+  result?  : Option ModuleHeader := none
   errors   : Array String := #[]
   deriving ToJson
 

src/Lean/Setup.lean

@@ -15,6 +15,7 @@ Data types used by Lean module headers and the `--setup` CLI.
 
 namespace Lean
 
+/- Abstract sturcture of an `import` statement. -/
 structure Import where
   module     : Name
   /-- `import all`; whether to import and expose all data saved by the module. -/
@@ -29,6 +30,14 @@ instance : Coe Name Import := ⟨({module := ·})⟩
 
 instance : ToString Import := ⟨fun imp => toString imp.module⟩
 
+/-- Abstract structure of a module's header. -/
+structure ModuleHeader where
+  /-- The module's direct imports (i.e., those listed in the header). -/
+  imports  : Array Import
+  /-- Whether the module is participating in the module system. -/
+  isModule : Bool
+  deriving Repr, Inhabited, ToJson, FromJson
+
 /-- Files containing data for a single module. -/
 structure ModuleArtifacts where
   lean? : Option System.FilePath := none
@@ -36,6 +45,8 @@ structure ModuleArtifacts where
   oleanServer? : Option System.FilePath := none
   oleanPrivate? : Option System.FilePath := none
   ilean? : Option System.FilePath := none
+  c? : Option System.FilePath := none
+  bc? : Option System.FilePath := none
   deriving Repr, Inhabited, ToJson, FromJson
 
 /--
@@ -47,7 +58,7 @@ structure ModuleSetup where
   name : Name
   /-- Whether the module is participating in the module system. -/
   isModule : Bool := false
-  /- The module's direct imports. -/
+  /-- The module's direct imports. -/
   imports : Array Import := #[]
   /-- Pre-resolved artifacts of related modules (e.g., this module's transitive imports). -/
   modules : NameMap ModuleArtifacts := {}

src/Lean/Util/LeanOptions.lean

@@ -58,6 +58,18 @@ def LeanOptionValue.asCliFlagValue : (v : LeanOptionValue) → String
   | (b : Bool)   => toString b
   | (n : Nat)    => toString n
 
+/-- An option that is used by Lean as if it was passed using `-D`. -/
+structure LeanOption where
+  /-- The option's name. -/
+  name  : Lean.Name
+  /-- The option's value. -/
+  value : Lean.LeanOptionValue
+  deriving Inhabited, Repr
+
+/-- Formats the lean option as a CLI argument using the `-D` flag. -/
+def LeanOption.asCliArg (o : LeanOption) : String :=
+  s!"-D{o.name}={o.value.asCliFlagValue}"
+
 /-- Options that are used by Lean as if they were passed using `-D`. -/
 structure LeanOptions where
   values : NameMap LeanOptionValue
@@ -65,6 +77,21 @@ structure LeanOptions where
 
 instance : EmptyCollection LeanOptions := ⟨⟨∅⟩⟩
 
+def LeanOptions.ofArray (opts : Array LeanOption) : LeanOptions :=
+  ⟨opts.foldl (fun m {name, value} => m.insert name value) {}⟩
+
+/-- Add the options from `new`, overriding those in `self`. -/
+protected def LeanOptions.append (self new : LeanOptions) : LeanOptions :=
+  ⟨self.values.mergeBy (fun _ _ b => b) new.values⟩
+
+instance : Append LeanOptions := ⟨LeanOptions.append⟩
+
+/-- Add the options from `new`, overriding those in `self`. -/
+def LeanOptions.appendArray (self : LeanOptions) (new : Array LeanOption) : LeanOptions :=
+  ⟨new.foldl (fun m {name, value} => m.insert name value) self.values⟩
+
+instance : HAppend LeanOptions (Array LeanOption) LeanOptions := ⟨LeanOptions.appendArray⟩
+
 def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do
   let mut options := KVMap.empty
   for ⟨name, optionValue⟩ in leanOptions.values do

src/lake/Lake/Build.lean

@@ -8,6 +8,5 @@ import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Build.Package
 import Lake.Build.Library
-import Lake.Build.Imports
 import Lake.Build.Targets
 import Lake.Build.Job

src/lake/Lake/Build/Actions.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 prelude
+import Lean.Setup
+import Lean.Data.Json
 import Lake.Config.Dynlib
 import Lake.Util.Proc
 import Lake.Util.NativeLib
@@ -21,29 +23,30 @@ namespace Lake
 
 def compileLeanModule
   (leanFile relLeanFile : FilePath)
-  (oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
-  (leanPath : SearchPath := []) (rootDir : FilePath := ".")
-  (dynlibs plugins : Array Dynlib := #[])
-  (leanArgs : Array String := #[]) (lean : FilePath := "lean")
+  (setup : ModuleSetup) (setupFile : FilePath)
+  (arts : ModuleArtifacts)
+  (leanArgs : Array String := #[])
+  (leanPath : SearchPath := [])
+  (rootDir : FilePath := ".")
+  (lean : FilePath := "lean")
 : LogIO Unit := do
-  let mut args := leanArgs ++
-    #[leanFile.toString, "-R", rootDir.toString]
-  if let some oleanFile := oleanFile? then
+  let mut args :=
+    leanArgs.push leanFile.toString ++ #["-R", rootDir.toString]
+  if let some oleanFile := arts.olean? then
     createParentDirs oleanFile
     args := args ++ #["-o", oleanFile.toString]
-  if let some ileanFile := ileanFile? then
+  if let some ileanFile := arts.ilean? then
     createParentDirs ileanFile
     args := args ++ #["-i", ileanFile.toString]
-  if let some cFile := cFile? then
+  if let some cFile := arts.c? then
     createParentDirs cFile
     args := args ++ #["-c", cFile.toString]
-  if let some bcFile := bcFile? then
+  if let some bcFile := arts.bc? then
     createParentDirs bcFile
     args := args ++ #["-b", bcFile.toString]
-  for dynlib in dynlibs do
-    args := args ++ #["--load-dynlib", dynlib.path.toString]
-  for plugin in plugins do
-    args := args ++ #["--plugin", plugin.path.toString]
+  createParentDirs setupFile
+  IO.FS.writeFile setupFile (toJson setup).pretty
+  args := args ++ #["--setup", setupFile.toString]
   args := args.push "--json"
   withLogErrorPos do
   let out ← rawProc {

src/lake/Lake/Build/Common.lean

@@ -190,7 +190,7 @@ def cacheFileHash (file : FilePath) : IO Unit := do
   createParentDirs hashFile
   IO.FS.writeFile hashFile hash.toString
 
-/-- Remove the cached hash of a file (its `.hash` file). -/
+/-- Remove the cached hash of a file (its `.hash` file) if it exists. -/
 def clearFileHash (file : FilePath) : IO Unit := do
   try
     IO.FS.removeFile <| file.toString ++ ".hash"

src/lake/Lake/Build/Executable.lean

@@ -14,7 +14,7 @@ The build function definition for a Lean executable.
 -/
 
 def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
-  withRegisterJob s!"{self.name}" do
+  withRegisterJob s!"{self.name}:exe" do
   /-
   Remark: We must build the root before we fetch the transitive imports
   so that errors in the import block of transitive imports will not kill this
@@ -25,7 +25,8 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
   let shouldExport := self.supportInterpreter
   for facet in self.root.nativeFacets shouldExport do
     objJobs := objJobs.push <| ← facet.fetch self.root
-  let imports ← (← self.root.transImports.fetch).await
+  let .ok imports _ ← (← self.root.transImports.fetch).wait
+    | error s!"bad imports (see the '{self.root.name.toString}' job for details)"
   for mod in imports do
     for facet in mod.nativeFacets shouldExport do
       objJobs := objJobs.push <| ← facet.fetch mod

src/lake/Lake/Build/Facets.lean

@@ -43,12 +43,25 @@ instance (facet : ModuleFacet α) : FamilyDef FacetOut facet.name α :=
 instance [FamilyOut FacetOut facet α] : CoeDep Name facet (ModuleFacet α) :=
   ⟨facet, FamilyOut.fam_eq⟩
 
+/-- The module's (Lean) source file. -/
+builtin_facet src : Module => FilePath
+
+/-- The parsed module header of the module's source file. -/
+builtin_facet header : Module => ModuleHeader
+
 /--
 The facet which builds all of a module's dependencies
 (i.e., transitive local imports and `--load-dynlib` shared libraries).
 Returns the list of shared libraries to load along with their search path.
 -/
-builtin_facet deps : Module => ModuleDeps
+builtin_facet setup : Module => ModuleSetup
+
+/--
+The facet which builds all of a module's dependencies
+(i.e., transitive local imports and `--load-dynlib` shared libraries).
+Returns the list of shared libraries to load along with their search path.
+-/
+builtin_facet deps : Module => Opaque
 
 /--
 The core build facet of a Lean file.
@@ -56,11 +69,17 @@ Elaborates the Lean file via `lean` and produces all the Lean artifacts
 of the module (i.e., `olean`, `ilean`, `c`).
 Its trace just includes its dependencies.
 -/
-builtin_facet leanArts : Module => Unit
+builtin_facet leanArts : Module => ModuleArtifacts
 
 /-- The `olean` file produced by `lean`. -/
 builtin_facet olean : Module => FilePath
 
+/-- The `olean.server` file produced by `lean` (with the module system enabled). -/
+builtin_facet oleanServerFacet @ olean.server : Module => FilePath
+
+/-- The `olean.private` file produced by `lean` (with the module system enabled). -/
+builtin_facet oleanPrivateFacet @ olean.private : Module => FilePath
+
 /-- The `ilean` file produced by `lean`. -/
 builtin_facet ilean : Module => FilePath
 

src/lake/Lake/Build/Imports.lean

@@ -1,44 +0,0 @@
-/-
-Copyright (c) 2022 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-prelude
-import Lake.Build.Module
-
-/-!
-Definitions to support `lake setup-file` builds.
--/
-
-open System
-namespace Lake
-
-/--
-Builds an `Array` of module imports for a Lean file.
-Used by `lake setup-file` to build modules for the Lean server and
-by `lake lean` to build the imports of a file.
-Returns the dynlibs and plugins built (so they can be loaded by Lean).
--/
-def buildImportsAndDeps
-  (leanFile : FilePath) (imports : Array Module)
-: FetchM (Job ModuleDeps) := do
-  withRegisterJob s!"setup ({leanFile})" do
-  let root ← getRootPackage
-  if imports.isEmpty then
-    -- build the package's (and its dependencies') `extraDepTarget`
-    root.extraDep.fetch <&> (·.map fun _ => {})
-  else
-    -- build local imports from list
-    let modJob := Job.mixArray <| ← imports.mapM (·.olean.fetch)
-    let precompileImports ← (← computePrecompileImportsAux leanFile imports).await
-    let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
-    let externLibsJob ← fetchExternLibs pkgs
-    let impLibsJob ← fetchImportLibs precompileImports
-    let dynlibsJob ← root.dynlibs.fetchIn root
-    let pluginsJob ← root.plugins.fetchIn root
-    modJob.bindM (sync := true) fun _ =>
-    impLibsJob.bindM (sync := true) fun impLibs =>
-    dynlibsJob.bindM (sync := true) fun dynlibs =>
-    pluginsJob.bindM (sync := true) fun plugins =>
-    externLibsJob.mapM fun externLibs => do
-      computeModuleDeps impLibs externLibs dynlibs plugins

src/lake/Lake/Build/Info.lean

@@ -17,8 +17,9 @@ Build info is what is the data passed to a Lake build function to facilitate
 the build.
 -/
 
+open Lean
+
 namespace Lake
-open Lean (Name)
 
 /-- The type of Lake's build info. -/
 inductive BuildInfo
@@ -160,6 +161,64 @@ and target facets.
 
 /-! #### Module Infos -/
 
+structure ModuleImports where
+  transSet : NameSet := {}
+  localImports : Array Module := #[]
+  transImports : Array Module := #[]
+  publicSet : NameSet := {}
+  publicImports : Array Module := #[]
+  libName? : Option Name := none
+  libSet : NameSet :=
+    match libName? with
+    | some libName => .insert {} libName
+    | none => {}
+  libs : Array LeanLib := #[]
+
+private def ModuleImports.addLibCore (self : ModuleImports) (lib : LeanLib) : ModuleImports :=
+  if self.libSet.contains lib.name then
+    self
+  else
+    {self with
+      libSet := self.libSet.insert lib.name
+      libs := self.libs.push lib
+    }
+
+private def ModuleImports.addPublicImportCore (self : ModuleImports) (mod : Module) : ModuleImports :=
+  if self.publicSet.contains mod.name then
+    self
+  else
+    {self with
+      publicSet := self.publicSet.insert mod.name
+      publicImports := self.publicImports.push mod
+    }
+
+private def ModuleImports.addImportCore
+  (self : ModuleImports) (mod : Module)
+: ModuleImports := Id.run do
+  let mut self := self
+  if self.transSet.contains mod.name then
+    return self
+  self := {self with
+    transSet := self.transSet.insert mod.name
+    transImports := self.transImports.push mod
+  }
+  if self.libName? = mod.lib.name then
+    self := {self with localImports := self.localImports.push mod}
+  else
+    self := self.addLibCore mod.lib
+  return self
+
+def ModuleImports.insert
+  (self : ModuleImports) (mod : Module) (isPublic : Bool)
+: ModuleImports :=
+  let self := inline <| self.addImportCore mod
+  if isPublic then inline <| self.addPublicImportCore mod else self
+
+def ModuleImports.append (self other : ModuleImports) : ModuleImports :=
+  let self := other.publicImports.foldl addPublicImportCore self
+  let self := other.transImports.foldl addImportCore self
+  self
+
 /--
 Build info for applying the specified facet to the module.
 It is the user's obiligation to ensure the facet in question is a module facet.
@@ -175,8 +234,17 @@ abbrev Module.facet (facet : Name) (self : Module) : BuildInfo :=
 abbrev BuildInfo.moduleFacet (module : Module) (facet : Name) : BuildInfo :=
   module.facetCore facet
 
+/-- The computed imports of a Lean module. -/
+builtin_facet allImports : Module => ModuleImports
+
 namespace Module
 
+@[inherit_doc srcFacet] abbrev src (self : Module) :=
+  self.facetCore srcFacet
+
+@[inherit_doc headerFacet] abbrev header (self : Module) :=
+  self.facetCore headerFacet
+
 @[inherit_doc importsFacet] abbrev imports (self : Module) :=
   self.facetCore importsFacet
 
@@ -186,15 +254,27 @@ namespace Module
 @[inherit_doc precompileImportsFacet] abbrev precompileImports (self : Module) :=
   self.facetCore precompileImportsFacet
 
+@[inherit_doc allImportsFacet] abbrev allImports (self : Module) :=
+  self.facetCore allImportsFacet
+
+@[inherit_doc setupFacet] abbrev setup  (self : Module) :=
+  self.facetCore setupFacet
+
 @[inherit_doc depsFacet] abbrev deps  (self : Module) :=
   self.facetCore depsFacet
 
-@[inherit_doc leanArtsFacet] abbrev leanArts  (self : Module) :=
+@[inherit_doc leanArtsFacet] abbrev leanArts (self : Module) :=
   self.facetCore leanArtsFacet
 
 @[inherit_doc oleanFacet] abbrev olean (self : Module) :=
   self.facetCore oleanFacet
 
+@[inherit_doc oleanServerFacet] abbrev oleanServer (self : Module) :=
+  self.facetCore oleanServerFacet
+
+@[inherit_doc oleanPrivateFacet] abbrev oleanPrivate (self : Module) :=
+  self.facetCore oleanPrivateFacet
+
 @[inherit_doc ileanFacet] abbrev ilean (self : Module)  :=
   self.facetCore ileanFacet
 

src/lake/Lake/Build/Job/Monad.lean

@@ -6,7 +6,7 @@ Authors: Mac Malone
 prelude
 import Lake.Build.Fetch
 
-open System
+open System Lean
 
 /-! # Job Monad
 
@@ -237,6 +237,10 @@ def collectList (jobs : List (Job α)) (traceCaption := "<collection>") : Job (L
 def collectArray (jobs : Array (Job α)) (traceCaption := "<collection>") : Job (Array α) :=
   jobs.foldl (zipWith Array.push) (traceRoot (Array.mkEmpty jobs.size) traceCaption)
 
+/-- Merge a `NameMap` of jobs into one, collecting their outputs into an `NameMap`. -/
+def collectNameMap (jobs : NameMap (Job α)) (traceCaption := "<collection>") : Job (NameMap α) :=
+  jobs.fold (fun s k v => s.zipWith (·.insert k) v) (traceRoot {} traceCaption)
+
 end Job
 
 /-! ## BuildJob (deprecated) -/

src/lake/Lake/Build/Module.lean

@@ -29,82 +29,86 @@ def recBuildExternDynlibs (pkgs : Array Package)
     jobs := jobs.append <| ← pkg.externLibs.mapM (·.dynlib.fetch)
   return (jobs, libDirs)
 
-/--
-Recursively parse the Lean files of a module and its imports
-building an `Array` product of its direct local imports.
--/
-def Module.recParseImports (mod : Module) : FetchM (Job (Array Module)) := Job.async do
-  let contents ← IO.FS.readFile mod.leanFile
-  let res ← Lean.parseImports' contents mod.leanFile.toString
-  let mods ← res.imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
-    findModule? imp.module <&> fun | some mod => set.insert mod | none => set
-  return mods.toArray
+/-- The `ModuleFacetConfig` for the builtin `srcFacet`. -/
+def Module.srcFacetConfig : ModuleFacetConfig srcFacet :=
+  mkFacetJobConfig fun mod => inputFile mod.leanFile (text := true)
+
+/-- Parse the header of a Lean file from its source. -/
+def Module.recParseHeader (mod : Module) : FetchM (Job ModuleHeader) := do
+  (← mod.src.fetch).mapM fun srcFile => do
+    setTraceCaption s!"{mod.name}:header"
+    let contents ← IO.FS.readFile srcFile
+    Lean.parseImports' contents srcFile.toString
+
+/-- The `ModuleFacetConfig` for the builtin `headerFacet`. -/
+def Module.headerFacetConfig : ModuleFacetConfig headerFacet :=
+  mkFacetJobConfig recParseHeader (buildable := false)
+
+/-- Compute an `Array` of a module's direct local imports from its header. -/
+def Module.recParseImports (mod : Module) : FetchM (Job (Array Module)) := do
+  (← mod.header.fetch).mapM (sync := true) fun header => do
+    let mods ← header.imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
+      findModule? imp.module <&> fun | some mod => set.insert mod | none => set
+    return mods.toArray
 
 /-- The `ModuleFacetConfig` for the builtin `importsFacet`. -/
 def Module.importsFacetConfig : ModuleFacetConfig importsFacet :=
   mkFacetJobConfig recParseImports (buildable := false)
 
-structure ModuleImportData where
-  module : Module
-  transImports : Job (Array Module)
-  includeSelf : Bool
+private def computeAllImportsAux
+  (leanFile : FilePath) (libName? : Option Name) (imports : Array Import)
+: FetchM (Job ModuleImports) := do
+  let task : JobTask ModuleImports := .pure (.ok {libName? := libName?} {})
+  let task ← imports.foldlM (init := task) fun task imp => do
+    let some mod ← findModule? imp.module
+      | return task
+    let impsJob ← mod.allImports.fetch
+    let task :=
+      task.bind (sync := true) fun r =>
+      impsJob.task.map (sync := true) fun
+      | .ok transImps _ =>
+        match r with
+        | .ok imps s => Id.run do
+          let imps := imps.append transImps
+          let imps := imps.insert mod imp.isExported
+          return .ok imps s
+        | .error e s => .error e s
+      | .error _ _ =>
+        let entry := LogEntry.error s!"{leanFile}: bad import '{mod.name}'"
+        match r with
+        | .ok _ s => .error 0 (s.logEntry entry)
+        | .error e s => .error e (s.logEntry entry)
+    return task
+  return Job.ofTask task
 
-@[inline] def collectImportsAux
-  (leanFile : FilePath) (imports : Array Module)
-  (f : Module → FetchM (Bool × Job (Array Module)))
-: FetchM (Job (Array Module)) := do
-  let imps ← imports.mapM fun imp => do
-    let (includeSelf, transImports) ← f imp
-    return {module := imp, transImports, includeSelf : ModuleImportData}
-  let task : JobTask OrdModuleSet := imps.foldl (init := .pure (.ok .empty {})) fun r imp =>
-    r.bind (sync := true) fun r =>
-    imp.transImports.task.map (sync := true) fun
-    | .ok transImps _ =>
-      match r with
-      | .ok impSet s =>
-        let impSet := impSet.appendArray transImps
-        let impSet := if imp.includeSelf then impSet.insert imp.module else impSet
-        .ok impSet s
-      | .error e s => .error e s
-    | .error _ _ =>
-      let entry := LogEntry.error s!"{leanFile}: bad import '{imp.module.name}'"
-      match r with
-      | .ok _ s => .error 0 (s.logEntry entry)
-      | .error e s => .error e (s.logEntry entry)
-  return Job.ofTask <| task.map (sync := true) fun
-    | .ok impSet s => .ok impSet.toArray s
-    | .error e s => .error e s
+def Module.recComputeAllImports (self : Module) : FetchM (Job ModuleImports) := do
+  (← self.header.fetch).bindM fun header =>
+    computeAllImportsAux self.relLeanFile self.lib.name header.imports
+
+/-- The `ModuleFacetConfig` for the builtin `allImportsFacet`. -/
+def Module.allImportsFacetConfig : ModuleFacetConfig allImportsFacet :=
+  mkFacetJobConfig recComputeAllImports (buildable := false)
 
 /-- Recursively compute a module's transitive imports. -/
 def Module.recComputeTransImports (mod : Module) : FetchM (Job (Array Module)) := ensureJob do
-  collectImportsAux mod.leanFile (← (← mod.imports.fetch).await) fun imp =>
-    (true, ·) <$> imp.transImports.fetch
+  return (← mod.allImports.fetch).map (sync := true) (·.transImports)
 
 /-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/
 def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet :=
   mkFacetJobConfig recComputeTransImports (buildable := false)
 
-def computePrecompileImportsAux
-  (leanFile : FilePath) (imports : Array Module)
-: FetchM (Job (Array Module)) := do
-  collectImportsAux leanFile imports fun imp =>
-    if imp.shouldPrecompile then
-      (true, ·) <$> imp.transImports.fetch
-    else
-      (false, ·) <$> imp.precompileImports.fetch
-
 /-- Recursively compute a module's precompiled imports. -/
 def Module.recComputePrecompileImports (mod : Module) : FetchM (Job (Array Module)) := ensureJob do
-  inline <| computePrecompileImportsAux mod.leanFile (← (← mod.imports.fetch).await)
+  return (← mod.allImports.fetch).map (sync := true) fun imps =>
+    if mod.shouldPrecompile then
+      imps.transImports
+    else
+      imps.transImports.filter (·.shouldPrecompile)
 
 /-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/
 def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet :=
   mkFacetJobConfig recComputePrecompileImports (buildable := false)
 
-/-- Fetch dynlibs of the packages' external libraries. **For internal use.** -/
-def fetchExternLibs (pkgs : Array Package) : FetchM (Job (Array Dynlib)) :=
-  Job.collectArray <$> pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch))
-
 /--
 Computes the transitive dynamic libraries of a module's imports.
 Modules from the same library are loaded individually, while modules
@@ -126,25 +130,6 @@ private def Module.fetchImportLibs
       return (libs, jobs)
   return jobs
 
-/--
-**For internal use.**
-
-Fetches the library dynlibs of a list of non-local imports.
-Modules are loaded as part of their whole library.
--/
-def fetchImportLibs
-  (mods : Array Module) : FetchM (Job (Array Dynlib))
-:= do
-  let (_, jobs) ← mods.foldlM (init := (({} : NameSet), #[])) fun (libs, jobs) imp => do
-    if libs.contains imp.lib.name then
-      return (libs, jobs)
-    else if imp.shouldPrecompile then
-      let jobs ← jobs.push <$> imp.lib.shared.fetch
-      return (libs.insert imp.lib.name, jobs)
-    else
-      return (libs, jobs)
-  return Job.collectArray jobs "import dynlibs"
-
 /--
 Topologically sorts the library dependency tree by name.
 Libraries come *after* their dependencies.
@@ -168,7 +153,7 @@ where
     let o := o.push lib
     return (v, o)
 
-def computeModuleDeps
+private def computeModuleDeps
   (impLibs : Array Dynlib) (externLibs : Array Dynlib)
   (dynlibs : Array Dynlib) (plugins : Array Dynlib)
 : FetchM ModuleDeps := do
@@ -197,42 +182,83 @@ def computeModuleDeps
     plugins := plugins.push (← getLakeInstall).sharedDynlib
   return {dynlibs, plugins}
 
+private def Module.fetchOLeanArts
+  (mod : Module) (importAll : Bool := false)
+: FetchM (Job ModuleArtifacts) := do
+  let eJob ← mod.olean.fetch
+  if importAll then
+    fetchAll eJob
+  else
+    (← mod.header.fetch).bindM fun header => do
+      if header.isModule then
+        fetchAll eJob
+      else
+        newTrace mod.name.toString
+        eJob.mapM (sync := true) fun olean => do
+          return {olean? := olean}
+where
+  fetchAll eJob := do
+    let sJob ← mod.oleanServer.fetch
+    let pJob ← mod.oleanPrivate.fetch
+    eJob.bindM (sync := true) fun oe =>
+    sJob.bindM (sync := true) fun os =>
+    pJob.mapM (sync := true) fun op => do
+      setTraceCaption mod.name.toString
+      return {olean? := oe, oleanServer? := os, oleanPrivate? := op}
+
 /--
 Recursively build a module's dependencies, including:
 * Transitive local imports
 * Shared libraries (e.g., `extern_lib` targets or precompiled modules)
 * `extraDepTargets` of its library
 -/
-def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
+def Module.recFetchSetup (mod : Module) : FetchM (Job ModuleSetup) := ensureJob do
   let extraDepJob ← mod.lib.extraDep.fetch
 
-  /-
-  Remark: We must build direct imports before we fetch the transitive
-  precompiled imports so that errors in the import block of transitive imports
-  will not kill this job before the direct imports are built.
-  -/
-  let directImports ← (← mod.imports.fetch).await
-  let importJobs ← directImports.mapM fun imp => do
-    if imp.name = mod.name then
-      logError s!"{mod.leanFile}: module imports itself"
-    imp.olean.fetch
-  let importJob := Job.mixArray importJobs "import oleans"
-  /-
-  Remark: It should be possible to avoid transitive imports here when the module
-  itself is precompiled, but they are currently kept to preserve the "bad import" errors.
-  -/
-  let precompileImports ← if mod.shouldPrecompile then
-    mod.transImports.fetch else mod.precompileImports.fetch
-  let precompileImports ← precompileImports.await
-  let impLibsJob ← Job.collectArray (traceCaption := "import dynlibs") <$>
-    mod.fetchImportLibs precompileImports mod.shouldPrecompile
+  let headerJob ← mod.header.fetch
+  let impsJob ← mod.allImports.fetch
+  let impArtsJob ←
+    headerJob.bindM fun header => do
+      let artsJobMap : NameMap (Job ModuleArtifacts) := {}
+      /-
+      Remark: Errrors in the transitive import graph will prevent downstream builds.
+      Thus, we fetch the direct import artifacts first so they can still potentially
+      succeed even if the overall graph is erronous.
+      -/
+      let artsJobMap ← header.imports.foldlM (init := artsJobMap) fun s imp => do
+        if s.contains imp.module then
+          return s
+        if mod.name = imp.module then
+          logError s!"{mod.relLeanFile}: module imports itself"
+          return s
+        let some mod ← findModule? imp.module
+          | return s
+        return s.insert mod.name (← mod.fetchOLeanArts imp.importAll)
+      impsJob.bindM fun imps => do
+        let artsJobMap ← imps.publicImports.foldlM (init := artsJobMap) fun s mod =>
+          if s.contains mod.name then
+            return s
+          else
+            return s.insert mod.name (← mod.fetchOLeanArts)
+        return Job.collectNameMap artsJobMap "import artifacts"
+  let impLibsJob ← impsJob.bindM fun imps => do
+    let jobs ←
+      if mod.shouldPrecompile then
+        let jobs := #[]
+        let jobs ← imps.localImports.foldlM (·.push <$> ·.dynlib.fetch) jobs
+        imps.libs.foldlM (·.push <$> ·.shared.fetch) jobs
+      else
+        imps.libs.foldlM (init := #[]) fun jobs lib =>
+          if lib.precompileModules then jobs.push <$> lib.shared.fetch else pure jobs
+    return Job.collectArray jobs "import dynlibs"
   let externLibsJob ← Job.collectArray (traceCaption := "package external libraries") <$>
     if mod.shouldPrecompile then mod.pkg.externLibs.mapM (·.dynlib.fetch) else pure #[]
   let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg "module dynlibs"
   let pluginsJob ← mod.plugins.fetchIn mod.pkg "module plugins"
 
   extraDepJob.bindM (sync := true) fun _ => do
-  importJob.bindM (sync := true) fun _ => do
+  headerJob.bindM (sync := true) fun header => do
+  impArtsJob.bindM (sync := true) fun modules => do
   let depTrace ← takeTrace
   impLibsJob.bindM (sync := true) fun impLibs => do
   externLibsJob.bindM (sync := true) fun externLibs => do
@@ -246,71 +272,125 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
     | none => addTrace depTrace; addTrace libTrace
     | some false => addTrace depTrace; addTrace libTrace; addPlatformTrace
     | some true => addTrace depTrace
-    computeModuleDeps impLibs externLibs dynlibs plugins
+    let {dynlibs, plugins} ← computeModuleDeps impLibs externLibs dynlibs plugins
+    return {
+      name := mod.name
+      isModule := header.isModule
+      imports := header.imports
+      modules := modules
+      dynlibs := dynlibs.map (·.path.toString)
+      plugins := plugins.map (·.path.toString)
+      options := mod.leanOptions
+    }
+
+/-- The `ModuleFacetConfig` for the builtin `setupFacet`. -/
+def Module.setupFacetConfig : ModuleFacetConfig setupFacet :=
+  mkFacetJobConfig recFetchSetup
 
 /-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/
 def Module.depsFacetConfig : ModuleFacetConfig depsFacet :=
-  mkFacetJobConfig recBuildDeps
+  mkFacetJobConfig fun mod => (·.toOpaque) <$> mod.setup.fetch
 
-/-- Remove cached file hashes of the module build outputs (in `.hash` files). -/
+/-- Remove any cached file hashes of the module build outputs (in `.hash` files). -/
 def Module.clearOutputHashes (mod : Module) : IO PUnit := do
   clearFileHash mod.oleanFile
+  clearFileHash mod.oleanServerFile
+  clearFileHash mod.oleanPrivateFile
   clearFileHash mod.ileanFile
   clearFileHash mod.cFile
-  if Lean.Internal.hasLLVMBackend () then
-    clearFileHash mod.bcFile
+  clearFileHash mod.bcFile
 
 /-- Cache the file hashes of the module build outputs in `.hash` files. -/
 def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
   cacheFileHash mod.oleanFile
+  if (← mod.oleanServerFile.pathExists) then
+    cacheFileHash mod.oleanServerFile
+  if (← mod.oleanPrivateFile.pathExists)  then
+    cacheFileHash mod.oleanPrivateFile
   cacheFileHash mod.ileanFile
   cacheFileHash mod.cFile
   if Lean.Internal.hasLLVMBackend () then
     cacheFileHash mod.bcFile
 
+private def traceOptions (opts : LeanOptions) (caption := "opts") : BuildTrace :=
+  opts.values.fold (init := .nil caption) fun t n v =>
+    let opt := s!"-D{n}={v.asCliFlagValue}"
+    t.mix <| .ofHash (pureHash opt) opt
+
 /--
 Recursively build a Lean module.
 Fetch its dependencies and then elaborate the Lean source file, producing
-all possible artifacts (i.e., `.olean`, `ilean`, `.c`, and `.bc`).
+all possible artifacts (e.g., `.olean`, `.ilean`, `.c`, `.bc`).
 -/
-def Module.recBuildLean (mod : Module) : FetchM (Job Unit) := do
+def Module.recBuildLean (mod : Module) : FetchM (Job ModuleArtifacts) := do
   withRegisterJob mod.name.toString do
-  (← mod.deps.fetch).mapM fun {dynlibs, plugins} => do
+  (← mod.src.fetch).bindM fun srcFile => do
+  let srcTrace ← getTrace
+  (← mod.setup.fetch).mapM fun setup => do
     addLeanTrace
+    addTrace <| traceOptions setup.options "options"
     addPureTrace mod.leanArgs "Module.leanArgs"
-    let srcTrace ← computeTrace (TextFilePath.mk mod.leanFile)
-    addTrace srcTrace
     setTraceCaption s!"{mod.name.toString}:leanArts"
+    let arts : ModuleArtifacts := {
+      lean? := srcFile
+      olean? := mod.oleanFile
+      oleanServer? := if setup.isModule then some mod.oleanServerFile else none
+      oleanPrivate? := if setup.isModule then some mod.oleanPrivateFile else none
+      ilean? := mod.ileanFile
+      c? := mod.cFile
+      bc? := if Lean.Internal.hasLLVMBackend () then some mod.bcFile else none
+    }
     let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace.mtime) mod (← getTrace) mod.traceFile do
-      compileLeanModule mod.leanFile mod.relLeanFile mod.oleanFile mod.ileanFile mod.cFile mod.bcFile?
-        (← getLeanPath) mod.rootDir dynlibs plugins
-        (mod.weakLeanArgs ++ mod.leanArgs) (← getLean)
+      let args := mod.weakLeanArgs ++ mod.leanArgs
+      let relSrcFile := relPathFrom mod.pkg.dir srcFile
+      compileLeanModule srcFile relSrcFile setup mod.setupFile arts args
+        (← getLeanPath) mod.rootDir (← getLean)
       mod.clearOutputHashes
     unless upToDate && (← getTrustHash) do
       mod.cacheOutputHashes
+    return arts
 
 /-- The `ModuleFacetConfig` for the builtin `leanArtsFacet`. -/
 def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
   mkFacetJobConfig recBuildLean
 
+@[inline] private def Module.fetchOLeanCore
+  (facet : String) (f : ModuleArtifacts → Option FilePath) (errMsg : String) (mod : Module)
+: FetchM (Job FilePath) := do
+  (← mod.leanArts.fetch).mapM fun arts => do
+      let some oleanFile := f arts
+        | error errMsg
+      /-
+      Avoid recompiling unchanged OLean files.
+      While OLean files transitively include their imports,
+      Lake also traverses this graph itself, so the transtive imports
+      are not included in this trace.
+      -/
+      newTrace s!"{mod.name.toString}:{facet}"
+      addTrace (← fetchFileTrace oleanFile)
+      return oleanFile
+
 /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
 def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
-  mkFacetJobConfig fun mod => do
-    (← mod.leanArts.fetch).mapM fun _ => do
-      /-
-      Avoid recompiling unchanged Olean files.
-      Olean files incorporate not only their own content, but also their
-      transitive imports. However, they are independent of their module sources.
-      -/
-      newTrace s!"{mod.name.toString}:olean"
-      addTrace (← mod.deps.fetch).getTrace.withoutInputs
-      addTrace (← fetchFileTrace mod.oleanFile)
-      return mod.oleanFile
+  mkFacetJobConfig <| fetchOLeanCore "olean" (·.olean?)
+    "No olean generated. This is likely an error in Lean or Lake."
+
+/-- The `ModuleFacetConfig` for the builtin `oleanServerFacet`. -/
+def Module.oleanServerFacetConfig : ModuleFacetConfig oleanServerFacet :=
+  mkFacetJobConfig <| fetchOLeanCore "olean.server" (·.oleanServer?)
+    "No server olean generated. Ensure the module system is enabled."
+
+/-- The `ModuleFacetConfig` for the builtin `oleanPrivateFacet`. -/
+def Module.oleanPrivateFacetConfig : ModuleFacetConfig oleanPrivateFacet :=
+  mkFacetJobConfig <| fetchOLeanCore "olean.private" (·.oleanPrivate?)
+    "No private olean generated. Ensure the module system is enabled."
 
 /-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
 def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
   mkFacetJobConfig fun mod => do
-    (← mod.leanArts.fetch).mapM fun _ => do
+    (← mod.leanArts.fetch).mapM fun arts => do
+      let some ileanFile := arts.ilean?
+        | error "No ilean generated. This is likely an error in Lean or Lake."
       /-
       Avoid recompiling unchanged Ilean files.
       Ilean files are assumed to only incorporate their own content
@@ -318,13 +398,15 @@ def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
       Lean also produces LF-only Ilean files, so no line ending normalization.
       -/
       newTrace s!"{mod.name.toString}:ilean"
-      addTrace (← fetchFileTrace mod.ileanFile)
-      return mod.ileanFile
+      addTrace (← fetchFileTrace ileanFile)
+      return ileanFile
 
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 def Module.cFacetConfig : ModuleFacetConfig cFacet :=
   mkFacetJobConfig fun mod => do
-    (← mod.leanArts.fetch).mapM fun _ => do
+    (← mod.leanArts.fetch).mapM fun arts => do
+      let some cFile := arts.c?
+        | error "No C file generated. This is likely an error in Lean or Lake."
       /-
       Avoid recompiling unchanged C files.
       C files are assumed to incorporate their own content
@@ -333,22 +415,24 @@ def Module.cFacetConfig : ModuleFacetConfig cFacet :=
       Lean also produces LF-only C files, so no line ending normalization.
       -/
       newTrace s!"{mod.name.toString}:c"
-      addTrace (← fetchFileTrace mod.cFile)
+      addTrace (← fetchFileTrace cFile)
       addLeanTrace
-      return mod.cFile
+      return cFile
 
 /-- The `ModuleFacetConfig` for the builtin `bcFacet`. -/
 def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
   mkFacetJobConfig fun mod => do
-    (← mod.leanArts.fetch).mapM fun _ => do
+    (← mod.leanArts.fetch).mapM fun arts => do
+      let some bcFile := arts.bc?
+        | error "No LLVM bitcode generated. Ensure your Lean version supports the LLVM backend."
       /-
       Avoid recompiling unchanged bitcode files.
       Bitcode files are assumed to only depend on their content
       and not transitively on their inputs (e.g., imports).
       -/
       newTrace s!"{mod.name.toString}:bc"
-      addTrace (← fetchFileTrace mod.bcFile)
-      return mod.bcFile
+      addTrace (← fetchFileTrace bcFile)
+      return bcFile
 
 /--
 Recursively build the module's object file from its C file produced by `lean`
@@ -452,12 +536,18 @@ Lake module facets (e.g., `imports`, `c`, `o`, `dynlib`).
 -/
 def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   DNameMap.empty
+  |>.insert srcFacet srcFacetConfig
+  |>.insert headerFacet headerFacetConfig
   |>.insert importsFacet importsFacetConfig
   |>.insert transImportsFacet transImportsFacetConfig
   |>.insert precompileImportsFacet precompileImportsFacetConfig
+  |>.insert allImportsFacet allImportsFacetConfig
+  |>.insert setupFacet setupFacetConfig
   |>.insert depsFacet depsFacetConfig
   |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert oleanFacet oleanFacetConfig
+  |>.insert oleanServerFacet oleanServerFacetConfig
+  |>.insert oleanPrivateFacet oleanPrivateFacetConfig
   |>.insert ileanFacet ileanFacetConfig
   |>.insert cFacet cFacetConfig
   |>.insert bcFacet bcFacetConfig
@@ -472,3 +562,42 @@ def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
 
 @[inherit_doc Module.initFacetConfigs]
 abbrev initModuleFacetConfigs := Module.initFacetConfigs
+
+/-!
+Definitions to support `lake setup-file` builds.
+-/
+
+/--
+Builds an `Array` of module imports for a Lean file.
+Used by `lake setup-file` to build modules for the Lean server and
+by `lake lean` to build the imports of a file.
+Returns the dynlibs and plugins built (so they can be loaded by Lean).
+-/
+def buildImportsAndDeps
+  (leanFile : FilePath) (imports : Array Import)
+: FetchM (Job ModuleDeps) := do
+  withRegisterJob s!"setup ({leanFile})" do
+  let root ← getRootPackage
+  if imports.isEmpty then
+    -- build the package's (and its dependencies') `extraDepTarget`
+    root.extraDep.fetch <&> (·.map fun _ => {})
+  else
+    -- build local imports from list
+    let modJob ← imports.foldlM (init := Job.pure ()) fun job imp => do
+      let some mod ← findModule? imp.module
+        | return job
+      job.mix <$> mod.fetchOLeanArts imp.importAll
+    let impsJob ← computeAllImportsAux leanFile none imports
+    let externLibsJob ← Job.collectArray <$>
+      if root.precompileModules then root.externLibs.mapM (·.dynlib.fetch) else pure #[]
+    let impLibsJob ← impsJob.bindM fun {libs, ..} =>
+      Job.collectArray <$> libs.foldlM (init := #[]) fun jobs lib =>
+        if lib.precompileModules then jobs.push <$> lib.shared.fetch else pure jobs
+    let dynlibsJob ← root.dynlibs.fetchIn root
+    let pluginsJob ← root.plugins.fetchIn root
+    modJob.bindM (sync := true) fun _ =>
+    impLibsJob.bindM (sync := true) fun impLibs =>
+    dynlibsJob.bindM (sync := true) fun dynlibs =>
+    pluginsJob.bindM (sync := true) fun plugins =>
+    externLibsJob.mapM fun externLibs => do
+      computeModuleDeps impLibs externLibs dynlibs plugins

src/lake/Lake/CLI/Main.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Load
-import Lake.Build.Imports
 import Lake.Util.Error
 import Lake.Util.MainM
 import Lake.Util.Cli
@@ -446,8 +445,10 @@ protected def setupFile : CliM PUnit := do
   let loadConfig ← mkLoadConfig opts
   let buildConfig := mkBuildConfig opts
   let filePath ← takeArg "file path"
-  let imports ← takeArgs
-  setupFile loadConfig filePath imports buildConfig
+  -- Additional arguments (imports) are ignored
+  -- TODO: Forbid them once the language server is updated
+  -- noArgsRem do
+  setupFile loadConfig filePath buildConfig
 
 protected def test : CliM PUnit := do
   processOptions lakeOption
@@ -537,34 +538,34 @@ private def evalLeanFile
 : LoggerIO UInt32 := do
   let some path ← resolvePath? leanFile
     | error s!"file not found: {leanFile}"
-  let spawnArgs ← id do
+  let args ← do
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
-      return mkSpawnArgs ws path deps (some mod.rootDir) mod.leanArgs
+      let setup ← ws.runBuild (cfg := buildConfig) do
+        withRegisterJob s!"{mod.name}:setup" do mod.setup.fetch
+      mkArgs path setup (some mod.rootDir) mod.leanArgs
     else
-      let res ← Lean.parseImports' (← IO.FS.readFile path) leanFile.toString
-      let imports := res.imports.filterMap (ws.findModule? ·.module)
-      let deps ← ws.runBuild (buildImportsAndDeps leanFile imports) buildConfig
-      return mkSpawnArgs ws path deps none ws.root.moreLeanArgs
+      let setup ← mkModuleSetup
+        ws leanFile.toString (← IO.FS.readFile path) ws.leanOptions buildConfig
+      mkArgs path setup none ws.root.moreLeanArgs
+  let spawnArgs : IO.Process.SpawnArgs := {
+    args := args ++ moreArgs
+    cmd := ws.lakeEnv.lean.lean.toString
+    env := ws.augmentedEnvVars
+  }
   logVerbose (mkCmdLog spawnArgs)
   let child ← IO.Process.spawn spawnArgs
   child.wait
 where
-  mkSpawnArgs ws leanFile deps rootDir? cfgArgs := Id.run do
+  mkArgs leanFile setup rootDir? cfgArgs := do
     let mut args := cfgArgs.push leanFile.toString
     if let some rootDir := rootDir? then
       args := args ++ #["-R", rootDir.toString]
-    let {dynlibs, plugins} := deps
-    for dynlib in dynlibs do
-      args := args ++ #["--load-dynlib", dynlib.path.toString]
-    for plugin in plugins do
-      args := args ++ #["--plugin", plugin.path.toString]
-    return {
-      args := args ++ moreArgs
-      cmd := ws.lakeEnv.lean.lean.toString
-      env := ws.augmentedEnvVars
-      : IO.Process.SpawnArgs
-    }
+    let (h, setupFile) ← IO.FS.createTempFile
+    let contents := (toJson setup).compress
+    logVerbose s!"module setup: {contents}"
+    h.putStr contents
+    args := args ++ #["--setup", setupFile.toString]
+    return args
 
 protected def lean : CliM PUnit := do
   processOptions lakeOption

src/lake/Lake/CLI/Serve.lean

@@ -23,11 +23,27 @@ and falls back to plain `lean --server`.
 -/
 def invalidConfigEnvVar := "LAKE_INVALID_CONFIG"
 
-private def mkLeanPaths (ws : Workspace) (deps : ModuleDeps) : LeanPaths where
+private def mkLeanPaths (ws : Workspace) (setup : ModuleSetup) : LeanPaths where
   oleanPath := ws.leanPath
   srcPath := ws.leanSrcPath
-  loadDynlibPaths := deps.dynlibs.map (·.path)
-  pluginPaths := deps.plugins.map (·.path)
+  loadDynlibPaths := setup.dynlibs
+  pluginPaths := setup.plugins
+
+def mkModuleSetup
+  (ws : Workspace) (fileName : String) (input : String) (opts : LeanOptions)
+  (buildConfig : BuildConfig)
+: IO ModuleSetup := do
+  let header ← Lean.parseImports' input fileName
+  let {dynlibs, plugins} ← ws.runBuild (buildImportsAndDeps fileName header.imports) buildConfig
+  return {
+    name := ← Lean.moduleNameOfFileName fileName none
+    isModule := header.isModule
+    imports := header.imports
+    modules := {} -- TODO
+    dynlibs := dynlibs.map (·.path.toString)
+    plugins := plugins.map (·.path.toString)
+    options := opts
+  }
 
 /--
 Build a list of imports of a file and print the `.olean` and source directories
@@ -37,8 +53,7 @@ If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).
 The `setup-file` command is used internally by the Lean 4 server.
 -/
 def setupFile
-  (loadConfig : LoadConfig) (path : FilePath) (imports : List String := [])
-  (buildConfig : BuildConfig := {})
+  (loadConfig : LoadConfig) (path : FilePath) (buildConfig : BuildConfig := {})
 : MainM PUnit := do
   let path ← resolvePath path
   let configFile ← realConfigFile loadConfig.configFile
@@ -62,21 +77,19 @@ def setupFile
     let some ws ← loadWorkspace loadConfig |>.toBaseIO buildConfig.outLv buildConfig.ansiMode
       | error "failed to load workspace"
     if let some mod := ws.findModuleBySrc? path then
-      let deps ← ws.runBuild (withRegisterJob s!"setup ({mod.name})" do mod.deps.fetch) buildConfig
-      let opts := mod.serverOptions.foldl (init := {}) fun opts opt =>
-        opts.insert opt.name opt.value
+      let setup ← ws.runBuild (cfg := buildConfig) do
+        withRegisterJob s!"{mod.name}:setup" do mod.setup.fetch
       let info : FileSetupInfo := {
-        paths := mkLeanPaths ws deps
-        setupOptions := ⟨opts⟩
+        paths := mkLeanPaths ws setup
+        setupOptions := mod.serverOptions
       }
       IO.println (toJson info).compress
     else
-      let imports := imports.foldl (init := #[]) fun imps imp =>
-        if let some mod := ws.findModule? imp.toName then imps.push mod else imps
-      let deps ← ws.runBuild (buildImportsAndDeps path imports) buildConfig
+      let setup ← mkModuleSetup
+        ws path.toString (← IO.FS.readFile path) ws.serverOptions buildConfig
       let info : FileSetupInfo := {
-        paths := mkLeanPaths ws deps
-        setupOptions := ⟨∅⟩
+        paths := mkLeanPaths ws setup
+        setupOptions := setup.options
       }
       IO.println (toJson info).compress
 

src/lake/Lake/Config/LeanConfig.lean

@@ -9,7 +9,7 @@ import Lake.Build.Target.Basic
 import Lake.Config.Dynlib
 import Lake.Config.Meta
 
-open System
+open System Lean
 
 namespace Lake
 
@@ -121,18 +121,6 @@ protected def BuildType.toString (bt : BuildType) : String :=
 
 instance : ToString BuildType := ⟨BuildType.toString⟩
 
-/-- An option that is used by Lean as if it was passed using `-D`. -/
-structure LeanOption where
-  /-- The option's name. -/
-  name  : Lean.Name
-  /-- The option's value. -/
-  value : Lean.LeanOptionValue
-  deriving Inhabited, Repr
-
-/-- Formats the lean option as a CLI argument using the `-D` flag. -/
-def LeanOption.asCliArg (o : LeanOption) : String :=
-  s!"-D{o.name}={o.value.asCliFlagValue}"
-
 /-- Configuration options common to targets that build modules. -/
 configuration LeanConfig where
   /--
@@ -251,10 +239,11 @@ deriving Inhabited, Repr
 instance : EmptyCollection LeanConfig := ⟨{}⟩
 
 /-- The options to pass to `lean` based on the build type. -/
-def BuildType.leanOptions : BuildType → Array LeanOption
-| debug => #[{ name := `debugAssertions, value := true }]
-| _ => #[]
+def BuildType.leanOptions : BuildType → LeanOptions
+| debug => ⟨NameMap.empty.insert `debugAssertions true⟩
+| _ => {}
 
+set_option linter.unusedVariables false in
 /-- The arguments to pass to `lean` based on the build type. -/
 def BuildType.leanArgs (t : BuildType) : Array String :=
-  t.leanOptions.map (·.asCliArg)
+  #[]

src/lake/Lake/Config/LeanLib.lean

@@ -120,8 +120,9 @@ The arguments to pass to `lean --server` when running the Lean language server.
 - the library's `leanOptions`
 - the library's `moreServerOptions`
 -/
-@[inline] def serverOptions (self : LeanLib) : Array LeanOption :=
-  self.buildType.leanOptions ++ self.pkg.moreServerOptions ++ self.config.leanOptions ++ self.config.moreServerOptions
+@[inline] def serverOptions (self : LeanLib) : LeanOptions :=
+  ({} : LeanOptions) ++ self.buildType.leanOptions ++ self.pkg.moreServerOptions ++
+  self.config.leanOptions ++ self.config.moreServerOptions
 
 /--
 The backend type for modules of this library.
@@ -148,14 +149,22 @@ The targets of the package plus the targets of the library (in that order).
 /--
 The arguments to pass to `lean` when compiling the library's Lean files.
 `leanArgs` is the accumulation of:
-- the build type's `leanArgs`
+- the build type's `leanOptions`
 - the package's `leanOptions`
-- the package's `moreLeanArgs`
 - the library's `leanOptions`
+-/
+@[inline] def leanOptions (self : LeanLib) : LeanOptions :=
+  self.buildType.leanOptions ++ self.pkg.leanOptions ++ self.config.leanOptions
+
+/--
+The arguments to pass to `lean` when compiling the library's Lean files.
+`leanArgs` is the accumulation of:
+- the build type's `leanArgs`
+- the package's `moreLeanArgs`
 - the library's `moreLeanArgs`
 -/
 @[inline] def leanArgs (self : LeanLib) : Array String :=
-  self.buildType.leanArgs ++ self.pkg.moreLeanArgs ++ self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs
+ self.buildType.leanArgs ++ self.pkg.moreLeanArgs ++ self.config.moreLeanArgs
 
 /--
 The arguments to weakly pass to `lean` when compiling the library's Lean files.

src/lake/Lake/Config/Module.lean

@@ -83,10 +83,7 @@ abbrev pkg (self : Module) : Package :=
   self.srcPath "lean"
 
 @[inline] def relLeanFile (self : Module) : FilePath :=
-  if let some relPath := self.leanFile.toString.dropPrefix? self.pkg.dir.toString then
-    FilePath.mk (relPath.drop 1).toString -- remove leading `/`
-  else
-    self.leanFile
+  relPathFrom self.pkg.dir self.leanFile
 
 @[inline] def leanLibPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.leanLibDir ext
@@ -94,6 +91,12 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def oleanFile (self : Module) : FilePath :=
   self.leanLibPath "olean"
 
+@[inline] def oleanServerFile (self : Module) : FilePath :=
+  self.leanLibPath "olean.server"
+
+@[inline] def oleanPrivateFile (self : Module) : FilePath :=
+  self.leanLibPath "olean.private"
+
 @[inline] def ileanFile (self : Module) : FilePath :=
   self.leanLibPath "ilean"
 
@@ -103,6 +106,9 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def irPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.irDir ext
 
+@[inline] def setupFile (self : Module) : FilePath :=
+  self.irPath "setup.json"
+
 @[inline] def cFile (self : Module) : FilePath :=
   self.irPath "c"
 
@@ -136,7 +142,7 @@ def dynlibSuffix := "-1"
 @[inline] def dynlibFile (self : Module) : FilePath :=
   self.pkg.leanLibDir / s!"{self.dynlibName}.{sharedLibExt}"
 
-@[inline] def serverOptions (self : Module) : Array LeanOption :=
+@[inline] def serverOptions (self : Module) : LeanOptions :=
   self.lib.serverOptions
 
 @[inline] def buildType (self : Module) : BuildType :=
@@ -151,6 +157,9 @@ def dynlibSuffix := "-1"
 @[inline] def plugins (self : Module) : TargetArray Dynlib :=
   self.lib.plugins
 
+@[inline] def leanOptions (self : Module) : LeanOptions :=
+  self.lib.leanOptions
+
 @[inline] def leanArgs (self : Module) : Array String :=
   self.lib.leanArgs
 

src/lake/Lake/Config/Package.lean

@@ -513,8 +513,8 @@ namespace Package
   self.config.moreGlobalServerArgs
 
 /-- The package's `moreServerOptions` configuration appended to its `leanOptions` configuration. -/
-@[inline] def moreServerOptions (self : Package) : Array LeanOption :=
-  self.config.leanOptions ++ self.config.moreServerOptions
+@[inline] def moreServerOptions (self : Package) : LeanOptions :=
+  LeanOptions.ofArray self.config.leanOptions ++ self.config.moreServerOptions
 
 /-- The package's `buildType` configuration. -/
 @[inline] def buildType (self : Package) : BuildType :=
@@ -533,12 +533,12 @@ namespace Package
   self.config.plugins
 
 /-- The package's `leanOptions` configuration. -/
-@[inline] def leanOptions (self : Package) : Array LeanOption :=
-  self.config.leanOptions
+@[inline] def leanOptions (self : Package) : LeanOptions :=
+  .ofArray self.config.leanOptions
 
 /-- The package's `moreLeanArgs` configuration appended to its `leanOptions` configuration. -/
 @[inline] def moreLeanArgs (self : Package) : Array String :=
-  self.config.leanOptions.map (·.asCliArg) ++ self.config.moreLeanArgs
+  self.config.moreLeanArgs
 
 /-- The package's `weakLeanArgs` configuration. -/
 @[inline] def weakLeanArgs (self : Package) : Array String :=

src/lake/Lake/Config/Workspace.lean

@@ -11,9 +11,9 @@ import Lake.Config.Env
 import Lake.Util.Log
 
 open System
+open Lean (Name LeanOptions)
 
 namespace Lake
-open Lean (Name)
 
 /-- A Lake workspace -- the top-level package directory. -/
 structure Workspace : Type where
@@ -66,6 +66,14 @@ namespace Workspace
 @[inline] def pkgsDir (self : Workspace) : FilePath :=
   self.root.pkgsDir
 
+/-- Options to pass to `lean` for files outside a library (e.g., via `lake lean`). -/
+@[inline] def leanOptions (self : Workspace) : LeanOptions :=
+  self.root.leanOptions
+
+/-- Options to pass to the Lean server when editing Lean files outside a library. -/
+@[inline] def serverOptions (self : Workspace) : LeanOptions :=
+  self.root.moreServerOptions
+
 /-- The workspace's Lake manifest. -/
 @[inline] def manifestFile (self : Workspace) : FilePath :=
   self.root.manifestFile

src/lake/Lake/Util/FilePath.lean

@@ -10,6 +10,13 @@ open System Lean
 
 namespace Lake
 
+/-- Returns the portion of `path` relative to `root`. If none, returns `path` verbatim. -/
+def relPathFrom (root path : FilePath) : FilePath :=
+  if let some relPath := path.toString.dropPrefix? root.toString then
+    FilePath.mk (relPath.drop 1).toString -- remove leading `/`
+  else
+    path
+
 /--
 Convert a relative file path to a platform-independent string.
 Uses `/` as the path separator, even on Windows.

src/lake/tests/lean/test.sh

@@ -12,7 +12,7 @@ test_out 'Hello Bob!' lean Test.lean -- --run Test.lean Bob
 
 # Test that Lake uses module-specific configuration
 # if the source file is a module in the workspace
-test_out '-Dweak.foo="bar"' -v lean Lib/Basic.lean
+test_out '"options":{"weak.foo":"bar"}' -v lean Lib/Basic.lean
 
 # cleanup
 rm -f produced.out

src/lake/tests/noBuild/ImportTest.lean

@@ -0,0 +1 @@
+import Test

src/lake/tests/noBuild/test.sh

@@ -10,11 +10,11 @@ NO_BUILD_CODE=3
 
 # Test `--no-build` for setup-file and module builds (`buildUnlessUpToDate`)
 echo "# TEST: --no-build setup-file & modules"
-test_status $NO_BUILD_CODE setup-file bogus Test --no-build
+test_status $NO_BUILD_CODE setup-file ImportTest.lean --no-build
 test ! -f .lake/build/lib/lean/Test.olean
 test_run build Test
 test -f .lake/build/lib/lean/Test.olean
-test_run setup-file bogus Test --no-build
+test_run setup-file ImportTest.lean --no-build
 
 # Test `--no-build` for file builds (`buildFileUnlessUpToDate`)
 echo "# TEST: --no-build file"

src/lake/tests/precompileLink/ImportDownstream.lean

@@ -0,0 +1 @@
+import Downstream

src/lake/tests/precompileLink/test.sh

@@ -13,7 +13,7 @@ test_run -v exe orderTest
 
 # Test that transitively importing a precompiled module
 # from a non-precompiled module works
-test_not_out '"pluginPaths":[]' -v setup-file bogus Downstream
+test_not_out '"pluginPaths":[]' -v setup-file ImportDownstream.lean
 test_run -v build Downstream
 
 # Test that `moreLinkArgs` are included when linking precompiled modules

src/lake/tests/setupFile/ImportFoo.lean

@@ -0,0 +1 @@
+import Foo

src/lake/tests/setupFile/test.sh

@@ -8,20 +8,20 @@ source ../common.sh
 #---
 
 # Test that, by default, no plugins are used.
-test_out '"pluginPaths":[]' setup-file bogus Foo
+test_out '"pluginPaths":[]' setup-file ImportFoo.lean
 
 # Test that, by default, no dynlibs are used.
-test_out '"loadDynlibPaths":[]' setup-file bogus Foo
+test_out '"loadDynlibPaths":[]' setup-file ImportFoo.lean
 
 # Test that, generally, no options are set.
-test_out '"setupOptions":{}' setup-file bogus Foo
+test_out '"setupOptions":{}' setup-file ImportFoo.lean
 
 # Test that a more specific configuration will be used if
 # Lake can identify the module corresponding to the path.
 test_out '"setupOptions":{"weak.foo":"bar"}' setup-file Test.lean
 
 # Test that `setup-file` on an invalid Lean configuration file succeeds.
-test_run -f invalid.lean setup-file invalid.lean Lake
+test_run -f invalid.lean setup-file invalid.lean
 
 # Test that `setup-file` on a configuration file uses the Lake plugin,
 # even if the file is invalid and/or is not using a `Lake` import.