chore: partially reverrt "feat: lake: use lean --setup "

Author: tydeu

src/lake/Lake/Build/Actions.lean

@@ -4,8 +4,6 @@ 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
@@ -23,30 +21,29 @@ namespace Lake
 
 def compileLeanModule
   (leanFile relLeanFile : FilePath)
-  (setup : ModuleSetup) (setupFile : FilePath)
-  (arts : ModuleArtifacts)
-  (leanArgs : Array String := #[])
-  (leanPath : SearchPath := [])
-  (rootDir : FilePath := ".")
-  (lean : FilePath := "lean")
+  (oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
+  (leanPath : SearchPath := []) (rootDir : FilePath := ".")
+  (dynlibs plugins : Array Dynlib := #[])
+  (leanArgs : Array String := #[]) (lean : FilePath := "lean")
 : LogIO Unit := do
-  let mut args :=
-    leanArgs.push leanFile.toString ++ #["-R", rootDir.toString]
-  if let some oleanFile := arts.olean? then
+  let mut args := leanArgs ++
+    #[leanFile.toString, "-R", rootDir.toString]
+  if let some oleanFile := oleanFile? then
     createParentDirs oleanFile
     args := args ++ #["-o", oleanFile.toString]
-  if let some ileanFile := arts.ilean? then
+  if let some ileanFile := ileanFile? then
     createParentDirs ileanFile
     args := args ++ #["-i", ileanFile.toString]
-  if let some cFile := arts.c? then
+  if let some cFile := cFile? then
     createParentDirs cFile
     args := args ++ #["-c", cFile.toString]
-  if let some bcFile := arts.bc? then
+  if let some bcFile := bcFile? then
     createParentDirs bcFile
     args := args ++ #["-b", bcFile.toString]
-  createParentDirs setupFile
-  IO.FS.writeFile setupFile (toJson setup).pretty
-  args := args ++ #["--setup", setupFile.toString]
+  for dynlib in dynlibs do
+    args := args ++ #["--load-dynlib", dynlib.path.toString]
+  for plugin in plugins do
+    args := args ++ #["--plugin", plugin.path.toString]
   args := args.push "--json"
   withLogErrorPos do
   let out ← rawProc {

src/lake/Lake/Build/Facets.lean

@@ -43,43 +43,24 @@ 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 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
+builtin_facet deps : Module => ModuleDeps
 
 /--
 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 => ModuleArtifacts
+builtin_facet leanArts : Module => Unit
 
 /-- 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

@@ -161,64 +161,6 @@ 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.
@@ -234,17 +176,8 @@ 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
 
@@ -254,27 +187,15 @@ 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