From e5782adeff57418184a1588bcf83415456fb978d Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 10 Jun 2022 12:08:58 -0400 Subject: [PATCH] feat: replace `moreLibTargets` w/ new `extern_lib` syntax --- Lake/Build/Binary.lean | 7 ++---- Lake/Build/Package.lean | 2 +- Lake/CLI/Build.lean | 40 +++++++++++++++++++++------------- Lake/CLI/Error.lean | 2 ++ Lake/Config/Load.lean | 17 ++++++++++----- Lake/Config/Package.lean | 40 +++++++++++++++++++++------------- Lake/Config/Targets.lean | 22 ++++++++++++++----- Lake/Config/Workspace.lean | 12 ++++++---- Lake/DSL/Attributes.lean | 9 +++++--- Lake/DSL/Targets.lean | 16 ++++++++++++++ examples/ffi/lib/lakefile.lean | 31 ++++++++++++-------------- 11 files changed, 128 insertions(+), 70 deletions(-) diff --git a/Lake/Build/Binary.lean b/Lake/Build/Binary.lean index af3966b282..4c4a6434b1 100644 --- a/Lake/Build/Binary.lean +++ b/Lake/Build/Binary.lean @@ -44,9 +44,6 @@ def Package.mkStaticLibTarget (self : Package) (lib : LeanLibConfig) : FileTarge protected def Package.staticLibTarget (self : Package) : FileTarget := self.mkStaticLibTarget self.builtinLibConfig -def Package.staticLibTargets (self : Package) : Array FileTarget := - #[self.staticLibTarget] ++ self.moreLibTargets - -- # Build Package Shared Lib def Package.linkTargetsOf @@ -54,13 +51,13 @@ def Package.linkTargetsOf let collect dep recurse := do let pkg := (← getPackageByName? dep.name).get! pkg.dependencies.forM fun dep => discard <| recurse dep - return pkg.oFileTargetsOf targetMap ++ pkg.moreLibTargets + return pkg.oFileTargetsOf targetMap ++ pkg.externLibTargets let ⟨x, map⟩ ← RBTopT.run <| self.dependencies.forM fun dep => discard <| buildRBTop (cmp := Name.quickCmp) collect Dependency.name dep match x with | Except.ok _ => let ts := map.fold (fun acc _ vs => acc ++ vs) #[] - return self.oFileTargetsOf targetMap ++ self.moreLibTargets ++ ts + return self.oFileTargetsOf targetMap ++ self.externLibTargets ++ ts | Except.error _ => panic! "dependency cycle emerged after resolution" def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget := diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean index b357b755f1..9fd59b2ac1 100644 --- a/Lake/Build/Package.lean +++ b/Lake/Build/Package.lean @@ -102,7 +102,7 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build else -- build local imports from list let infos := (← getWorkspace).processImportList imports - if self.exes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then + if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then let build := recBuildModuleOleanTargetWithLocalImports depTarget let targets ← buildModuleArray infos build targets.forM (·.buildOpaque) diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index 7f08c7975d..1bde91f853 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -56,9 +56,14 @@ def resolveExeTarget (pkg : Package) (exe : LeanExeConfig) (facet : String) : Ex throw <| CliError.unknownFacet "executable" facet def resolveTargetInPackage (pkg : Package) (target : Name) (facet : String) : Except CliError OpaqueTarget := - if let some exe := pkg.findExe? target then + if let some exe := pkg.findLeanExe? target then resolveExeTarget pkg exe facet - else if let some lib := pkg.findLib? target then + 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 else if pkg.hasModule target then resolveModuleTarget pkg target facet @@ -86,6 +91,23 @@ def resolvePackageTarget (pkg : Package) (facet : String) : Except CliError Opaq else throw <| CliError.unknownFacet "package" facet +def resolveTargetInWorkspace (ws : Workspace) (spec : String) (facet : String) : Except CliError OpaqueTarget := + if let some (pkg, exe) := ws.findLeanExe? spec then + resolveExeTarget pkg exe facet + else if let some (_, lib) := ws.findExternLib? spec then + if facet.isEmpty then + return lib.target.withoutInfo + else + throw <| CliError.invalidFacet spec facet + else if let some (pkg, lib) := ws.findLeanLib? spec then + resolveLibTarget pkg lib facet + else if let some pkg := ws.packageByName? spec then + resolvePackageTarget pkg facet + else if let some pkg := ws.packageForModule? spec then + resolveModuleTarget pkg spec facet + else + throw <| CliError.unknownTarget spec + def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Except CliError OpaqueTarget := do match spec.splitOn "/" with | [spec] => @@ -101,16 +123,7 @@ def resolveTargetBaseSpec (ws : Workspace) (spec : String) (facet := "") : Excep else throw <| CliError.unknownModule mod else - if let some (pkg, exe) := ws.findExe? spec then - resolveExeTarget pkg exe facet - else if let some (pkg, lib) := ws.findLib? spec then - resolveLibTarget pkg lib facet - else if let some pkg := ws.packageByName? spec then - resolvePackageTarget pkg facet - else if let some pkg := ws.packageForModule? spec then - resolveModuleTarget pkg spec facet - else - throw <| CliError.unknownTarget spec + resolveTargetInWorkspace ws spec facet | [pkgSpec, targetSpec] => let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec let pkg ← parsePackageSpec ws pkgSpec @@ -130,6 +143,3 @@ def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError OpaqueTar resolveTargetBaseSpec ws rootSpec facet | _ => throw <| CliError.invalidTargetSpec spec ':' - -def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (List OpaqueTarget) := - specs.mapM <| parseTargetSpec ws diff --git a/Lake/CLI/Error.lean b/Lake/CLI/Error.lean index 947bf44f57..46c01857c8 100644 --- a/Lake/CLI/Error.lean +++ b/Lake/CLI/Error.lean @@ -24,6 +24,7 @@ inductive CliError | missingModule (pkg : Name) (mod : Name) | missingTarget (pkg : Name) (spec : String) | invalidTargetSpec (spec : String) (tooMany : Char) +| invalidFacet (target : Name) (facet : String) /- Script CLI Error -/ | unknownScript (script : String) | missingScriptDoc (script : String) @@ -51,6 +52,7 @@ def toString : CliError → String | missingModule pkg mod => s!"package '{pkg.toString false}' has no module '{mod.toString false}'" | missingTarget pkg spec => s!"package '{pkg.toString false}' has no target '{spec}'" | invalidTargetSpec s c => s!"invalid script spec '{s}' (too many '{c}')" +| invalidFacet t f => s!"invalid facet `{f}`; target {t.toString false} has no facets" | unknownScript s => s!"unknown script {s}" | missingScriptDoc s => s!"no documentation provided for `{s}`" | invalidScriptSpec s => s!"invalid script spec '{s}' (too many '/')" diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean index 45e8ef3ffe..939edd9640 100644 --- a/Lake/Config/Load.lean +++ b/Lake/Config/Load.lean @@ -97,7 +97,9 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := []) | [pkgDeclName] => let config ← evalPackageDecl env pkgDeclName dir args leanOpts unless config.dependencies.isEmpty do - logWarning "Syntax for package dependencies has changed. Use the new require syntax." + logWarning "Syntax for package dependencies has changed. Use the new `require` syntax." + unless config.moreLibTargets.isEmpty do + logWarning "Syntax for `moreLibTargets` has changed. Use the new `extern_lib` syntax." if config.defaultFacet = PackageFacet.bin then logWarning "The `bin` package facet has been deprecated in favor of `exe`." if config.defaultFacet = PackageFacet.oleans then @@ -105,17 +107,22 @@ 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 libs ← leanLibAttr.ext.getState env |>.foldM (init := {}) fun m d => + let leanLibs ← 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 exes ← leanExeAttr.ext.getState env |>.foldM (init := {}) fun m d => + let leanExes ← 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 - if libs.isEmpty && exes.isEmpty && !config.defaultFacet = .none then + let externLibs ← 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 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, libs, exes, defaultTargets} + return {dir, config, scripts, leanLibs, leanExes, externLibs, defaultTargets} | _ => error s!"configuration file has multiple `package` declarations" else error s!"package configuration `{configFile}` has errors" diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 0c7f61dc33..04bf2a5917 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -261,10 +261,12 @@ structure Package where config : PackageConfig /-- Scripts for the package. -/ scripts : NameMap Script := {} - /-- Additional Lean library targets for the package. -/ - libs : NameMap LeanLibConfig := {} - /-- Additional Lean binary executable targets for the package. -/ - exes : NameMap LeanExeConfig := {} + /-- Lean library targets for the package. -/ + leanLibs : NameMap LeanLibConfig := {} + /-- Lean binary executable targets for the package. -/ + leanExes : NameMap LeanExeConfig := {} + /-- External library targets for the package. -/ + externLibs : NameMap ExternLibConfig := {} /-- The names of the package's targets to build by default (i.e., on a bare `lake build` of the package). @@ -323,13 +325,25 @@ def extraDepTarget (self : Package) : OpaqueTarget := def defaultFacet (self : Package) : PackageFacet := self.config.defaultFacet +/-- The package's `moreLibTargets` configuration. -/ +def moreLibTargets (self : Package) : Array FileTarget := + self.config.moreLibTargets + /-- Get the package's library configuration with the given name. -/ -def findLib? (self : Package) (name : Name) : Option LeanLibConfig := - self.libs.find? name +def findLeanLib? (name : Name) (self : Package) : Option LeanLibConfig := + self.leanLibs.find? name /-- Get the package's executable configuration with the given name. -/ -def findExe? (self : Package) (name : Name) : Option LeanExeConfig := - self.exes.find? name +def findLeanExe? (name : Name) (self : Package) : Option LeanExeConfig := + self.leanExes.find? name + +/-- Get the package's external library target with the given name. -/ +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.moreLibTargets /-- The package's `moreServerArgs` configuration. -/ def moreServerArgs (self : Package) : Array String := @@ -403,10 +417,6 @@ def libDir (self : Package) : FilePath := def binDir (self : Package) : FilePath := self.buildDir / self.config.binDir -/-- The package's `moreLibTargets` configuration. -/ -def moreLibTargets (self : Package) : Array FileTarget := - self.config.moreLibTargets - /-- The library configuration built into the package configuration. -/ def builtinLibConfig (self : Package) : LeanLibConfig := self.config.toLeanLibConfig @@ -421,12 +431,12 @@ def getModuleArray (self : Package) : IO (Array Name) := /-- Whether the given module is considered local to the package. -/ def isLocalModule (mod : Name) (self : Package) : Bool := - self.libs.any (fun _ lib => lib.isLocalModule mod) || + self.leanLibs.any (fun _ lib => lib.isLocalModule mod) || self.builtinLibConfig.isLocalModule mod /-- Whether the given module is in the package (i.e., can build it). -/ def hasModule (mod : Name) (self : Package) : Bool := - self.libs.any (fun _ lib => lib.hasModule mod) || - self.exes.any (fun _ exe => exe.root == mod) || + self.leanLibs.any (fun _ lib => lib.hasModule mod) || + self.leanExes.any (fun _ exe => exe.root == mod) || self.builtinLibConfig.hasModule mod || self.config.binRoot == mod diff --git a/Lake/Config/Targets.lean b/Lake/Config/Targets.lean index 70bb87a3e8..c8ff6474ad 100644 --- a/Lake/Config/Targets.lean +++ b/Lake/Config/Targets.lean @@ -46,10 +46,9 @@ structure LeanLibConfig where -/ libName := toUpperCamelCase name |>.toString (escape := false) - /-- + /-- Additional arguments to pass to `leanc` while linking the shared library. - These will come *after* the paths of libraries built with the package's - `moreLibTargets`. + These will come *after* the paths of package's external libraries. -/ moreLinkArgs : Array String := #[] @@ -132,8 +131,7 @@ structure LeanExeConfig where /-- Additional arguments to pass to `leanc` when linking the binary executable. - These will come *after* the paths of libraries built with the package's - `moreLibTargets`. + These will come *after* the paths of the package's external libraries. -/ moreLinkArgs : Array String := #[] @@ -159,3 +157,17 @@ def linkArgs (self : LeanExeConfig) : Array String := 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 a7795aea21..02c542e88e 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -96,12 +96,16 @@ def packageForModule? (mod : Name) (self : Workspace) : Option Package := self.findPackage? (·.isLocalModule mod) /-- Get the workspace's library configuration with the given name. -/ -def findLib? (name : Name) (self : Workspace) : Option (Package × LeanLibConfig) := - self.packageArray.findSome? fun pkg => pkg.findLib? name <&> (pkg, ·) +def findLeanLib? (name : Name) (self : Workspace) : Option (Package × LeanLibConfig) := + self.packageArray.findSome? fun pkg => pkg.findLeanLib? name <&> (pkg, ·) /-- Get the workspace's executable configuration with the given name. -/ -def findExe? (name : Name) (self : Workspace) : Option (Package × LeanExeConfig) := - self.packageArray.findSome? fun pkg => pkg.findExe? name <&> (pkg, ·) +def findLeanExe? (name : Name) (self : Workspace) : Option (Package × LeanExeConfig) := + self.packageArray.findSome? fun pkg => pkg.findLeanExe? name <&> (pkg, ·) + +/-- 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, ·) /-- The `LEAN_PATH` of the workspace. -/ def oleanPath (self : Workspace) : SearchPath := diff --git a/Lake/DSL/Attributes.lean b/Lake/DSL/Attributes.lean index ecc8ada5df..b4e9633629 100644 --- a/Lake/DSL/Attributes.lean +++ b/Lake/DSL/Attributes.lean @@ -9,16 +9,16 @@ open Lean namespace Lake initialize packageAttr : TagAttribute ← - registerTagAttribute `package "mark a definition as a Lake package declaration" + registerTagAttribute `package "mark a definition as a Lake package configuration" initialize scriptAttr : TagAttribute ← registerTagAttribute `script "mark a definition as a Lake script" initialize leanLibAttr : TagAttribute ← - registerTagAttribute `leanLib "mark a definition as a Lake Lean library target declaration" + registerTagAttribute `leanLib "mark a definition as a Lake Lean library target configuration" initialize leanExeAttr : TagAttribute ← - registerTagAttribute `leanExe "mark a definition as a Lake Lean executable target declaration" + registerTagAttribute `leanExe "mark a definition as a Lake Lean executable target configuration" initialize defaultTargetAttr : TagAttribute ← registerTagAttribute `defaultTarget "mark a Lake target as the package's default" @@ -27,3 +27,6 @@ initialize defaultTargetAttr : TagAttribute ← leanLibAttr.hasTag env name || leanExeAttr.hasTag env name unless valid do throwError "attribute `defaultTarget` can only be used on a target (e.g., `lean_lib`, `lean_exe`)" + +initialize externLibAttr : TagAttribute ← + registerTagAttribute `externLib "mark a definition as a Lake external library target" diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean index 4ecaa95591..bc042ebf1d 100644 --- a/Lake/DSL/Targets.lean +++ b/Lake/DSL/Targets.lean @@ -52,3 +52,19 @@ doc?:optional(docComment) attrs?:optional(Term.attributes) let ty := mkCIdentFrom (← getRef) ``LeanExeConfig let attrs := #[attr] ++ expandAttrs attrs? mkTargetDecl doc? attrs ty spec + +syntax externLibDeclSpec := + ident optional(Term.typeSpec) declValSimple + +/-- Define a new external library target for the package. -/ +scoped macro (name := externLibDecl) +doc?:optional(docComment) attrs?:optional(Term.attributes) +"extern_lib " spec:externLibDeclSpec : command => do + match spec with + | `(externLibDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) => + let attr ← `(Term.attrInstance| externLib) + let ty := ty?.getD <| mkCIdentFrom (← getRef) ``ExternLibConfig + let attrs := #[attr] ++ expandAttrs attrs? + `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := + {name := $(quote id.getId), target := $defn} $[$wds?]?) + | stx => Macro.throwErrorAt stx "ill-formed external library declaration" diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean index edd136ea3a..bab774d7d5 100644 --- a/examples/ffi/lib/lakefile.lean +++ b/examples/ffi/lib/lakefile.lean @@ -1,25 +1,8 @@ import Lake open System Lake DSL -def cDir : FilePath := "c" -def ffiSrc := cDir / "ffi.cpp" -def buildDir := defaultBuildDir - -def ffiOTarget (pkgDir : FilePath) : FileTarget := - let oFile := pkgDir / buildDir / cDir / "ffi.o" - let srcTarget := inputFileTarget <| pkgDir / ffiSrc - fileTargetWithDep oFile srcTarget fun srcFile => do - compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString] "c++" - -def cLibTarget (pkgDir : FilePath) : FileTarget := - let libFile := pkgDir / buildDir / cDir / "libffi.a" - staticLibTarget libFile #[ffiOTarget pkgDir] - package ffi { - -- customize layout srcDir := "lean" - -- specify the lib as an additional target - moreLibTargets := #[cLibTarget __dir__] } lean_lib FFI @@ -27,3 +10,17 @@ lean_lib FFI @[defaultTarget] lean_exe test { root := `Main } + +def pkgDir := __dir__ +def cSrcDir := pkgDir / "c" +def cBuildDir := pkgDir / defaultBuildDir / "c" + +def ffiOTarget : FileTarget := + let oFile := cBuildDir / "ffi.o" + let srcTarget := inputFileTarget <| cSrcDir / "ffi.cpp" + fileTargetWithDep oFile srcTarget fun srcFile => do + compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString] "c++" + +extern_lib cLib := + let libFile := cBuildDir / "libffi.a" + staticLibTarget libFile #[ffiOTarget]