feat: lake: reintroduce lean --setup basics (leanprover#8846)

This PR reintroduces the basics of `lean --setup` integration into Lake
without the module computation which is still undergoing performance
debugging in leanprover#8787.

Partially reverts leanprover#8736 and partially reimplements leanprover#8447.

Author: tydeu

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
+  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/Facets.lean

@@ -43,24 +43,54 @@ instance (facet : ModuleFacet α) : FamilyDef FacetOut facet.name α :=
 instance [FamilyOut FacetOut facet α] : CoeDep Name facet (ModuleFacet α) :=
   ⟨facet, FamilyOut.fam_eq⟩
 
+/-- A module's source file path plus its parsed header. -/
+structure ModuleInput where
+  path : FilePath
+  header : ModuleHeader
+
+/--
+The module's processed Lean source file.
+Combines tracing the file with parsing its header.
+-/
+builtin_facet input : Module => ModuleInput
+
+/-- The module's Lean source file. -/
+builtin_facet lean : 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 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 => ModuleDeps
+builtin_facet deps : Module => Opaque
 
 /--
 The core build facet of a Lean file.
 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/Info.lean

@@ -178,6 +178,15 @@ abbrev BuildInfo.moduleFacet (module : Module) (facet : Name) : BuildInfo :=
 
 namespace Module
 
+@[inherit_doc inputFacet] abbrev input (self : Module) :=
+  self.facetCore inputFacet
+
+@[inherit_doc leanFacet] abbrev lean (self : Module) :=
+  self.facetCore leanFacet
+
+@[inherit_doc headerFacet] abbrev header (self : Module) :=
+  self.facetCore headerFacet
+
 @[inherit_doc importsFacet] abbrev imports (self : Module) :=
   self.facetCore importsFacet
 
@@ -187,15 +196,24 @@ 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
 
-@[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

@@ -237,10 +237,6 @@ 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) -/