refactor: add LeanLib/LeanExe/ExternLib + reorg & cleanup

Author: tydeu

Diff for: Lake/Build.lean

@@ -5,7 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Build.Monad
 import Lake.Build.Actions
-import Lake.Build.Module
-import Lake.Build.Library
-import Lake.Build.Executable
+import Lake.Build.LeanLib
+import Lake.Build.LeanExe
 import Lake.Build.Imports

Diff for: Lake/Build/Executable.lean

@@ -31,7 +31,7 @@ Used by `lake print-paths` to build modules for the Lean server.
 Returns the set of module dynlibs built (so they can be loaded by the server).
 
 Builds only module `.olean` and `.ilean` files if the package is configured
-as "Lean-only". Otherwise, also build `.c` and `.o` files.
+as "Lean-only". Otherwise, also build `.c` files.
 -/
 def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
   if imports.isEmpty then
@@ -47,7 +47,7 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build
       else if mod.isLeanOnly then
         buildModuleTop mod &`lean
       else
-        buildModuleTop mod &`lean.o <&> (·.withoutInfo)
+        buildModuleTop mod &`lean.c <&> (·.withoutInfo)
     let importTargets ← failOnBuildCycle res
     let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
     let externLibTargets := bStore.collectPackageFacetArray &`externSharedLibs

Diff for: Lake/Build/Imports.lean

@@ -130,7 +130,7 @@ the initial set of Lake package facets (e.g., `extraDep`).
   -- Build the `extern_lib` targets of the package
   |>.insert &`externSharedLibs (mkPackageFacetBuild <| fun pkg => do
     let mut targets := #[]
-    for (_, config) in pkg.externLibs.toList do
+    for (_, config) in pkg.externLibConfigs.toList do
       let target := staticToLeanDynlibTarget config.target
       targets := targets.push <| ← target.activate
     return targets

Diff for: Lake/Build/Index.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.LeanLib
+
+namespace Lake
+
+-- # Build Package Executable
+
+def LeanExe.target (self : LeanExe) : FileTarget :=
+  BuildTarget.mk' self.file do
+    let cTargetMap ← buildModuleFacetMap #[self.root] &`lean.c
+    let pkgLinkTargets ← self.pkg.linkTargetsOf cTargetMap
+    let linkTargets :=
+      if self.pkg.isLocalModule self.root.name then
+        pkgLinkTargets
+      else
+        let rootTarget := cTargetMap.find? self.root.name |>.get!
+        let rootLinkTarget := self.root.mkOTarget <| Target.active rootTarget
+        #[rootLinkTarget] ++ pkgLinkTargets
+    let target := leanExeTarget self.file linkTargets self.linkArgs
+    target.materializeAsync
+
+protected def Package.exeTarget (self : Package) : FileTarget :=
+  self.builtinExe.target

Diff for: Lake/Build/LeanExe.lean

@@ -10,47 +10,45 @@ open Lean hiding SearchPath
 
 namespace Lake
 
--- # Build Package Lean Lib
-
-def Package.getLibModuleArray (lib : LeanLibConfig) (self : Package) : IO (Array Module) := do
-  return (← lib.getModuleArray self.srcDir).map (⟨self, WfName.ofName ·⟩)
+-- # Build Lean Lib
 
 /--
 Build the `extraDepTarget` of a package and its (transitive) dependencies
 and then build the target `facet` of library's modules recursively, constructing
 a single opaque target for the whole build.
 -/
-def Package.buildLibModules
-(self : Package) (lib : LeanLibConfig) (facet : WfName)
+def LeanLib.buildModules (self : LeanLib) (facet : WfName)
 [DynamicType ModuleData facet (ActiveBuildTarget α)] : SchedulerM Job := do
   let buildMods : BuildM _ := do
-    let mods ← self.getLibModuleArray lib
+    let mods ← self.getModuleArray
     let modTargets ← buildModuleFacetArray mods facet
     (·.task) <$> ActiveTarget.collectOpaqueArray modTargets
   buildMods.catchFailure fun _ => pure <| failure
 
-def Package.mkLibTarget (self : Package) (lib : LeanLibConfig) : OpaqueTarget :=
-  Target.opaque <| self.buildLibModules lib &`lean
+def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget :=
+  Target.opaque <| self.buildModules &`lean
 
 def Package.libTarget (self : Package) : OpaqueTarget :=
-  self.mkLibTarget self.builtinLibConfig
+  self.builtinLib.leanTarget
 
--- # Build Package Static Lib
+-- # Build Static Lib
 
-def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
+def LeanLib.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : LeanLib) : Array (BuildTarget α) :=
   map.fold (fun a n v => if self.isLocalModule n then a.push (Target.active v) else a) #[]
 
-def Package.mkStaticLibTarget (lib : LeanLibConfig) (self : Package) : FileTarget :=
-  let libFile := self.libDir / lib.staticLibFileName
-  BuildTarget.mk' libFile do
-    let mods ← self.getLibModuleArray lib
+protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
+  BuildTarget.mk' self.staticLibFile do
+    let mods ← self.getModuleArray
     let oFileTargets := self.localTargetsOf <| ← buildModuleFacetMap mods &`lean.o
-    staticLibTarget libFile oFileTargets |>.materializeAsync
+    staticLibTarget self.staticLibFile oFileTargets |>.materializeAsync
 
 protected def Package.staticLibTarget (self : Package) : FileTarget :=
-  self.mkStaticLibTarget self.builtinLibConfig
+  self.builtinLib.staticLibTarget
+
+-- # Build Shared Lib
 
--- # Build Package Shared Lib
+def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
+  map.fold (fun a n v => if self.isLocalModule n then a.push (Target.active v) else a) #[]
 
 def Package.linkTargetsOf
 (targetMap : NameMap ActiveFileTarget) (self : Package) : LakeM (Array FileTarget) := do
@@ -66,13 +64,12 @@ def Package.linkTargetsOf
     return self.localTargetsOf targetMap ++ self.externLibTargets ++ ts
   | Except.error _ => panic! "dependency cycle emerged after resolution"
 
-def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget :=
-  let libFile := self.libDir / lib.sharedLibFileName
-  BuildTarget.mk' libFile do
-    let mods ← self.getLibModuleArray lib
-    let linkTargets ← self.linkTargetsOf <| ← buildModuleFacetMap mods &`lean.o
-    let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
+protected def LeanLib.sharedLibTarget (self : LeanLib) : FileTarget :=
+  BuildTarget.mk' self.sharedLibFile do
+    let mods ← self.getModuleArray
+    let linkTargets ← self.pkg.linkTargetsOf <| ← buildModuleFacetMap mods &`lean.o
+    let target := leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs
     target.materializeAsync
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
-  self.mkSharedLibTarget self.builtinLibConfig
+  self.builtinLib.sharedLibTarget

Diff for: Lake/Build/Library.lean renamed to Lake/Build/LeanLib.lean

@@ -40,32 +40,32 @@ def resolveModuleTarget (mod : Module) (facet : String) : Except CliError Opaque
   else
     throw <| CliError.unknownFacet "module" facet
 
-def resolveLibTarget (pkg : Package) (lib : LeanLibConfig) (facet : String) : Except CliError OpaqueTarget :=
+def resolveLibTarget (lib : LeanLib) (facet : String) : Except CliError OpaqueTarget :=
   if facet.isEmpty || facet == "lean" || facet == "oleans" then
-    return pkg.mkLibTarget lib
+    return lib.leanTarget
   else if facet == "static" then
-    return pkg.mkStaticLibTarget lib |>.withoutInfo
+    return lib.staticLibTarget |>.withoutInfo
   else if facet == "shared" then
-    return pkg.mkSharedLibTarget lib |>.withoutInfo
+    return lib.sharedLibTarget |>.withoutInfo
   else
     throw <| CliError.unknownFacet "library" facet
 
-def resolveExeTarget (pkg : Package) (exe : LeanExeConfig) (facet : String) : Except CliError OpaqueTarget :=
+def resolveExeTarget (exe : LeanExe) (facet : String) : Except CliError OpaqueTarget :=
   if facet.isEmpty || facet == "exe" then
-    return pkg.mkExeTarget exe |>.withoutInfo
+    return exe.target |>.withoutInfo
   else
     throw <| CliError.unknownFacet "executable" facet
 
 def resolveTargetInPackage (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget :=
   if let some exe := pkg.findLeanExe? target then
-    resolveExeTarget pkg exe facet
+    resolveExeTarget exe facet
   else if let some lib := pkg.findExternLib? target then
     if facet.isEmpty then
       return lib.target.withoutInfo
     else
       throw <| CliError.invalidFacet target facet
   else if let some lib := pkg.findLeanLib? target then
-    resolveLibTarget pkg lib facet
+    resolveLibTarget lib facet
   else if let some mod := pkg.findModule? target then
     resolveModuleTarget mod facet
   else
@@ -93,15 +93,15 @@ def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError Opaq
     throw <| CliError.unknownFacet "package" facet
 
 def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget :=
-  if let some (pkg, exe) := ws.findLeanExe? spec.toName then
-    resolveExeTarget pkg exe facet
-  else if let some (_, lib) := ws.findExternLib? spec.toName then
+  if let some exe := ws.findLeanExe? spec.toName then
+    resolveExeTarget exe facet
+  else if let some lib := ws.findExternLib? spec.toName then
     if facet.isEmpty then
       return lib.target.withoutInfo
     else
       throw <| CliError.invalidFacet spec facet
-  else if let some (pkg, lib) := ws.findLeanLib? spec.toName then
-    resolveLibTarget pkg lib facet
+  else if let some lib := ws.findLeanLib? spec.toName then
+    resolveLibTarget lib facet
   else if let some pkg := ws.findPackage? spec.toName then
     resolvePackageTarget pkg facet
   else if let some mod := ws.findModule? spec.toName then

Diff for: Lake/CLI/Build.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Config.Package
+
+namespace Lake
+
+/-- An external library -- its package plus its configuration. -/
+structure ExternLib where
+  /-- The package the library belongs to. -/
+  pkg : Package
+   /-- The library's user-defined configuration. -/
+  config : ExternLibConfig
+  deriving Inhabited
+
+/-- Try to find a external library in the package with the given name. -/
+@[inline] def Package.findExternLib? (name : Name) (self : Package) : Option ExternLib :=
+  self.externLibConfigs.find? name |>.map (⟨self, ·⟩)
+
+namespace ExternLib
+
+/-- The external library's user-defined `target`. -/
+@[inline] def target (self : ExternLib) : FileTarget :=
+  self.config.target

Diff for: Lake/Config/ExternLib.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Build.TargetTypes
+
+namespace Lake
+open Lean System
+
+/-- A external library's declarative configuration. -/
+structure ExternLibConfig where
+  /-- The name of the target. -/
+  name : Name
+
+  /-- The library's build target. -/
+  target : FileTarget
+
+deriving Inhabited

Diff for: Lake/Config/ExternLibConfig.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Mac Malone
 -/
 import Lean.Util.Path
+import Lake.Util.Name
 
 open Lean (Name)
 open System (FilePath)
@@ -22,29 +23,25 @@ deriving Inhabited, Repr
 
 instance : Coe Name Glob := ⟨Glob.one⟩
 
-def Glob.matches (m : Name) : (self : Glob) → Bool
+partial def forEachNoduleIn [Monad m] [MonadLiftT IO m]
+(dir : FilePath) (f : WfName → m PUnit) : m PUnit := do
+  for entry in (← dir.readDir) do
+    if (← liftM (m := IO) <| entry.path.isDir) then
+      f entry.fileName
+    else if entry.path.extension == some "lean" then
+      f <| FilePath.withExtension entry.fileName "" |>.toString
+
+namespace Glob
+
+def «matches» (m : Name) : (self : Glob) → Bool
 | one n => n == m
 | submodules n => n.isPrefixOf m && n != m
 | andSubmodules n => n.isPrefixOf m
 
-partial def pushSubmodules
-(rootDir : FilePath) (mod : Name) (arr : Array Name) : IO (Array Name) := do
-  let mut arr := arr
-  let dirPath := Lean.modToFilePath rootDir mod ""
-  for entry in (← dirPath.readDir) do
-    let path := entry.path
-    if (← path.isDir) then
-      arr ← pushSubmodules rootDir (mod ++ entry.fileName) arr
-    else if path.extension == some "lean" then
-      let fileName := FilePath.withExtension entry.fileName "" |>.toString
-      arr := arr.push (mod ++ fileName)
-  return arr
-
-def Glob.pushModules
-(dir : FilePath) (arr : Array Name) : (self : Glob) → IO (Array Name)
-| one n => pure #[n]
-| submodules n => pushSubmodules dir n arr
-| andSubmodules n => pushSubmodules dir n (arr.push n)
-
-def Glob.getModules (dir : FilePath) (self : Glob) : IO (Array Name) :=
-  self.pushModules dir #[]
+def forEachModuleIn [Monad m] [MonadLiftT IO m]
+(dir : FilePath) (f : WfName → m PUnit) : (self : Glob) → m PUnit
+| one n => f (WfName.ofName n)
+| submodules n => forEachNoduleIn (Lean.modToFilePath dir n "") f
+| andSubmodules n =>
+  f (WfName.ofName n) *>
+  forEachNoduleIn (Lean.modToFilePath dir n "") f

Diff for: Lake/Config/Glob.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Config.Module
+
+namespace Lake
+open Lean System
+
+/-- A Lean executable -- its package plus its configuration. -/
+structure LeanExe where
+  /-- The package the executable belongs to. -/
+  pkg : Package
+   /-- The executable's user-defined configuration. -/
+  config : LeanExeConfig
+  deriving Inhabited
+
+/-- The Lean executable built into the package. -/
+@[inline] def Package.builtinExe (self : Package) : LeanExe :=
+  ⟨self, self.builtinExeConfig⟩
+
+/-- Try to find a Lean executable in the package with the given name. -/
+@[inline] def Package.findLeanExe? (name : Name) (self : Package) : Option LeanExe :=
+  self.leanExeConfigs.find? name |>.map (⟨self, ·⟩)
+
+namespace LeanExe
+
+/-- The executable's root module. -/
+@[inline] def root (self : LeanExe) : Module :=
+  ⟨self.pkg, WfName.ofName self.config.root⟩
+
+/--
+The file name of binary executable
+(i.e., `exeName` plus the platform's `exeExtension`).
+-/
+@[inline] def fileName (self : LeanExe) : FilePath :=
+  FilePath.withExtension self.config.exeName FilePath.exeExtension
+
+/-- The path to the executable in the package's `binDir`. -/
+@[inline] def file (self : LeanExe) : FilePath :=
+  self.pkg.binDir / self.fileName
+
+/--
+The arguments to pass to `leanc` when linking the binary executable.
+
+That is, `-rdynamic` (if non-Windows and `supportInterpreter`) plus the
+package's and then the executable's `moreLinkArgs`.
+-/
+def linkArgs (self : LeanExe) : Array String :=
+  if self.config.supportInterpreter && !Platform.isWindows then
+    #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+  else
+    self.pkg.moreLinkArgs ++ self.config.moreLinkArgs