Skip to content

Commit 0853d40

Browse files
tydeutydeu
authored
feat: lake: per-target external libraries (#7716)
This PR adds the `moreLinkObjs` and `moreLinkLibs` options for Lean packages, libraries, and executables. These serves as functional replacements for `extern_lib` and provided additional flexibility. External libraries applied to the whole package and were necessarily static. This options are configured on a per-target basis and support shared-only libraries. **Breaking change:** `precompileModules` now only loads modules of the current library individually. Modules of other libraries are loaded together via that library's shared library.
1 parent 014e5d9 commit 0853d40

40 files changed

Lines changed: 496 additions & 217 deletions

‎src/lake/Lake/Build/Actions.lean‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
55
-/
66
prelude
7+
import Lake.Config.Dynlib
78
import Lake.Util.Proc
89
import Lake.Util.NativeLib
910
import Lake.Util.IO
@@ -21,7 +22,7 @@ def compileLeanModule
2122
(leanFile : FilePath)
2223
(oleanFile? ileanFile? cFile? bcFile?: Option FilePath)
2324
(leanPath : SearchPath := []) (rootDir : FilePath := ".")
24-
(dynlibs : Array FilePath := #[]) (plugins : Array FilePath := #[])
25+
(dynlibs plugins : Array Dynlib := #[])
2526
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
2627
: LogIO Unit := do
2728
let mut args := leanArgs ++
@@ -39,9 +40,9 @@ def compileLeanModule
3940
createParentDirs bcFile
4041
args := args ++ #["-b", bcFile.toString]
4142
for dynlib in dynlibs do
42-
args := args ++ #["--load-dynlib", dynlib.toString]
43+
args := args ++ #["--load-dynlib", dynlib.path.toString]
4344
for plugin in plugins do
44-
args := args ++ #["--plugin", plugin.toString]
45+
args := args ++ #["--plugin", plugin.path.toString]
4546
args := args.push "--json"
4647
withLogErrorPos do
4748
let out ← rawProc {

‎src/lake/Lake/Build/Common.lean‎

Lines changed: 49 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Mac Malone
66
prelude
77
import Lake.Config.Monad
88
import Lake.Util.JsonObject
9+
import Lake.Build.Target.Fetch
910
import Lake.Build.Actions
1011
import Lake.Build.Job
1112

@@ -382,75 +383,77 @@ def buildStaticLib
382383
compileStaticLib libFile oFiles (← getLeanAr) thin
383384
return libFile
384385

386+
private def mkLinkObjArgs
387+
(objs : Array FilePath) (libs : Array Dynlib) : Array String
388+
:= Id.run do
389+
let mut args := #[]
390+
for obj in objs do
391+
args := args.push obj.toString
392+
for lib in libs do
393+
if let some dir := lib.dir? then
394+
args := args.push s!"-L{dir}"
395+
args := args.push s!"-l{lib.name}"
396+
return args
397+
385398
/--
386399
Build a shared library by linking the results of `linkJobs`
387400
using the Lean toolchain's C compiler.
388401
-/
402+
def buildSharedLib
403+
(libName : String) (libFile : FilePath)
404+
(linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
405+
(weakArgs traceArgs : Array String := #[]) (linker := "c++")
406+
(extraDepTrace : JobM _ := pure BuildTrace.nil)
407+
(plugin := false)
408+
: SpawnM (Job Dynlib) :=
409+
(Job.collectArray linkObjs).bindM fun objs => do
410+
(Job.collectArray linkLibs).mapM (sync := true) fun libs => do
411+
addPureTrace traceArgs
412+
addPlatformTrace -- shared libraries are platform-dependent artifacts
413+
addTrace (← extraDepTrace)
414+
buildFileUnlessUpToDate' libFile do
415+
let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs
416+
compileSharedLib libFile args linker
417+
return {name := libName, path := libFile, plugin}
418+
419+
/--
420+
Build a shared library by linking the results of `linkJobs`
421+
using `linker`.
422+
-/
389423
def buildLeanSharedLib
390-
(libFile : FilePath) (linkJobs : Array (Job FilePath))
391-
(weakArgs traceArgs : Array String := #[])
392-
: SpawnM (Job FilePath) :=
393-
(Job.collectArray linkJobs).mapM fun links => do
424+
(libName : String) (libFile : FilePath)
425+
(linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
426+
(weakArgs traceArgs : Array String := #[]) (plugin := false)
427+
: SpawnM (Job Dynlib) :=
428+
(Job.collectArray linkObjs).bindM fun objs => do
429+
(Job.collectArray linkLibs).mapM (sync := true) fun libs => do
394430
addLeanTrace
395431
addPureTrace traceArgs
396432
addPlatformTrace -- shared libraries are platform-dependent artifacts
397433
buildFileUnlessUpToDate' libFile do
398434
let lean ← getLeanInstall
399-
let args := links.map toString ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
435+
let args := mkLinkObjArgs objs libs ++
436+
weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
400437
compileSharedLib libFile args lean.cc
401-
return libFile
438+
return {name := libName, path := libFile, plugin}
402439

403440
/--
404441
Build an executable by linking the results of `linkJobs`
405442
using the Lean toolchain's linker.
406443
-/
407444
def buildLeanExe
408-
(exeFile : FilePath) (linkJobs : Array (Job FilePath))
445+
(exeFile : FilePath)
446+
(linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib))
409447
(weakArgs traceArgs : Array String := #[]) (sharedLean : Bool := false)
410448
: SpawnM (Job FilePath) :=
411-
(Job.collectArray linkJobs).mapM fun links => do
449+
(Job.collectArray linkObjs).bindM fun objs => do
450+
(Job.collectArray linkLibs).mapM (sync := true) fun libs => do
412451
addLeanTrace
413452
addPureTrace traceArgs
414453
addPlatformTrace -- executables are platform-dependent artifacts
415454
buildFileUnlessUpToDate' exeFile do
416455
let lean ← getLeanInstall
417-
let args := links.map toString ++ weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
456+
let args := mkLinkObjArgs objs libs ++
457+
weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean
418458
compileExe exeFile args lean.cc
419459
return exeFile
420-
421-
/--
422-
Build a shared library from a static library using `leanc`
423-
using the Lean toolchain's linker.
424-
-/
425-
def buildLeanSharedLibOfStatic
426-
(staticLibJob : Job FilePath)
427-
(weakArgs traceArgs : Array String := #[])
428-
: SpawnM (Job FilePath) :=
429-
staticLibJob.mapM fun staticLib => do
430-
addLeanTrace
431-
addPureTrace traceArgs
432-
addPlatformTrace -- shared libraries are platform-dependent artifacts
433-
let dynlib := staticLib.withExtension sharedLibExt
434-
buildFileUnlessUpToDate' dynlib do
435-
let lean ← getLeanInstall
436-
let baseArgs :=
437-
if System.Platform.isOSX then
438-
#[s!"-Wl,-force_load,{staticLib}"]
439-
else
440-
#["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
441-
let args := baseArgs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
442-
compileSharedLib dynlib args lean.cc
443-
return dynlib
444-
445-
/-- Construct a `Dynlib` object for a shared library target. -/
446-
def computeDynlibOfShared (sharedLibTarget : Job FilePath) : SpawnM (Job Dynlib) :=
447-
sharedLibTarget.mapM fun sharedLib => do
448-
if let some stem := sharedLib.fileStem then
449-
if Platform.isWindows then
450-
return {path := sharedLib, name := stem}
451-
else if stem.startsWith "lib" then
452-
return {path := sharedLib, name := stem.drop 3}
453-
else
454-
error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix"
455-
else
456-
error s!"shared library `{sharedLib}` has no file name"

‎src/lake/Lake/Build/Data.lean‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Mac Malone
66
prelude
77
import Lake.Build.Key
88
import Lake.Util.Family
9+
import Lake.Config.Dynlib
910

1011
open Lean
1112
namespace Lake
@@ -28,7 +29,7 @@ class DataKind (α : Type u) where
2829
/-- The name which describes `α`. -/
2930
name : Name
3031
/-- Proof that `α` is the data type described by `name`. -/
31-
wf : α = DataType name
32+
wf : ¬ name.isAnonymous ∧ α = DataType name
3233

3334
/--
3435
Tries to synthesize a `Name` descriptor of a data type.
@@ -54,7 +55,7 @@ theorem OptDataKind.eq_data_type
5455

5556
instance [DataKind α] : OptDataKind α where
5657
name := DataKind.name α
57-
wf _ := DataKind.wf
58+
wf _ := DataKind.wf.2
5859

5960
instance : CoeOut (OptDataKind α) Lean.Name := ⟨(·.name)⟩
6061
instance : ToString (OptDataKind α) := ⟨(·.name.toString)⟩
@@ -177,10 +178,13 @@ scoped macro (name := dataTypeDecl)
177178
: command => do
178179
let fam := mkCIdentFrom (← getRef) ``DataType
179180
let kindName := Name.quoteFrom kind kind.getId
180-
let id := mkIdentFrom kind (canonical := true) <|
181-
kind.getId.modifyBase (kind.getId ++ ·)
182-
`($[$doc?]? family_def $id : $fam $kindName := $ty
183-
instance : DataKind $ty := ⟨$kindName, by simp⟩)
181+
`($[$doc?]? family_def $kind : $fam $kindName := $ty
182+
instance : DataKind $ty := ⟨$kindName, by simp [Name.isAnonymous]⟩)
183+
184+
data_type unit : Unit
185+
data_type bool : Bool
186+
data_type file_path : System.FilePath
187+
data_type dynlib : Dynlib
184188

185189
/-- Internal macro for declaring new facet within Lake. -/
186190
scoped macro (name := builtinFacetCommand)

‎src/lake/Lake/Build/Executable.lean‎

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,17 +20,26 @@ def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) :=
2020
so that errors in the import block of transitive imports will not kill this
2121
job before the root is built.
2222
-/
23-
let mut linkJobs := #[]
24-
for facet in self.root.nativeFacets self.supportInterpreter do
25-
linkJobs := linkJobs.push <| ← facet.fetch self.root
23+
let mut objJobs := #[]
24+
let mut libJobs := #[]
25+
let shouldExport := self.supportInterpreter
26+
for facet in self.root.nativeFacets shouldExport do
27+
objJobs := objJobs.push <| ← facet.fetch self.root
2628
let imports ← (← self.root.transImports.fetch).await
2729
for mod in imports do
28-
for facet in mod.nativeFacets self.supportInterpreter do
29-
linkJobs := linkJobs.push <| ← facet.fetch mod
30+
for facet in mod.nativeFacets shouldExport do
31+
objJobs := objJobs.push <| ← facet.fetch mod
32+
let libs := imports.foldl (·.insert ·.lib) OrdHashSet.empty |>.toArray
33+
for lib in libs do
34+
for link in lib.moreLinkObjs do
35+
objJobs := objJobs.push <| ← link.fetchIn lib.pkg
36+
for link in lib.moreLinkLibs do
37+
libJobs := libJobs.push <| ← link.fetchIn lib.pkg
3038
let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg
31-
for dep in deps do for lib in dep.externLibs do
32-
linkJobs := linkJobs.push <| ← lib.static.fetch
33-
buildLeanExe self.file linkJobs self.weakLinkArgs self.linkArgs self.sharedLean
39+
for dep in deps do
40+
for lib in dep.externLibs do
41+
objJobs := objJobs.push <| ← lib.static.fetch
42+
buildLeanExe self.file objJobs libJobs self.weakLinkArgs self.linkArgs self.sharedLean
3443

3544
/-- The facet configuration for the builtin `LeanExe.exeFacet`. -/
3645
def LeanExe.exeFacetConfig : LeanExeFacetConfig exeFacet :=

‎src/lake/Lake/Build/ExternLib.lean‎

Lines changed: 38 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ import Lake.Build.Common
1010
Build function definitions for external libraries.
1111
-/
1212

13-
open System (FilePath)
13+
open System
1414

1515
namespace Lake
1616

@@ -22,6 +22,30 @@ def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
2222
def ExternLib.staticFacetConfig : ExternLibFacetConfig staticFacet :=
2323
mkFacetJobConfig recBuildStatic
2424

25+
/--
26+
Build a shared library from a static library using `leanc`
27+
using the Lean toolchain's linker.
28+
-/
29+
def buildLeanSharedLibOfStatic
30+
(staticLibJob : Job FilePath)
31+
(weakArgs traceArgs : Array String := #[])
32+
: SpawnM (Job FilePath) :=
33+
staticLibJob.mapM fun staticLib => do
34+
addLeanTrace
35+
addPureTrace traceArgs
36+
addPlatformTrace -- shared libraries are platform-dependent artifacts
37+
let dynlib := staticLib.withExtension sharedLibExt
38+
buildFileUnlessUpToDate' dynlib do
39+
let lean ← getLeanInstall
40+
let baseArgs :=
41+
if System.Platform.isOSX then
42+
#[s!"-Wl,-force_load,{staticLib}"]
43+
else
44+
#["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
45+
let args := baseArgs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
46+
compileSharedLib dynlib args lean.cc
47+
return dynlib
48+
2549
def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
2650
withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
2751
buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs
@@ -30,6 +54,19 @@ def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
3054
def ExternLib.sharedFacetConfig : ExternLibFacetConfig sharedFacet :=
3155
mkFacetJobConfig recBuildShared
3256

57+
/-- Construct a `Dynlib` object for a shared library target. -/
58+
def computeDynlibOfShared (sharedLibTarget : Job FilePath) : SpawnM (Job Dynlib) :=
59+
sharedLibTarget.mapM fun sharedLib => do
60+
if let some stem := sharedLib.fileStem then
61+
if Platform.isWindows then
62+
return {path := sharedLib, name := stem}
63+
else if stem.startsWith "lib" then
64+
return {path := sharedLib, name := stem.drop 3}
65+
else
66+
error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix"
67+
else
68+
error s!"shared library `{sharedLib}` has no file name"
69+
3370
def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
3471
withRegisterJob s!"{lib.staticTargetName.toString}:dynlib" do
3572
computeDynlibOfShared (← lib.shared.fetch)

‎src/lake/Lake/Build/Facets.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,8 @@ open Lean hiding SearchPath
2323
namespace Lake
2424

2525
structure ModuleDeps where
26-
dynlibs : Array FilePath := #[]
27-
plugins : Array FilePath := #[]
26+
dynlibs : Array Dynlib := #[]
27+
plugins : Array Dynlib := #[]
2828
deriving Inhabited, Repr
2929

3030
/-! ## Module Facets -/
@@ -168,7 +168,7 @@ much better for distribution.
168168
builtin_facet staticExportFacet @ static.export : LeanLib => FilePath
169169

170170
/-- A Lean library's shared artifact. -/
171-
builtin_facet shared : LeanLib => FilePath
171+
builtin_facet shared : LeanLib => Dynlib
172172

173173
/-- A Lean library's `extraDepTargets` mixed with its package's. -/
174174
builtin_facet extraDep : LeanLib => Unit

‎src/lake/Lake/Build/Imports.lean‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -23,25 +23,22 @@ def buildImportsAndDeps
2323
(leanFile : FilePath) (imports : Array Module)
2424
: FetchM (Job ModuleDeps) := do
2525
withRegisterJob s!"setup ({leanFile})" do
26+
let root ← getRootPackage
2627
if imports.isEmpty then
2728
-- build the package's (and its dependencies') `extraDepTarget`
28-
(← getRootPackage).extraDep.fetch <&> (·.map fun _ => {})
29+
root.extraDep.fetch <&> (·.map fun _ => {})
2930
else
3031
-- build local imports from list
3132
let modJob := Job.mixArray <| ← imports.mapM (·.olean.fetch)
3233
let precompileImports ← (← computePrecompileImportsAux leanFile imports).await
3334
let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
3435
let externLibsJob ← fetchExternLibs pkgs
35-
let modLibsJob ← Job.collectArray <$>
36-
precompileImports.mapM (·.dynlib.fetch)
37-
let dynlibsJob ← (← getRootPackage).dynlibs.fetch
38-
let pluginsJob ← (← getRootPackage).plugins.fetch
36+
let impLibsJob ← fetchImportLibs imports
37+
let dynlibsJob ← root.dynlibs.fetchIn root
38+
let pluginsJob ← root.plugins.fetchIn root
3939
modJob.bindM fun _ =>
40-
modLibsJob.bindM fun modLibs =>
40+
impLibsJob.bindM fun impLibs =>
4141
dynlibsJob.bindM fun dynlibs =>
4242
pluginsJob.bindM fun plugins =>
4343
externLibsJob.mapM fun externLibs => do
44-
-- NOTE: Lean wants the external library symbols before module symbols
45-
let dynlibs := (externLibs ++ dynlibs).map (·.path)
46-
let plugins := (modLibs ++ plugins).map (·.path)
47-
return {dynlibs, plugins}
44+
return computeModuleDeps impLibs externLibs dynlibs plugins

‎src/lake/Lake/Build/InputFile.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ namespace Lake
1919

2020
private def InputFile.recFetch (t : InputFile) : FetchM (Job FilePath) :=
2121
withRegisterJob s!"{t.name}" do
22-
inputFile t.config.path t.config.text
22+
inputFile t.path t.text
2323

2424
/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
2525
def InputFile.defaultFacetConfig : KFacetConfig InputFile.facetKind defaultFacet :=
@@ -37,7 +37,7 @@ def InputFile.initFacetConfigs : DNameMap (KFacetConfig InputFile.facetKind) :=
3737

3838
private def InputDir.recFetch (t : InputDir) : FetchM (Job (Array FilePath)) :=
3939
withRegisterJob s!"{t.name}" do
40-
inputDir t.config.path t.config.text t.config.filter.matches
40+
inputDir t.path t.text t.filter
4141

4242
/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
4343
def InputDir.defaultFacetConfig : KFacetConfig InputDir.facetKind defaultFacet :=

‎src/lake/Lake/Build/Job/Register.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Preserves information that downstream jobs want to depend on while resetting
2424
job-local information that should not be inherited by downstream jobs.
2525
-/
2626
def Job.renew (self : Job α) : Job α :=
27+
have : OptDataKind α := self.kind
2728
self.mapResult (sync := true) fun
2829
| .ok a s => .ok a s.renew
2930
| .error _ s => .error 0 s.renew

‎src/lake/Lake/Build/Key.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,7 @@ def PartialBuildKey.toString : (self : PartialBuildKey) → String
9696
| .facet t f => if f.isAnonymous then toString t else s!"{toString t}:{f}"
9797

9898
instance : ToString PartialBuildKey := ⟨PartialBuildKey.toString⟩
99+
instance : Repr PartialBuildKey := inferInstanceAs (Repr BuildKey)
99100

100101
namespace BuildKey
101102

0 commit comments

Comments
 (0)