From 4f505cd056897a7abb37bc6a1d6bb819ce3bc76c Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 11 Jan 2023 16:17:08 -0500
Subject: [PATCH] fix: use full path when loading dynlibs in the server

closes leanprover/lake#146
---
 Lake/Build/Imports.lean | 10 +++++-----
 Lake/Build/Module.lean  | 18 ++++++++++--------
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean
index 45d02329c5..392b162770 100644
--- a/Lake/Build/Imports.lean
+++ b/Lake/Build/Imports.lean
@@ -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
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 92151fa41e..98e3684392 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -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. -/