From c0bc0344b025016ef36e4104de0bf3adf5eeecc1 Mon Sep 17 00:00:00 2001 From: tydeu Date: Sun, 26 Jun 2022 18:26:12 -0400 Subject: [PATCH] refactor: add `LeanLib`/`LeanExe`/`ExternLib` + reorg & cleanup --- Lake/Build.lean | 5 +- Lake/Build/Executable.lean | 29 ---- Lake/Build/Imports.lean | 4 +- Lake/Build/Index.lean | 2 +- Lake/Build/LeanExe.lean | 27 ++++ Lake/Build/{Library.lean => LeanLib.lean} | 57 ++++--- Lake/CLI/Build.lean | 26 ++-- Lake/Config/ExternLib.lean | 26 ++++ Lake/Config/ExternLibConfig.lean | 19 +++ Lake/Config/Glob.lean | 41 +++-- Lake/Config/LeanExe.lean | 54 +++++++ Lake/Config/LeanExeConfig.lean | 50 +++++++ Lake/Config/LeanLib.lean | 72 +++++++++ Lake/Config/LeanLibConfig.lean | 80 ++++++++++ Lake/Config/Load.lean | 16 +- Lake/Config/Module.lean | 17 ++- Lake/Config/Package.lean | 50 +++---- Lake/Config/Targets.lean | 173 ---------------------- Lake/Config/Workspace.lean | 22 ++- Lake/DSL/Targets.lean | 4 +- Lake/Util/{String.lean => Casing.lean} | 0 Lake/Util/Name.lean | 29 +++- examples/init/.gitignore | 4 +- 23 files changed, 476 insertions(+), 331 deletions(-) delete mode 100644 Lake/Build/Executable.lean create mode 100644 Lake/Build/LeanExe.lean rename Lake/Build/{Library.lean => LeanLib.lean} (60%) create mode 100644 Lake/Config/ExternLib.lean create mode 100644 Lake/Config/ExternLibConfig.lean create mode 100644 Lake/Config/LeanExe.lean create mode 100644 Lake/Config/LeanExeConfig.lean create mode 100644 Lake/Config/LeanLib.lean create mode 100644 Lake/Config/LeanLibConfig.lean delete mode 100644 Lake/Config/Targets.lean rename Lake/Util/{String.lean => Casing.lean} (100%) diff --git a/Lake/Build.lean b/Lake/Build.lean index cc9b7b7da1..c25666172a 100644 --- a/Lake/Build.lean +++ b/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 --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean deleted file mode 100644 index 2fd1b5c3d4..0000000000 --- a/Lake/Build/Executable.lean +++ /dev/null @@ -1,29 +0,0 @@ -/- -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.Library - -namespace Lake - --- # Build Package Executable - -def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget := - let exeFile := self.binDir / exe.fileName - BuildTarget.mk' exeFile do - let root : Module := ⟨self, WfName.ofName exe.root⟩ - let cTargetMap ← buildModuleFacetMap #[root] &`lean.c - let pkgLinkTargets ← self.linkTargetsOf cTargetMap - let linkTargets := - if self.isLocalModule exe.root then - pkgLinkTargets - else - let rootTarget := cTargetMap.find? root.name |>.get! - let rootLinkTarget := root.mkOTarget <| Target.active rootTarget - #[rootLinkTarget] ++ pkgLinkTargets - let target := leanExeTarget exeFile linkTargets exe.linkArgs - target.materializeAsync - -protected def Package.exeTarget (self : Package) : FileTarget := - self.mkExeTarget self.builtinExeConfig diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index 539b177b5d..a9a8b52c8f 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.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 --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index af44384a37..1b445c81b9 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.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 --git a/Lake/Build/LeanExe.lean b/Lake/Build/LeanExe.lean new file mode 100644 index 0000000000..551f92a866 --- /dev/null +++ b/Lake/Build/LeanExe.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 --git a/Lake/Build/Library.lean b/Lake/Build/LeanLib.lean similarity index 60% rename from Lake/Build/Library.lean rename to Lake/Build/LeanLib.lean index 6246ff58d2..cc3096e8a2 100644 --- a/Lake/Build/Library.lean +++ b/Lake/Build/LeanLib.lean @@ -10,48 +10,46 @@ 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 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) #[] + +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 self.staticLibFile oFileTargets |>.materializeAsync + +protected def Package.staticLibTarget (self : Package) : FileTarget := + self.builtinLib.staticLibTarget + +-- # Build 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.mkStaticLibTarget (lib : LeanLibConfig) (self : Package) : FileTarget := - let libFile := self.libDir / lib.staticLibFileName - BuildTarget.mk' libFile do - let mods ← self.getLibModuleArray lib - let oFileTargets := self.localTargetsOf <| ← buildModuleFacetMap mods &`lean.o - staticLibTarget libFile oFileTargets |>.materializeAsync - -protected def Package.staticLibTarget (self : Package) : FileTarget := - self.mkStaticLibTarget self.builtinLibConfig - --- # Build Package Shared Lib - def Package.linkTargetsOf (targetMap : NameMap ActiveFileTarget) (self : Package) : LakeM (Array FileTarget) := do let collect dep recurse := 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 --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 6c530c00e2..18c385cd5d 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.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 --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean new file mode 100644 index 0000000000..371fc3b6a9 --- /dev/null +++ b/Lake/Config/ExternLib.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 --git a/Lake/Config/ExternLibConfig.lean b/Lake/Config/ExternLibConfig.lean new file mode 100644 index 0000000000..f7eeb199ac --- /dev/null +++ b/Lake/Config/ExternLibConfig.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 --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean index 18be1ab7a2..ce2d683c27 100644 --- a/Lake/Config/Glob.lean +++ b/Lake/Config/Glob.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 --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean new file mode 100644 index 0000000000..6a0502e071 --- /dev/null +++ b/Lake/Config/LeanExe.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 diff --git a/Lake/Config/LeanExeConfig.lean b/Lake/Config/LeanExeConfig.lean new file mode 100644 index 0000000000..f60bd6a545 --- /dev/null +++ b/Lake/Config/LeanExeConfig.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +namespace Lake +open Lean System + +/-- A Lean executable's declarative configuration. -/ +structure LeanExeConfig where + /-- The name of the target. -/ + name : Name + + /-- + The root module of the binary executable. + Should include a `main` definition that will serve + as the entry point of the program. + + The root is built by recursively building its + local imports (i.e., fellow modules of the workspace). + + Defaults to the name of the target. + -/ + root : Name := name + + /-- + The name of the binary executable. + Defaults to the target name with any `.` replaced with a `-`. + -/ + exeName : String := name.toStringWithSep "-" (escape := false) + + /-- + Whether to expose symbols within the executable to the Lean interpreter. + This allows the executable to interpret Lean files (e.g., via + `Lean.Elab.runFrontend`). + + Implementation-wise, this passes `-rdynamic` to the linker when building + on non-Windows systems. + + Defaults to `false`. + -/ + supportInterpreter : Bool := false + + /-- + Additional arguments to pass to `leanc` when linking the binary executable. + These will come *after* the paths of the package's external libraries. + -/ + moreLinkArgs : Array String := #[] + +deriving Inhabited, Repr diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean new file mode 100644 index 0000000000..be61f919cb --- /dev/null +++ b/Lake/Config/LeanLib.lean @@ -0,0 +1,72 @@ +/- +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 +open Lean System + +/-- A Lean library -- its package plus its configuration. -/ +structure LeanLib where + /-- The package the library belongs to. -/ + pkg : Package + /-- The library's user-defined configuration. -/ + config : LeanLibConfig + deriving Inhabited + +/-- The Lean library built into the package. -/ +@[inline] def Package.builtinLib (self : Package) : LeanLib := + ⟨self, self.builtinLibConfig⟩ + +/-- Try to find a Lean library in the package with the given name. -/ +@[inline] def Package.findLeanLib? (name : Name) (self : Package) : Option LeanLib := + self.leanLibConfigs.find? name |>.map (⟨self, ·⟩) + +namespace LeanLib + +/- The package's `srcDir` joined with the library's `srcDir`. -/ +def srcDir (self : LeanLib) : FilePath := + self.pkg.srcDir / self.config.srcDir + +/-- Whether the given module is considered local to the library. -/ +@[inline] def isLocalModule (mod : Name) (self : LeanLib) : Bool := + self.config.isLocalModule mod + +/-- Whether the given module is a buildable part of the library. -/ +@[inline] def isBuildableModule (mod : Name) (self : LeanLib) : Bool := + self.config.isBuildableModule mod + +/-- The file name of the library's static binary (i.e., `lib{libName}.a`) -/ +def staticLibFileName (self : LeanLib) : FilePath := + s!"lib{self.config.libName}.a" + +/-- The path to the static library in the package's `libDir`. -/ +def staticLibFile (self : LeanLib) : FilePath := + self.pkg.libDir / self.staticLibFileName + +/-- The file name of the library's shared binary (i.e., its `dll`/`dylib`/`so`) . -/ +def sharedLibFileName (self : LeanLib) : FilePath := + s!"{self.config.libName}.{sharedLibExt}" + +/-- The path to the shared library in the package's `libDir`. -/ +def sharedLibFile (self : LeanLib) : FilePath := + self.pkg.libDir / self.sharedLibFileName + +/-- +The arguments to pass to `leanc` when compiling the library's C files. +It is `-O3`, `-DNDEBUG`, the package's `moreLeancArgs`, and then the library's +`moreLeancArgs`. + +TODO: Use this option. +-/ +def leancArgs (self : LeanLib) : Array String := + self.pkg.moreLeancArgs ++ self.config.moreLeancArgs + +/-- +The arguments to pass to `leanc` when linking the shared library. +That is, the package's `moreLinkArgs` plus the library's `moreLinkArgs`. +-/ +def linkArgs (self : LeanLib) : Array String := + self.pkg.moreLinkArgs ++ self.config.moreLinkArgs diff --git a/Lake/Config/LeanLibConfig.lean b/Lake/Config/LeanLibConfig.lean new file mode 100644 index 0000000000..88dd1678e1 --- /dev/null +++ b/Lake/Config/LeanLibConfig.lean @@ -0,0 +1,80 @@ +/- +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.Util.Casing +import Lake.Config.InstallPath +import Lake.Config.Glob + +namespace Lake +open Lean System + +/-- A Lean library's declarative configuration. -/ +structure LeanLibConfig where + /-- The name of the target. -/ + name : Name + + /-- + The subdirectory of the package containing the library's Lean source files. + Defaults to the package's `srcDir`. + + (This will be passed to `lean` as the `-R` option.) + -/ + srcDir : FilePath := "." + + /-- + The root module(s) of the library. + + Submodules of these roots (e.g., `Lib.Foo` of `Lib`) are considered + part of the package. + + Defaults to a single root of the library's upper camel case name. + -/ + roots : Array Name := #[toUpperCamelCase name] + + /-- + An `Array` of module `Glob`s to build for the library. + Defaults to a `Glob.one` of each of the library's `roots`. + + Submodule globs build every source file within their directory. + Local imports of glob'ed files (i.e., fellow modules of the workspace) are + also recursively built. + -/ + globs : Array Glob := roots.map Glob.one + + /-- + The name of the library. + Used as a base for the file names of its static and dynamic binaries. + Defaults to the upper camel case name of the target. + -/ + libName := toUpperCamelCase name |>.toString (escape := false) + + /-- + Additional arguments to pass to `leanc` + while compiling the library's C source files generated by `lean`. + + Lake already passes `-O3` and `-DNDEBUG` automatically, + but you can change this by, for example, adding `-O0` and `-UNDEBUG`. + -/ + moreLeancArgs : Array String := #[] + + /-- + Additional arguments to pass to `leanc` while linking the shared library. + These will come *after* the paths of package's external libraries. + -/ + moreLinkArgs : Array String := #[] + +deriving Inhabited, Repr + +namespace LeanLibConfig + +/-- Whether the given module is considered local to the library. -/ +def isLocalModule (mod : Name) (self : LeanLibConfig) : Bool := + self.roots.any (fun root => root.isPrefixOf mod) || + self.globs.any (fun glob => glob.matches mod) + +/-- Whether the given module is a buildable part of the library. -/ +def isBuildableModule (mod : Name) (self : LeanLibConfig) : Bool := + self.globs.any (fun glob => glob.matches mod) || + self.roots.any (fun root => root.isPrefixOf mod && self.globs.any (·.matches root)) diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 23fa7326ec..280d66533d 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -107,22 +107,24 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) let config := {config with dependencies := depsExt.getState env ++ config.dependencies} let scripts ← scriptAttr.ext.getState env |>.foldM (init := {}) fun m d => return m.insert d <| ← evalScriptDecl env d leanOpts - let leanLibs ← leanLibAttr.ext.getState env |>.foldM (init := {}) fun m d => + let leanLibConfigs ← leanLibAttr.ext.getState env |>.foldM (init := {}) fun m d => let eval := env.evalConstCheck LeanLibConfig leanOpts ``LeanLibConfig d return m.insert d <| ← IO.ofExcept eval.run.run - let leanExes ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d => + let leanExeConfigs ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d => let eval := env.evalConstCheck LeanExeConfig leanOpts ``LeanExeConfig d return m.insert d <| ← IO.ofExcept eval.run.run - let externLibs ← externLibAttr.ext.getState env |>.foldM (init := {}) fun m d => + let externLibConfigs ← externLibAttr.ext.getState env |>.foldM (init := {}) fun m d => let eval := env.evalConstCheck ExternLibConfig leanOpts ``ExternLibConfig d return m.insert d <| ← IO.ofExcept eval.run.run - - - if leanLibs.isEmpty && leanExes.isEmpty && config.defaultFacet ≠ .none then + if leanLibConfigs.isEmpty && leanExeConfigs.isEmpty && config.defaultFacet ≠ .none then logWarning <| "Package targets are deprecated. " ++ "Add a `lean_exe` and/or `lean_lib` default target to the package instead." let defaultTargets := defaultTargetAttr.ext.getState env |>.toArray - return {dir, config, scripts, leanLibs, leanExes, externLibs, defaultTargets} + return { + dir, config, scripts, + leanLibConfigs, leanExeConfigs, externLibConfigs, + defaultTargets + } | _ => error s!"configuration file has multiple `package` declarations" else error s!"package configuration `{configFile}` has errors" diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index a30a9f91b9..a2bcddfe47 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Build.Trace -import Lake.Config.Package -import Lake.Util.Name +import Lake.Config.LeanLib namespace Lake open Std System @@ -22,7 +21,19 @@ abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name) abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name) @[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty -/-- Locate the named module in the package (if it is local to it). -/ +/-- Locate the named module in the library (if it is buildable and local to it). -/ +def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module := + let mod := WfName.ofName mod + if self.isBuildableModule mod then some ⟨self.pkg, mod⟩ else none + +/-- Get an `Array` of the library's modules. -/ +def LeanLib.getModuleArray (self : LeanLib) : IO (Array Module) := + (·.2) <$> StateT.run (s := #[]) do + self.config.globs.forM fun glob => do + glob.forEachModuleIn self.srcDir fun mod => do + modify (·.push ⟨self.pkg, mod⟩) + +/-- Locate the named module in the package (if it is buildable and local to it). -/ def Package.findModule? (mod : Name) (self : Package) : Option Module := let mod := WfName.ofName mod if self.isBuildableModule mod then some ⟨self, mod⟩ else none diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 4ef6358a32..85228fe372 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -3,13 +3,11 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ -import Lake.Util.Name -import Lake.Util.String -import Lake.Build.TargetTypes -import Lake.Config.Glob import Lake.Config.Opaque +import Lake.Config.LeanLibConfig +import Lake.Config.LeanExeConfig +import Lake.Config.ExternLibConfig import Lake.Config.WorkspaceConfig -import Lake.Config.Targets import Lake.Config.Dependency import Lake.Config.Script @@ -31,7 +29,7 @@ def defaultBinDir : FilePath := "bin" def defaultLibDir : FilePath := "lib" /-- The default setting for a `PackageConfig`'s `oleanDir` option. -/ -def defaultOleanDir : FilePath := "lib" +def defaultOleanDir : FilePath := defaultLibDir /-- The default setting for a `PackageConfig`'s `irDir` option. -/ def defaultIrDir : FilePath := "ir" @@ -281,18 +279,18 @@ end PackageConfig structure Package where /-- The path to the package's directory. -/ dir : FilePath - /-- The package's configuration. -/ + /-- The package's user-defined configuration. -/ config : PackageConfig /-- The package's well-formed name. -/ name : WfName := WfName.ofName config.name /-- Scripts for the package. -/ scripts : NameMap Script := {} - /-- Lean library targets for the package. -/ - leanLibs : NameMap LeanLibConfig := {} - /-- Lean binary executable targets for the package. -/ - leanExes : NameMap LeanExeConfig := {} + /-- Lean library configurations for the package. -/ + leanLibConfigs : NameMap LeanLibConfig := {} + /-- Lean binary executable configurations for the package. -/ + leanExeConfigs : NameMap LeanExeConfig := {} /-- External library targets for the package. -/ - externLibs : NameMap ExternLibConfig := {} + externLibConfigs : NameMap ExternLibConfig := {} /-- The names of the package's targets to build by default (i.e., on a bare `lake build` of the package). @@ -350,21 +348,9 @@ namespace Package @[inline] def defaultFacet (self : Package) : PackageFacet := self.config.defaultFacet -/-- Get the package's library configuration with the given name. -/ -@[inline] def findLeanLib? (name : Name) (self : Package) : Option LeanLibConfig := - self.leanLibs.find? name - -/-- Get the package's executable configuration with the given name. -/ -@[inline] def findLeanExe? (name : Name) (self : Package) : Option LeanExeConfig := - self.leanExes.find? name - -/-- Get the package's external library target with the given name. -/ -@[inline] def findExternLib? (name : Name) (self : Package) : Option ExternLibConfig := - self.externLibs.find? name - /-- Get an `Array` of the package's external library targets. -/ def externLibTargets (self : Package) : Array FileTarget := - self.externLibs.fold (fun xs _ x => xs.push x.target) #[] ++ + self.externLibConfigs.fold (fun xs _ x => xs.push x.target) #[] ++ self.config.moreLibTargets /-- The package's `precompileModules` configuration. -/ @@ -403,6 +389,10 @@ def externLibTargets (self : Package) : Array FileTarget := @[inline] def moreLeancArgs (self : Package) : Array String := #["-O3", "-DNDEBUG"] ++ self.config.moreLeancArgs +/-- The package's `moreLinkArgs` configuration. -/ +@[inline] def moreLinkArgs (self : Package) : Array String := + self.config.moreLinkArgs + /-- The package's `buildDir` joined with its `irDir` configuration. -/ @[inline] def irDir (self : Package) : FilePath := self.buildDir / self.config.irDir @@ -423,18 +413,14 @@ def externLibTargets (self : Package) : Array FileTarget := @[inline] def builtinExeConfig (self : Package) : LeanExeConfig := self.config.toLeanExeConfig -/-- Get an `Array` of the package's modules. -/ -@[inline] def getModuleArray (self : Package) : IO (Array Name) := - self.builtinLibConfig.getModuleArray self.srcDir - /-- Whether the given module is considered local to the package. -/ def isLocalModule (mod : Name) (self : Package) : Bool := - self.leanLibs.any (fun _ lib => lib.isLocalModule mod) || + self.leanLibConfigs.any (fun _ lib => lib.isLocalModule mod) || self.builtinLibConfig.isLocalModule mod /-- Whether the given module is in the package (i.e., can build it). -/ def isBuildableModule (mod : Name) (self : Package) : Bool := - self.leanLibs.any (fun _ lib => lib.isBuildableModule mod) || - self.leanExes.any (fun _ exe => exe.root == mod) || + self.leanLibConfigs.any (fun _ lib => lib.isBuildableModule mod) || + self.leanExeConfigs.any (fun _ exe => exe.root == mod) || self.builtinLibConfig.isBuildableModule mod || self.config.binRoot == mod diff --git a/Lake/Config/Targets.lean b/Lake/Config/Targets.lean deleted file mode 100644 index 6af0fe41ed..0000000000 --- a/Lake/Config/Targets.lean +++ /dev/null @@ -1,173 +0,0 @@ -/- -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.Util.String -import Lake.Build.TargetTypes -import Lake.Config.Glob - -namespace Lake -open Lean System - --------------------------------------------------------------------------------- --- # Lean Library Build Configuration --------------------------------------------------------------------------------- - -/-- A Lean library's declarative configuration. -/ -structure LeanLibConfig where - /-- The name of the target. -/ - name : Name - - /-- - The root module(s) of the library. - - Submodules of these roots (e.g., `Lib.Foo` of `Lib`) are considered - part of the package. - - Defaults to a single root of the library's upper camel case name. - -/ - roots : Array Name := #[toUpperCamelCase name] - - /-- - An `Array` of module `Glob`s to build for the library. - Defaults to a `Glob.one` of each of the library's `roots`. - - Submodule globs build every source file within their directory. - Local imports of glob'ed files (i.e., fellow modules of the workspace) are - also recursively built. - -/ - globs : Array Glob := roots.map Glob.one - - /-- - The name of the library. - Used as a base for the file names of its static and dynamic binaries. - Defaults to the upper camel case name of the target. - -/ - libName := toUpperCamelCase name |>.toString (escape := false) - - /-- - Additional arguments to pass to `leanc` while linking the shared library. - These will come *after* the paths of package's external libraries. - -/ - moreLinkArgs : Array String := #[] - -deriving Inhabited, Repr - -namespace LeanLibConfig - -/-- Whether the given module is considered local to the library. -/ -def isLocalModule (mod : Name) (self : LeanLibConfig) : Bool := - self.roots.any (fun root => root.isPrefixOf mod) || - self.globs.any (fun glob => glob.matches mod) - -/-- Whether the given module is a buildable part of the library. -/ -def isBuildableModule (mod : Name) (self : LeanLibConfig) : Bool := - self.globs.any (fun glob => glob.matches mod) || - self.roots.any (fun root => root.isPrefixOf mod && self.globs.any (·.matches root)) - -/-- Get an `Array` of the library's modules. -/ -def getModuleArray (self : LeanLibConfig) (srcDir : FilePath) : IO (Array Name) := do - let mut mods := #[] - for glob in self.globs do - mods ← glob.pushModules srcDir mods - return mods - -/-- The file name of package's static library (i.e., `lib{libName}.a`) -/ -def staticLibFileName (self : LeanLibConfig) : FilePath := - s!"lib{self.libName}.a" - -/-- The file name of package's shared library. -/ -def sharedLibFileName (self : LeanLibConfig) : FilePath := - s!"{self.libName}.{sharedLibExt}" - -/-- -The arguments to pass to `leanc` when linking the shared library. -Just `moreLinkArgs`. --/ -def linkArgs (self : LeanLibConfig) : Array String := - self.moreLinkArgs - -end LeanLibConfig - --------------------------------------------------------------------------------- --- # Lean Executable Build Configuration --------------------------------------------------------------------------------- - -/-- A Lean executable's declarative configuration. -/ -structure LeanExeConfig where - /-- The name of the target. -/ - name : Name - - /-- - The root module of the binary executable. - Should include a `main` definition that will serve - as the entry point of the program. - - The root is built by recursively building its - local imports (i.e., fellow modules of the workspace). - - Defaults to the name of the target. - -/ - root : Name := name - - /-- - The name of the binary executable. - Defaults to the target name with any `.` replaced with a `-`. - -/ - exeName : String := name.toStringWithSep "-" (escape := false) - - /-- - Whether to expose symbols within the executable to the Lean interpreter. - This allows the executable to interpret Lean files (e.g., via - `Lean.Elab.runFrontend`). - - Implementation-wise, this passes `-rdynamic` to the linker when building - on non-Windows systems. - - Defaults to `false`. - -/ - supportInterpreter : Bool := false - - /-- - Additional arguments to pass to `leanc` when linking the binary executable. - These will come *after* the paths of the package's external libraries. - -/ - moreLinkArgs : Array String := #[] - -deriving Inhabited, Repr - -namespace LeanExeConfig - -/-- -The file name of binary executable -(i.e., `exeName` plus the platform's `exeExtension`). --/ -def fileName (self : LeanExeConfig) : FilePath := - FilePath.withExtension self.exeName FilePath.exeExtension - -/-- -The arguments to pass to `leanc` when linking the binary executable. -`-rdynamic` (if non-Windows and `supportInterpreter`) plus `moreLinkArgs`. --/ -def linkArgs (self : LeanExeConfig) : Array String := - if self.supportInterpreter && !Platform.isWindows then - #["-rdynamic"] ++ self.moreLinkArgs - else - self.moreLinkArgs - -end LeanExeConfig - --------------------------------------------------------------------------------- --- # External Library Build Configuration --------------------------------------------------------------------------------- - -/-- 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 --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 492a01ad4d..402575b833 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lean.Util.Paths -import Lake.Config.Opaque -import Lake.Config.WorkspaceConfig -import Lake.Config.Package -import Lake.Config.Module +import Lake.Config.LeanExe +import Lake.Config.ExternLib open System open Lean (LeanPaths) @@ -92,17 +90,17 @@ def isLocalModule (mod : Name) (self : Workspace) : Bool := def findModule? (mod : Name) (self : Workspace) : Option Module := self.packageArray.findSome? (·.findModule? mod) -/-- Get the workspace's library configuration with the given name. -/ -def findLeanLib? (name : Name) (self : Workspace) : Option (Package × LeanLibConfig) := - self.packageArray.findSome? fun pkg => pkg.findLeanLib? name <&> (pkg, ·) +/-- Try to find a Lean library in the workspace with the given name. -/ +def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib := + self.packageArray.findSome? fun pkg => pkg.findLeanLib? name -/-- Get the workspace's executable configuration with the given name. -/ -def findLeanExe? (name : Name) (self : Workspace) : Option (Package × LeanExeConfig) := - self.packageArray.findSome? fun pkg => pkg.findLeanExe? name <&> (pkg, ·) +/-- Try to find a Lean executable in the workspace with the given name. -/ +def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe := + self.packageArray.findSome? fun pkg => pkg.findLeanExe? name /-- Get the workspace's external library with the given name. -/ -def findExternLib? (name : Name) (self : Workspace) : Option (Package × ExternLibConfig) := - self.packageArray.findSome? fun pkg => pkg.findExternLib? name <&> (pkg, ·) +def findExternLib? (name : Name) (self : Workspace) : Option ExternLib := + self.packageArray.findSome? fun pkg => pkg.findExternLib? name /-- The `LEAN_PATH` of the workspace. -/ def oleanPath (self : Workspace) : SearchPath := diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean index 7bfaef7af6..62aa2222f2 100644 --- a/Lake/DSL/Targets.lean +++ b/Lake/DSL/Targets.lean @@ -5,7 +5,9 @@ Authors: Mac Malone -/ import Lake.DSL.DeclUtil import Lake.DSL.Attributes -import Lake.Config.Targets +import Lake.Config.LeanExeConfig +import Lake.Config.LeanLibConfig +import Lake.Config.ExternLibConfig namespace Lake.DSL open Lean Parser Command diff --git a/Lake/Util/String.lean b/Lake/Util/Casing.lean similarity index 100% rename from Lake/Util/String.lean rename to Lake/Util/Casing.lean diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index d251d9631d..b338b99593 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -43,7 +43,7 @@ def WellFormed.elimNum : WellFormed (Name.num p v h) → WellFormed p | numWff w rfl => w theorem eq_of_wf_quickCmpAux -(n : Name) (w : Name.WellFormed n) (n' : Name) (w' : Name.WellFormed n') +(n : Name) (w : WellFormed n) (n' : Name) (w' : WellFormed n') : Name.quickCmpAux n n' = Ordering.eq → n = n' := by revert n' induction w with @@ -84,6 +84,20 @@ theorem eq_of_wf_quickCmpAux next => contradiction +theorem wf_of_append {n n' : Name} +(w : WellFormed n) (w' : WellFormed n') : WellFormed (n.append n') := by + induction w' with + | anonymousWff => + simp [w, Name.append] + | @strWff n' p s w' h' ih => + unfold Name.mkStr at h' + simp only [Name.append, h'] + exact WellFormed.strWff ih rfl + | @numWff n' p v w' h' ih => + unfold Name.mkNum at h' + simp only [Name.append, h'] + exact WellFormed.numWff ih rfl + end Name -- # Subtype Helpers @@ -144,6 +158,11 @@ def ofName : Name → WfName | .str p s _ => mkStr (ofName p) s | .num p v _ => mkNum (ofName p) v +def ofString (str : String) : WfName := + str.splitOn "." |>.foldl (fun n p => mkStr n p.trim) anonymous + +instance : Coe String WfName := ⟨ofString⟩ + @[inline] protected def toString (escape := true) : WfName → String | ⟨n, _⟩ => n.toString escape @@ -152,6 +171,14 @@ def ofName : Name → WfName instance : ToString WfName := ⟨(·.toString)⟩ +def isPrefixOf : WfName → WfName → Bool +| ⟨n, _⟩, ⟨n', _⟩ => n.isPrefixOf n' + +def append : WfName → WfName → WfName +| ⟨n, w⟩, ⟨n', w'⟩ => ⟨n.append n', Name.wf_of_append w w'⟩ + +instance : Append WfName := ⟨append⟩ + @[inline] protected def hash : WfName → UInt64 | ⟨n, _⟩ => n.hash diff --git a/examples/init/.gitignore b/examples/init/.gitignore index cb65808d9a..66d4cb4a17 100644 --- a/examples/init/.gitignore +++ b/examples/init/.gitignore @@ -1,2 +1,2 @@ -/helloNew -/helloInit +/hello_world +/hello-world