feat: replace moreLibTargets w/ new extern_lib syntax
This commit is contained in:
tydeu
parent
8428ef7cd7
commit
e5782adeff
11 changed files with 128 additions and 70 deletions
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 '/')"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue