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

fix: use full path when loading dynlibs in the server

Browse source 
closes leanprover/lake#146
This commit is contained in:
tydeu 2023-01-11 16:17:08 -05:00
parent 8c793eaae5
commit 4f505cd056
2 changed files with 15 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
Lake/Build/Imports.lean
View file

@ -30,7 +30,7 @@ the build jobs of their precompiled modules and the build jobs of said modules'
external libraries.
-/
def recBuildImports (imports : Array Module)
: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob FilePath)) := do
: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do
let mut modJobs := #[]
let mut precompileImports := OrdModuleSet.empty
for mod in imports do
@ -40,7 +40,7 @@ def recBuildImports (imports : Array Module)
precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch)
modJobs := modJobs.push <| ← mod.leanBin.fetch
let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch))
let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch)
return (modJobs, precompileJobs, externJobs)
@ -64,7 +64,7 @@ def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do
let (modJobs, precompileJobs, externLibJobs) ←
recBuildImports mods |>.run.run
modJobs.forM (·.await)
let dynlibs ← precompileJobs.mapM (·.await <&> (·.path))
let externLibs ← externLibJobs.mapM (·.await)
let modLibs ← precompileJobs.mapM (·.await <&> (·.path))
let externLibs ← externLibJobs.mapM (·.await <&> (·.path))
-- NOTE: Lean wants the external library symbols before module symbols
return externLibs ++ dynlibs
return externLibs ++ modLibs

18
Lake/Build/Module.lean
View file

@ -131,7 +131,7 @@ def Module.recBuildLeanCore (mod : Module)
let modJobs ← precompileImports.mapM (·.dynlib.fetch)
let pkgs := precompileImports.foldl (·.insert ·.pkg)
OrdPackageSet.empty |>.insert mod.pkg |>.toArray
let (externJobs, libDirs) ← recBuildExternDynlibs pkgs
let (externJobs, _libDirs) ← recBuildExternDynlibs pkgs
let importJob ← BuildJob.mixArray <| ← imports.mapM (·.leanBin.fetch)
let externDynlibsJob ← BuildJob.collectArray externJobs
let modDynlibsJob ← BuildJob.collectArray modJobs
@ -143,13 +143,15 @@ def Module.recBuildLeanCore (mod : Module)
modDynlibsJob.bindAsync fun modDynlibs modTrace => do
externDynlibsJob.bindSync fun externDynlibs externTrace => do
let depTrace := importTrace.mix <| modTrace.mix externTrace
let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList
-- NOTE: Lean wants the external library symbols before module symbols
-- NOTE: Unix requires the full file name of the dynlib (Windows doesn't care)
let dynlibs :=
externDynlibs.map (.mk <| nameToSharedLib ·.name) ++
modDynlibs.map (.mk <| nameToSharedLib ·.name)
let trace ← mod.buildUnlessUpToDate dynlibPath dynlibs depTrace leanOnly
/-
Requirements:
* Lean wants the external library symbols before module symbols.
* Unix requires the file extension of the dynlib.
* For some reason, building from the Lean server requires full paths.
Everything else loads fine with just the augmented library path.
-/
let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path)
let trace ← mod.buildUnlessUpToDate ∅ dynlibs depTrace leanOnly
return ((), trace)
/-- Possible artifacts of the `lean` command. -/