fix: include libleanshared in Lean trace

closes leanprover/lake#26

Lake/Build/Monad.lean

@@ -9,6 +9,10 @@ import Lake.Build.MonadBasic
 open System
 namespace Lake
 
+def mkBuildContext (pkg : Package) (leanInstall : LeanInstall) (lakeInstall : LakeInstall) : IO BuildContext := do
+  let leanTrace := mixTrace (← computeTrace leanInstall.lean) (← computeTrace leanInstall.sharedLib)
+  return {package := pkg, leanInstall, lakeInstall, leanTrace}
+
 deriving instance Inhabited for BuildContext
 
 def BuildM.adaptPackage (pkg : Package) (self : BuildM α) : BuildM α :=

Lake/Build/MonadBasic.lean

@@ -13,10 +13,10 @@ open System
 namespace Lake
 
 structure BuildContext where
-  leanTrace : BuildTrace
+  package : OpaquePackage
   leanInstall : LeanInstall
   lakeInstall : LakeInstall
-  package : OpaquePackage
+  leanTrace : BuildTrace
 
 abbrev BuildM :=
   ReaderT BuildContext BuildCoreM

Lake/CLI/Main.lean

@@ -135,8 +135,8 @@ def getInstall : CliM (LeanInstall × LakeInstall) := do
 /-- Perform the given build action using information from CLI. -/
 def runBuildM (pkg : Package) (x : BuildM α) : CliM α := do
   let (leanInstall, lakeInstall) ← getInstall
-  let leanTrace ← computeTrace leanInstall.lean
-  x.run LogMethods.io {leanTrace, leanInstall, lakeInstall, package := pkg}
+  let ctx ← mkBuildContext pkg leanInstall lakeInstall
+  x.run LogMethods.io ctx
 
 /-- Variant of `runBuildM` that discards the build monad's output. -/
 def runBuildM_  (pkg : Package) (x : BuildM α) : CliM PUnit :=
@@ -249,10 +249,8 @@ def printPaths (imports : List String := []) : CliM PUnit := do
   let configFile := (← getRootDir) / (← getConfigFile)
   if (← configFile.pathExists) then
     let pkg ← loadPkg (← getSubArgs)
-    let leanTrace ← computeTrace leanInstall.lean
-    let pkgs ← pkg.buildImportsAndDeps imports |>.run LogMethods.eio {
-      leanTrace, leanInstall, lakeInstall, package := pkg
-    }
+    let ctx ← mkBuildContext pkg leanInstall lakeInstall
+    let pkgs ← pkg.buildImportsAndDeps imports |>.run LogMethods.eio ctx
     IO.println <| Json.compress <| toJson {
       oleanPath := pkgs.map (·.oleanDir),
       srcPath := pkgs.map (·.srcDir) : LeanPaths

Lake/Config/InstallPath.lean

@@ -6,6 +6,12 @@ Authors: Mac Malone
 open System
 namespace Lake
 
+/-- The shared library file extension for the `Platform`. -/
+def sharedLibExt : String :=
+  if Platform.isWindows then "dll"
+  else if Platform.isOSX  then "dylib"
+  else "so"
+
 /-- Path information about the local Lean installation. -/
 structure LeanInstall where
   home : FilePath
@@ -15,6 +21,7 @@ structure LeanInstall where
   includeDir := home / "include"
   lean := binDir / "lean" |>.withExtension FilePath.exeExtension
   leanc := binDir / "leanc" |>.withExtension FilePath.exeExtension
+  sharedLib := (if Platform.isWindows then binDir else libDir) / "libleanshared" |>.withExtension sharedLibExt
   deriving Inhabited, Repr
 
 /-- Path information about the local Lake installation. -/

Lake/Config/Package.lean

@@ -44,12 +44,6 @@ def defaultBinRoot : Name := `Main
 -- # Auxiliary Definitions and Helpers
 --------------------------------------------------------------------------------
 
-/-- The shared library file extension for the `Platform`. -/
-def sharedLibExt : String :=
-  if Platform.isWindows then "dll"
-  else if Platform.isOSX  then "dynlib"
-  else "so"
-
 /--
   The `src` of a `Dependency`.