leanprover · tydeu · Jun 23, 2025 · Jun 9, 2025 · Jun 10, 2025 · Jun 10, 2025
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
@@ -158,10 +158,10 @@ def runFrontend
       return .ok {
         trustLevel
         mainModuleName := setup.name
-        isModule := setup.isModule
-        imports := setup.imports
+        isModule := strictOr setup.isModule stx.isModule
+        imports := setup.imports?.getD stx.imports
         plugins := plugins ++ setup.plugins
-        modules := setup.modules
+        importArts := setup.importArts
         -- override cmdline options with setup options
         opts := opts.mergeBy (fun _ _ hOpt => hOpt) setup.options.toOptions
       }

diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Module
-import Lean.Util.Paths
 import Lean.CoreM
 
 namespace Lean.Elab
@@ -29,13 +28,17 @@ def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Arr
       | _ => unreachable!
   | _ => unreachable!
 
+def HeaderSyntax.toModuleHeader (stx : HeaderSyntax) : ModuleHeader where
+  isModule := stx.isModule
+  imports := stx.imports
+
 abbrev headerToImports := @HeaderSyntax.imports
 
 def processHeaderCore
     (startPos : String.Pos) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
     (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
-    (mainModule := Name.anonymous) (arts : NameMap ModuleArtifacts := {})
+    (mainModule := Name.anonymous) (arts : NameMap ImportArtifacts := {})
     : IO (Environment × MessageLog) := do
   let level := if isModule then
     if Elab.inServer.get opts then

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
@@ -1876,18 +1876,6 @@ abbrev ImportStateM := StateRefT ImportState IO
 @[inline] nonrec def ImportStateM.run (x : ImportStateM α) (s : ImportState := {}) : IO (α × ImportState) :=
   x.run s
 
-def ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath := Id.run do
-  let mut fnames := #[]
-  -- Opportunistically load all available parts.
-  -- Producer (e.g., Lake) should limit parts to the proper import level.
-  if let some mFile := arts.olean? then
-    fnames := fnames.push mFile
-    if let some sFile := arts.oleanServer? then
-      fnames := fnames.push sFile
-      if let some pFile := arts.oleanPrivate? then
-        fnames := fnames.push pFile
-  return fnames
-
 private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do
   let mFile ← findOLean mod
   unless (← mFile.pathExists) do
@@ -1904,7 +1892,7 @@ private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do
   return fnames
 
 partial def importModulesCore
-    (imports : Array Import) (isModule := false) (arts : NameMap ModuleArtifacts := {}) :
+    (imports : Array Import) (isModule := false) (arts : NameMap ImportArtifacts := {}) :
     ImportStateM Unit := do
   go imports (importAll := true) (isExported := isModule) (isMeta := false)
   if isModule then
@@ -1977,10 +1965,9 @@ where go (imports : Array Import) (importAll isExported isMeta : Bool) := do
       continue
     let fnames ←
       if let some arts := arts.find? i.module then
-        let fnames := arts.oleanParts
-        if fnames.isEmpty then
-          findOLeanParts i.module
-        else pure fnames
+        -- Opportunistically load all available parts.
+        -- Producer (e.g., Lake) should limit parts to the proper import level.
+        pure arts.oleanParts
       else
         findOLeanParts i.module
     let parts ← readModuleDataParts fnames
@@ -2146,7 +2133,7 @@ as if no `module` annotations were present in the imports.
 -/
 def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0)
     (plugins : Array System.FilePath := #[]) (leakEnv := false) (loadExts := false)
-    (level := OLeanLevel.private) (arts : NameMap ModuleArtifacts := {})
+    (level := OLeanLevel.private) (arts : NameMap ImportArtifacts := {})
     : IO Environment := profileitIO "import" opts do
   for imp in imports do
     if imp.module matches .anonymous then

@@ -291,8 +291,8 @@ structure SetupImportsResult where
   opts : Options
   /-- Kernel trust level. -/
   trustLevel : UInt32 := 0
-  /-- Pre-resolved artifacts of related modules (e.g., this module's transitive imports). -/
-  modules : NameMap ModuleArtifacts := {}
+  /-- Pre-resolved artifacts of transitively imported modules. -/
+  importArts : NameMap ImportArtifacts := {}
   /-- Lean plugins to load as part of the environment setup. -/
   plugins : Array System.FilePath := #[]
 
@@ -479,7 +479,7 @@ where
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
       let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
         stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
-        setup.trustLevel setup.plugins setup.mainModuleName setup.modules
+        setup.trustLevel setup.plugins setup.mainModuleName setup.importArts
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then

@@ -5,7 +5,6 @@ Authors: Marc Huisinga
 -/
 prelude
 import Lean.Data.NameTrie
-import Lean.Util.Paths
 import Lean.Util.LakePath
 import Lean.Server.Completion.CompletionItemData
 import Lean.Parser.Module

@@ -14,7 +14,6 @@ import Lean.Environment
 import Lean.Data.Lsp
 import Lean.Data.Json.FromToJson
 
-import Lean.Util.FileSetupInfo
 import Lean.LoadDynlib
 import Lean.Language.Lean
 
@@ -372,7 +371,7 @@ def setupImports
     (doc         : DocumentMeta)
     (cmdlineOpts : Options)
     (chanOut     : Std.Channel JsonRpc.Message)
-    (stx         : TSyntax ``Parser.Module.header)
+    (stx         : Elab.HeaderSyntax)
     : Language.ProcessingT IO (Except Language.Lean.HeaderProcessedSnapshot SetupImportsResult) := do
   let importsAlreadyLoaded ← importsLoadedRef.modifyGet ((·, true))
   if importsAlreadyLoaded then
@@ -384,9 +383,9 @@ def setupImports
     -- should not be visible to user as task is already canceled
     return .error { diagnostics := .empty, result? := none }
 
+  let header := stx.toModuleHeader
   chanOut.sync.send <| mkInitialIleanInfoUpdateNotification doc <| collectImports stx
-  let imports := Elab.headerToImports stx
-  let fileSetupResult ← setupFile doc imports fun stderrLine => do
+  let fileSetupResult ← setupFile doc header fun stderrLine => do
     let progressDiagnostic := {
       range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
       -- make progress visible anywhere in the file
@@ -412,8 +411,10 @@ def setupImports
     }
   | _ => pure ()
 
+  let setup := fileSetupResult.setup
+
   -- override cmdline options with file options
-  let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) fileSetupResult.fileOptions
+  let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) setup.options.toOptions
 
   -- default to async elaboration; see also `Elab.async` docs
   let opts := Elab.async.setIfNotSet opts true
@@ -422,10 +423,11 @@ def setupImports
 
   return .ok {
     mainModuleName := doc.mod
-    isModule := Elab.HeaderSyntax.isModule stx
-    imports
+    isModule := strictOr setup.isModule header.isModule
+    imports := setup.imports?.getD header.imports
     opts
-    plugins := fileSetupResult.plugins
+    importArts := setup.importArts
+    plugins := setup.plugins
   }
 
 /- Worker initialization sequence. -/

@@ -6,7 +6,6 @@ Authors: Sebastian Ullrich, Marc Huisinga
 prelude
 import Init.System.IO
 import Lean.Server.Utils
-import Lean.Util.FileSetupInfo
 import Lean.Util.LakePath
 import Lean.LoadDynlib
 import Lean.Server.ServerTask
@@ -24,20 +23,22 @@ structure LakeSetupFileOutput where
 partial def runLakeSetupFile
     (m                 : DocumentMeta)
     (lakePath filePath : System.FilePath)
-    (imports           : Array Import)
+    (header            : ModuleHeader)
     (handleStderr      : String → IO Unit)
     : IO LakeSetupFileOutput := do
-  let mut args := #["setup-file", filePath.toString] ++ imports.map (toString ·.module)
+  let mut args := #["setup-file", filePath.toString, "-"]
   if m.dependencyBuildMode matches .never then
     args := args.push "--no-build" |>.push "--no-cache"
   let spawnArgs : Process.SpawnArgs := {
-    stdin  := Process.Stdio.null
+    stdin  := Process.Stdio.piped
     stdout := Process.Stdio.piped
     stderr := Process.Stdio.piped
     cmd    := lakePath.toString
     args
   }
   let lakeProc ← Process.spawn spawnArgs
+  let (stdin, lakeProc) ← lakeProc.takeStdin
+  stdin.putStrLn (toJson header).compress
 
   let rec processStderr (acc : String) : IO String := do
     let line ← lakeProc.stderr.getLine
@@ -68,61 +69,53 @@ inductive FileSetupResultKind where
 structure FileSetupResult where
   /-- Kind of outcome. -/
   kind        : FileSetupResultKind
-  /-- Additional options from successful setup, or else empty. -/
-  fileOptions : Options
-  /-- Lean plugins from successful setup, or else empty. -/
-  plugins     : Array System.FilePath
+  /-- Configuration from a successful setup, or else the default. -/
+  setup       : ModuleSetup
 
-def FileSetupResult.ofSuccess (fileOptions : Options)
-    (plugins : Array System.FilePath) : IO FileSetupResult := do return {
+def FileSetupResult.ofSuccess (setup : ModuleSetup) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.success
-  fileOptions, plugins
+  setup
 }
 
-def FileSetupResult.ofNoLakefile : IO FileSetupResult := do return {
+def FileSetupResult.ofNoLakefile (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.noLakefile
-  fileOptions   := Options.empty
-  plugins       := #[]
+  setup         := {name := m.mod, isModule := header.isModule}
 }
 
-def FileSetupResult.ofImportsOutOfDate : IO FileSetupResult := do return {
+def FileSetupResult.ofImportsOutOfDate (m : DocumentMeta) (header : ModuleHeader) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.importsOutOfDate
-  fileOptions   := Options.empty
-  plugins       := #[]
+  setup         := {name := m.mod, isModule := header.isModule}
 }
 
-def FileSetupResult.ofError (msg : String) : IO FileSetupResult := do return {
+def FileSetupResult.ofError (m : DocumentMeta) (header : ModuleHeader) (msg : String) : IO FileSetupResult := do return {
   kind          := FileSetupResultKind.error msg
-  fileOptions   := Options.empty
-  plugins       := #[]
+  setup         := {name := m.mod, isModule := header.isModule}
 }
 
 /-- 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
+partial def setupFile (m : DocumentMeta) (header : ModuleHeader) (handleStderr : String → IO Unit) : IO FileSetupResult := do
   let some filePath := System.Uri.fileUriToPath? m.uri
-    | return ← FileSetupResult.ofNoLakefile -- untitled files have no lakefile
+    | return ← FileSetupResult.ofNoLakefile m header -- untitled files have no lakefile
 
   let lakePath ← determineLakePath
   if !(← System.FilePath.pathExists lakePath) then
-    return ← FileSetupResult.ofNoLakefile
+    return ← FileSetupResult.ofNoLakefile m header
 
-  let result ← runLakeSetupFile m lakePath filePath imports handleStderr
+  let result ← runLakeSetupFile m lakePath filePath header 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 pluginPaths ← info.paths.pluginPaths.mapM realPathNormalized
-    FileSetupResult.ofSuccess info.setupOptions.toOptions pluginPaths
+    let Except.ok (setup : ModuleSetup) := Json.parse result.stdout >>= fromJson?
+      | return ← FileSetupResult.ofError m header s!"Invalid output from `{cmdStr}`:\n{result.stdout}\nstderr:\n{result.stderr}"
+    setup.dynlibs.forM loadDynlib
+    FileSetupResult.ofSuccess setup
   | 2 => -- exit code for lake reporting that there is no lakefile
-    FileSetupResult.ofNoLakefile
+    FileSetupResult.ofNoLakefile m header
   | 3 => -- exit code for `--no-build`
-    FileSetupResult.ofImportsOutOfDate
+    FileSetupResult.ofImportsOutOfDate m header
   | _ =>
-    FileSetupResult.ofError s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"
+    FileSetupResult.ofError m header s!"`{cmdStr}` failed:\n{result.stdout}\nstderr:\n{result.stderr}"
@@ -11,8 +11,6 @@ import Std.Data.TreeMap
 import Init.Data.ByteArray
 import Lean.Data.RBMap
 
-import Lean.Util.Paths
-
 import Lean.Data.FuzzyMatching
 import Lean.Data.Json
 import Lean.Data.Lsp

diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean
@@ -38,6 +38,26 @@ structure ModuleHeader where
   isModule : Bool
   deriving Repr, Inhabited, ToJson, FromJson
 
+/--
+Module data files used for an `import` statement.
+This structure is designed for efficient JSON serialization.
+-/
+structure ImportArtifacts where
+  oleanParts : Array System.FilePath
+  deriving Repr, Inhabited
+
+instance : ToJson ImportArtifacts := ⟨(toJson ·.oleanParts)⟩
+instance : FromJson ImportArtifacts := ⟨(.mk <$> fromJson? ·)⟩
+
+def ImportArtifacts.olean? (arts : ImportArtifacts) :=
+  arts.oleanParts[0]?
+
+def ImportArtifacts.oleanServer? (arts : ImportArtifacts) :=
+  arts.oleanParts[1]?
+
+def ImportArtifacts.oleanPrivate? (arts : ImportArtifacts) :=
+  arts.oleanParts[2]?
+
 /-- Files containing data for a single module. -/
 structure ModuleArtifacts where
   lean? : Option System.FilePath := none
@@ -49,19 +69,32 @@ structure ModuleArtifacts where
   bc? : Option System.FilePath := none
   deriving Repr, Inhabited, ToJson, FromJson
 
-/--
-A module's setup information as described by a JSON file.
-Supersedes the module's header when the `--setup` CLI option is used.
--/
+def ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath := Id.run do
+  let mut fnames := #[]
+  if let some mFile := arts.olean? then
+    fnames := fnames.push mFile
+    if let some sFile := arts.oleanServer? then
+      fnames := fnames.push sFile
+      if let some pFile := arts.oleanPrivate? then
+        fnames := fnames.push pFile
+  return fnames
+
+/-- A module's setup information as described by a JSON file. -/
 structure ModuleSetup where
   /-- Name of the module. -/
   name : Name
-  /-- Whether the module is participating in the module system. -/
+  /--
+  Whether the module, by default, participates in the module system.
+  Even if `false`, a module can still choose to participate by using `module` in its header.
+  -/
   isModule : Bool := false
-  /-- The module's direct imports. -/
-  imports : Array Import := #[]
-  /-- Pre-resolved artifacts of related modules (e.g., this module's transitive imports). -/
-  modules : NameMap ModuleArtifacts := {}
+  /--
+  The module's direct imports.
+  If `none`, uses the imports from the module header.
+  -/
+  imports? : Option (Array Import) := none
+  /-- Pre-resolved artifacts of transitively imported modules. -/
+  importArts : NameMap ImportArtifacts := {}
   /-- Dynamic libraries to load with the module. -/
   dynlibs : Array System.FilePath := #[]
   /-- Plugins to initialize with the module. -/

diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean
@@ -29,7 +29,6 @@ import Lean.Util.SCC
 import Lean.Util.TestExtern
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
-import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
 import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation

diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean