feat: use module setup in lake lean & setup-file

Author: tydeu

src/Lean/Elab/ParseImportsFast.lean

@@ -188,16 +188,16 @@ 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 setIsExported (isExported : Bool) : Parser := fun _ s =>
-  { s with isExported := isExported }
+  { s with isExported }
 
 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) >>
     keyword "import" >>

src/lake/Lake/Build/Facets.lean

@@ -54,7 +54,14 @@ 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.

src/lake/Lake/Build/Info.lean

@@ -192,6 +192,9 @@ namespace Module
 @[inherit_doc precompileImportsFacet] abbrev precompileImports (self : Module) :=
   self.facetCore precompileImportsFacet
 
+@[inherit_doc setupFacet] abbrev setup  (self : Module) :=
+  self.facetCore setupFacet
+
 @[inherit_doc depsFacet] abbrev deps  (self : Module) :=
   self.facetCore depsFacet
 

src/lake/Lake/Build/Module.lean

@@ -37,7 +37,7 @@ def Module.srcFacetConfig : ModuleFacetConfig srcFacet :=
 def Module.recParseHeader (mod : Module) : FetchM (Job ModuleHeader) := do
   (← mod.src.fetch).mapM fun srcFile => do
     let contents ← IO.FS.readFile srcFile
-    Lean.parseImports' contents mod.leanFile.toString
+    Lean.parseImports' contents srcFile.toString
 
 /-- The `ModuleFacetConfig` for the builtin `headerFacet`. -/
 def Module.headerFacetConfig : ModuleFacetConfig headerFacet :=
@@ -211,14 +211,15 @@ Recursively build a module's dependencies, including:
 * 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 headerJob ← mod.header.fetch
   let directImports ← (← mod.imports.fetch).await
   let importJobs ← directImports.mapM fun imp => do
     if imp.name = mod.name then
@@ -240,6 +241,7 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do
   let pluginsJob ← mod.plugins.fetchIn mod.pkg "module plugins"
 
   extraDepJob.bindM fun _ => do
+  headerJob.bindM fun header => do
   importJob.bindM (sync := true) fun _ => do
   let depTrace ← takeTrace
   impLibsJob.bindM (sync := true) fun impLibs => do
@@ -254,11 +256,24 @@ 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 := {} -- TODO
+      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). -/
 def Module.clearOutputHashes (mod : Module) : IO PUnit := do
@@ -290,22 +305,12 @@ def Module.recBuildLean (mod : Module) : FetchM (Job Unit) := do
   withRegisterJob mod.name.toString do
   (← mod.src.fetch).bindM fun srcFile => do
   let srcTrace ← getTrace
-  (← mod.header.fetch).bindM fun header => do
-  (← mod.deps.fetch).mapM fun {dynlibs, plugins} => do
+  (← mod.setup.fetch).mapM fun setup => do
     addLeanTrace
-    addTrace <| traceOptions mod.leanOptions "Module.leanOptions"
+    addTrace <| traceOptions setup.options "options"
     addPureTrace mod.leanArgs "Module.leanArgs"
     setTraceCaption s!"{mod.name.toString}:leanArts"
     let upToDate ← buildUnlessUpToDate? (oldTrace := srcTrace.mtime) mod (← getTrace) mod.traceFile do
-      let setup : ModuleSetup := {
-        name := mod.name
-        isModule := header.isModule
-        imports := header.imports
-        modules := {} -- TODO
-        dynlibs := dynlibs.map (·.path.toString)
-        plugins := plugins.map (·.path.toString)
-        options := mod.leanOptions
-      }
       let args := mod.weakLeanArgs ++ mod.leanArgs
       compileLeanModule srcFile setup mod.setupFile mod.arts args
         (← getLeanPath) mod.rootDir (← getLean)
@@ -327,7 +332,7 @@ def Module.leanArtsFacetConfig : ModuleFacetConfig leanArtsFacet :=
       transitive imports. However, they are independent of their module sources.
       -/
       newTrace s!"{mod.name.toString}:olean"
-      addTrace (← mod.deps.fetch).getTrace.withoutInputs
+      addTrace (← mod.setup.fetch).getTrace.withoutInputs
       addTrace (← fetchFileTrace file)
       return file
 
@@ -486,6 +491,7 @@ def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert importsFacet importsFacetConfig
   |>.insert transImportsFacet transImportsFacetConfig
   |>.insert precompileImportsFacet precompileImportsFacetConfig
+  |>.insert setupFacet setupFacetConfig
   |>.insert depsFacet depsFacetConfig
   |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert oleanFacet oleanFacetConfig

src/lake/Lake/CLI/Main.lean

@@ -446,8 +446,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,15 +539,15 @@ private def evalLeanFile
 : LoggerIO UInt32 := do
   let some path ← resolvePath? leanFile
     | error s!"file not found: {leanFile}"
-  let args ← 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 mkArgs path deps (some mod.rootDir) mod.leanArgs mod.leanOptions
+      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 mkArgs path deps none ws.root.moreLeanArgs ws.root.leanOptions
+      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
@@ -555,17 +557,15 @@ private def evalLeanFile
   let child ← IO.Process.spawn spawnArgs
   child.wait
 where
-  mkArgs leanFile deps rootDir? cfgArgs opts := 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]
-    for (name, val) in opts.values do
-      args := args.push s!"-D{name}={val.asCliFlagValue}"
+    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

src/lake/Lake/CLI/Serve.lean

@@ -23,11 +23,28 @@ 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 imports := header.imports.filterMap (ws.findModule? ·.module)
+  let {dynlibs, plugins} ← ws.runBuild (buildImportsAndDeps fileName 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 +54,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,19 +78,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 setup ← ws.runBuild (cfg := buildConfig) do
+        withRegisterJob s!"{mod.name}:setup" do mod.setup.fetch
       let info : FileSetupInfo := {
-        paths := mkLeanPaths ws deps
+        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/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 :=

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/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