max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: link libraries in a path and platform independent way

Browse source
This commit is contained in:
tydeu 2022-06-25 19:22:41 -04:00
parent c4580839b5
commit 6812bae11a
5 changed files with 65 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Lake/Build/Actions.lean
View file

@ -12,7 +12,8 @@ def createParentDirs (path : FilePath) : IO PUnit := do
if let some dir := path.parent then IO.FS.createDirAll dir
def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
let envStr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
let envStr := String.join <| args.env.toList.filterMap fun (k, v) =>
if k == "PATH" then none else some s!"{k}={v.getD ""} " -- PATH too big
let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
logInfo <| "> " ++ envStr ++
match args.cwd with
@ -31,11 +32,16 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
logError s!"external command {args.cmd} exited with status {out.exitCode}"
failure
def getSearchPath (envVar : String) : IO SearchPath := do
match (← IO.getEnv envVar) with
| some path => pure <| SearchPath.parse path
| none => pure []
def compileLeanModule (leanFile : FilePath)
(oleanFile? ileanFile? cFile? : Option FilePath)
(oleanPath : SearchPath := []) (rootDir : FilePath := ".")
(dynlibs : Array FilePath := #[]) (leanArgs : Array String := #[])
(lean : FilePath := "lean")
(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
: BuildM PUnit := do
let mut args := leanArgs ++
#[leanFile.toString, "-R", rootDir.toString]
@ -53,7 +59,11 @@ def compileLeanModule (leanFile : FilePath)
proc {
args
cmd := lean.toString
env := #[("LEAN_PATH", oleanPath.toString)]
env := #[
("LEAN_PATH", oleanPath.toString),
("PATH", (← getSearchPath "PATH") ++ dynlibPath |>.toString), -- Windows
("LD_LIBRARY_PATH", (← getSearchPath "LD_LIBRARY_PATH") ++ dynlibPath |>.toString) -- Unix
]
}
def compileO (oFile srcFile : FilePath)

54
Lake/Build/Module1.lean
View file

@ -14,8 +14,8 @@ namespace Lake
-- # Solo Module Targets
def Module.soloTarget (mod : Module)
(dynlibs : Array FilePath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
def Module.soloTarget (mod : Module) (dynlibs : Array FilePath)
(dynlibPath : SearchPath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget :=
Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do
let argTrace : BuildTrace := pureHash mod.leanArgs
let srcTrace : BuildTrace ← computeTrace mod.leanFile
@ -25,12 +25,12 @@ def Module.soloTarget (mod : Module)
let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
unless modUpToDate && cUpToDate do
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
(← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
modTrace.writeToFile mod.cTraceFile
else
unless modUpToDate do
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
(← getOleanPath) mod.pkg.rootDir dynlibs mod.leanArgs (← getLean)
(← getOleanPath) mod.pkg.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
modTrace.writeToFile mod.traceFile
return depTrace
@ -43,8 +43,15 @@ def Module.mkOTarget (cTarget : FileTarget) (self : Module) : FileTarget :=
leanOFileTarget self.oFile cTarget self.leancArgs
@[inline]
def Module.mkDynlibTarget (linkTargets : Array FileTarget) (self : Module) : FileTarget :=
leanSharedLibTarget self.dynlib linkTargets self.linkArgs
def Module.mkDynlibTarget (self : Module) (oTarget : FileTarget)
(libDirs : Array FilePath) (libTargets : Array FileTarget) : FileTarget :=
let libsTarget : BuildTarget _ := Target.collectArray libTargets
Target.mk self.dynlib do
oTarget.bindAsync fun oFile oTrace => do
libsTarget.bindSync fun libFiles libTrace => do
buildFileUnlessUpToDate self.dynlibFile (oTrace.mix libTrace) do
let args := #[oFile.toString] ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l:{·}")
compileSharedLib self.dynlibFile args (← getLeanc)
-- # Recursive Building
@ -53,9 +60,11 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
/-- Build the dynlibs of the imports that want precompilation. -/
@[specialize] def recBuildPrecompileDynlibs (pkg : Package) (imports : Array Module)
: IndexT m (Array ActiveFileTarget × Array ActiveFileTarget) := do
: IndexT m (Array ActiveFileTarget × Array ActiveFileTarget × Array FilePath) := do
have : MonadLift BuildM m := ⟨liftM⟩
-- Build and collect precompiled imports
let mut pkgs := #[]
let mut pkgSet := PackageSet.empty
let mut pkgSet := PackageSet.empty.insert pkg
let mut modTargets := #[]
for imp in imports do
if imp.shouldPrecompile then
@ -63,11 +72,21 @@ variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
pkgSet := pkgSet.insert imp.pkg
pkgs := pkgs.push imp.pkg
modTargets := modTargets.push <| ← imp.recBuildFacet &`lean.dynlib
pkgs := pkgs.push pkg
-- Compute library directories and external library targets
let mut libDirs := #[]
let mut pkgTargets := #[]
for pkg in pkgs do
pkgTargets := pkgTargets.append <| ← pkg.recBuildFacet &`externSharedLibs
pkgTargets := pkgTargets.append <| ← pkg.recBuildFacet &`externSharedLibs
return (modTargets, pkgTargets)
libDirs := libDirs.push pkg.libDir
let externLibTargets ← pkg.recBuildFacet &`externSharedLibs
for target in externLibTargets do
if let some parent := target.info.parent then
libDirs := libDirs.push parent
if let some fileName := target.info.fileName then
pkgTargets := pkgTargets.push <| target.withInfo fileName
else
logWarning s!"external library `{target.info}` was skipped because it has no file name"
return (modTargets, pkgTargets, libDirs)
/--
Recursively build a module and its (transitive, local) imports,
@ -78,7 +97,7 @@ optionally outputting a `.c` file as well if `c` is set to `true`.
have : MonadLift BuildM m := ⟨liftM⟩
let extraDepTarget ← mod.pkg.recBuildFacet &`extraDep
let (imports, transImports) ← mod.recBuildFacet &`lean.imports
let (modTargets, pkgTargets) ← recBuildPrecompileDynlibs mod.pkg transImports
let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
-- Note: Lean wants the external library symbols before module symbols
let dynlibsTarget ← ActiveTarget.collectArray <| pkgTargets ++ modTargets
let importTarget ←
@ -90,7 +109,7 @@ optionally outputting a `.c` file as well if `c` is set to `true`.
<| ← imports.mapM (·.recBuildFacet &`lean)
let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync
<| ← dynlibsTarget.mixOpaqueAsync importTarget
let modTarget ← mod.soloTarget dynlibsTarget.info depTarget c |>.activate
let modTarget ← mod.soloTarget dynlibsTarget.info libDirs.toList depTarget c |>.activate
store (mod.mkBuildKey &`lean) modTarget
store (mod.mkBuildKey &`olean) <| modTarget.withInfo mod.oleanFile
store (mod.mkBuildKey &`ilean) <| modTarget.withInfo mod.ileanFile
@ -132,9 +151,8 @@ Recursively build the shared library of a module (e.g., for `--load-dynlib`).
@[specialize] def Module.recBuildDynLib (mod : Module)
: IndexT m ActiveFileTarget := do
have : MonadLift BuildM m := ⟨liftM⟩
let oTarget ← mod.recBuildFacet &`lean.o
let oTarget := Target.active <| ← mod.recBuildFacet &`lean.o
let (_, transImports) ← mod.recBuildFacet &`lean.imports
let (modTargets, pkgTargets) ← recBuildPrecompileDynlibs mod.pkg transImports
let linkTargets := #[oTarget] ++ modTargets ++ pkgTargets
let linkTargets := linkTargets.map Target.active
mod.mkDynlibTarget linkTargets |>.activate
let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg transImports
let libTargets := modTargets ++ pkgTargets |>.map Target.active
mod.mkDynlibTarget oTarget libDirs libTargets |>.activate

22
Lake/Config/Module.lean
View file

@ -29,29 +29,33 @@ def Package.findModule? (mod : Name) (self : Package) : Option Module :=
namespace Module
def leanFile (self : Module) : FilePath :=
@[inline] def leanFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.srcDir self.name "lean"
def oleanFile (self : Module) : FilePath :=
@[inline] def oleanFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.oleanDir self.name "olean"
def ileanFile (self : Module) : FilePath :=
@[inline] def ileanFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.oleanDir self.name "ilean"
def traceFile (self : Module) : FilePath :=
@[inline] def traceFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.oleanDir self.name "trace"
def cFile (self : Module) : FilePath :=
@[inline] def cFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.irDir self.name "c"
def cTraceFile (self : Module) : FilePath :=
@[inline] def cTraceFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.irDir self.name "c.trace"
def oFile (self : Module) : FilePath :=
@[inline] def oFile (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.irDir self.name "o"
def dynlib (self : Module) : FilePath :=
Lean.modToFilePath self.pkg.oleanDir self.name sharedLibExt
@[inline] def dynlib (self : Module) : FilePath :=
-- NOTE: file name MUST be unique on Windows
s!"{self.name}.{sharedLibExt}"
@[inline] def dynlibFile (self : Module) : FilePath :=
self.pkg.libDir / self.dynlib
@[inline] def leanArgs (self : Module) : Array String :=
self.pkg.moreLeanArgs

2
examples/ffi/lib/lakefile.lean
View file

@ -23,5 +23,5 @@ def ffiOTarget : FileTarget :=
compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString] "c++"
extern_lib cLib :=
let libFile := cBuildDir / s!"libffi.a"
let libFile := cBuildDir / s!"libleanffi.a"
staticLibTarget libFile #[ffiOTarget]

3
examples/ffi/test.sh
View file

@ -5,5 +5,4 @@ set -e
./app/build/bin/app
./lib/build/bin/test
cd app # Library loading needs this; TODO: fix this
${LAKE:-../../../build/bin/lake} build Test
${LAKE:-../../build/bin/lake} -d app build Test