fix: report precompiled dynlibs to server

a feature of leanprover#47 I had hetherto missed

Lake/Build/Data.lean

@@ -25,6 +25,7 @@ opaque PackageData (facet : WfName) : Type
 /-- Type of build data associated with Lake targets (e.g., `extern_lib`). -/
 opaque TargetData (key : BuildKey) : Type
 
+
 /--
 Type of the build data associated with a key in the Lake build store.
 It is dynamic type composed of the three separate dynamic types for modules,
@@ -38,6 +39,19 @@ def BuildData (key : BuildKey) :=
   else
     TargetData key
 
+instance (k : ModuleBuildKey f)
+[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
+  eq_dynamic_type := by
+    unfold BuildData
+    simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
+
+instance (k : PackageBuildKey f)
+[t : DynamicType PackageData f α] : DynamicType BuildData k α where
+  eq_dynamic_type := by
+    unfold BuildData, BuildKey.isModuleKey
+    have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
+    simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
+
 /-- Macro for declaring new `PackageData`. -/
 scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment)
 "package_data " id:ident " : " ty:term : command => do

Lake/Build/Executable.lean

@@ -5,9 +5,6 @@ Authors: Mac Malone
 -/
 import Lake.Build.Library
 
-open Std System
-open Lean (Name NameMap)
-
 namespace Lake
 
 -- # Build Package Executable

Lake/Build/Imports.lean

@@ -10,6 +10,7 @@ import Lake.Config.Workspace
 Definitions to support `lake print-paths` builds.
 -/
 
+open System
 namespace Lake
 
 /--
@@ -25,22 +26,38 @@ def Workspace.processImportList
   return localImports
 
 /--
-Build the workspace-local modules of list of imports.
+Whether the package is "lean-only".
+That is, whether it has no need to build native files (e.g. `.c`).
+A package is considered lean-only if the package does not include any executable
+targets and is not precompiled.
+-/
+def Package.isLeanOnly (self : Package): Bool :=
+  self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans
+
+/--
+Builds the workspace-local modules of list of imports.
+Used by `lake print-paths` to build modules for the Lean server.
+Returns the set of module dynlibs built (so they can be loaded by the server).
 
-Build only module `.olean` and `.ilean` files if
-the default package build does not include any binary targets
-Otherwise, also build `.c` files.
+Builds only module `.olean` and `.ilean` files if the package is "lean-only"
+(see `isLeanOnly`). Otherwise, also build `.c` files.
 -/
-def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM PUnit := do
+def Package.buildImportsAndDeps (imports : List String) (self : Package) : BuildM (Array FilePath) := do
   if imports.isEmpty then
     -- build the package's (and its dependencies') `extraDepTarget`
     buildPackageFacet self &`extraDep >>= (·.buildOpaque)
+    return #[]
   else
     -- build local imports from list
     let mods := (← getWorkspace).processImportList imports
-    if self.leanExes.isEmpty && self.defaultFacet matches .none | .leanLib | .oleans then
-      let targets ← buildModuleFacetArray mods &`lean
-      targets.forM (·.buildOpaque)
-    else
-      let targets ← buildModuleFacetArray mods &`lean.c
-      targets.forM (·.buildOpaque)
+    let (res, bStore) ← EStateT.run BuildStore.empty <| mods.mapM fun mod =>
+      if mod.shouldPrecompile then
+        buildModuleTop mod &`lean.dynlib <&> (·.withoutInfo)
+      else if self.isLeanOnly then
+        buildModuleTop mod &`lean.c <&> (·.withoutInfo)
+      else
+        buildModuleTop mod &`lean
+    let importTargets ← failOnBuildCycle res
+    let dynlibTargets := bStore.collectModuleFacetArray &`lean.dynlib
+    importTargets.forM (·.buildOpaque)
+    dynlibTargets.mapM (·.build)

Lake/Build/Index.lean

@@ -111,12 +111,8 @@ the initial set of Lake package facets (e.g., `extraDep`).
 ## Topologically-based Recursive Build Using the Index
 -/
 
-/-- The type of a recursive build function for the Lake build index. -/
-abbrev RecIndexBuildFn (m) :=
-  DRecBuildFn BuildInfo (BuildData ·.key) m
-
 /-- Recursive build function for anything in the Lake build index. -/
-@[specialize] def recBuildIndex : RecIndexBuildFn m := fun info => do
+@[specialize] def recBuildIndex (info : BuildInfo) : IndexT m (BuildData info.key) := do
   have : MonadLift BuildM m := ⟨liftM⟩
   match info with
   | .module mod facet =>

Lake/Build/Module.lean

@@ -65,14 +65,7 @@ def buildModuleFacetMap
   let (x, bStore) ← EStateT.run BuildStore.empty <| mods.forM fun mod =>
     buildModuleTop' mod facet
   failOnBuildCycle x
-  let mut res : NameMap α := RBMap.empty
-  for ⟨k, v⟩ in bStore do
-    if h : k.isModuleKey ∧ k.facet = facet then
-      let of_data := by
-        unfold BuildData
-        simp [h, eq_dynamic_type]
-      res := res.insert (k.module h.1) <| cast of_data v
-  return res
+  return bStore.collectModuleFacetMap facet
 
 -- # Module Facet Targets
 

Lake/Build/Module1.lean

@@ -8,17 +8,10 @@ import Lake.Build.Info
 import Lake.Build.Store
 import Lake.Build.Targets
 
-open Std System
-open Lean hiding SearchPath
+open System
 
 namespace Lake
 
-abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
-@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
-
-abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
-@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
-
 -- # Solo Module Targets
 
 def Module.soloTarget (mod : Module)
@@ -106,7 +99,7 @@ building an `Array` product of its direct and transitive local imports.
 : IndexT m (Array Module × Array Module) := do
   have : MonadLift BuildM m := ⟨liftM⟩
   let contents ← IO.FS.readFile mod.leanFile
-  let (imports, _, _) ← Elab.parseImports contents mod.leanFile.toString
+  let (imports, _, _) ← Lean.Elab.parseImports contents mod.leanFile.toString
   let importSet ← imports.foldlM (init := ModuleSet.empty) fun a imp => do
     if let some mod ← findModule? imp.module then return a.insert mod else return a
   let mut imports := #[]

Lake/Build/Monad.lean

@@ -7,7 +7,6 @@ import Lake.Config.Monad
 import Lake.Build.Context
 
 open System
-open Lean (Name)
 
 namespace Lake
 

Lake/Build/Store.lean

@@ -16,34 +16,47 @@ topological-based build of an initial key's dependencies).
 
 namespace Lake
 
-/-- The type of the Lake build store. -/
-abbrev BuildStore :=
-  DRBMap BuildKey BuildData BuildKey.quickCmp
-
-@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
+/-! ## Abstract Monad -/
 
 /-- A monad equipped with a Lake build store. -/
 abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
 
-instance (k : ModuleBuildKey f)
-[t : DynamicType ModuleData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    unfold BuildData
-    simp [k.is_module_key, k.facet_eq_fixed, t.eq_dynamic_type]
-
 @[inline] instance [MonadBuildStore m]
 [DynamicType ModuleData f α] : MonadStore (ModuleBuildKey f) α m where
   fetch? k := fetch? k.toBuildKey
   store k a := store k.toBuildKey a
 
-instance (k : PackageBuildKey f)
-[t : DynamicType PackageData f α] : DynamicType BuildData k α where
-  eq_dynamic_type := by
-    unfold BuildData, BuildKey.isModuleKey
-    have has_pkg := of_decide_eq_true (of_decide_eq_true k.is_package_key |>.1)
-    simp [has_pkg, k.is_package_key, k.facet_eq_fixed, t.eq_dynamic_type]
-
 @[inline] instance [MonadBuildStore m]
 [DynamicType PackageData f α] : MonadStore (PackageBuildKey f) α m where
   fetch? k := fetch? k.toBuildKey
   store k a := store k.toBuildKey a
+
+/-! ## Concrete Type -/
+
+/-- The type of the Lake build store. -/
+abbrev BuildStore :=
+  DRBMap BuildKey BuildData BuildKey.quickCmp
+
+@[inline] def BuildStore.empty : BuildStore := DRBMap.empty
+
+namespace BuildStore
+
+/-- Derive an array of module names to built facets from the store. -/
+def collectModuleFacetArray (self : BuildStore)
+(facet : WfName) [DynamicType ModuleData facet α] : Array α := Id.run do
+  let mut res : Array α := #[]
+  for ⟨k, v⟩ in self do
+    if h : k.isModuleKey ∧ k.facet = facet then
+      let of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+      res := res.push <| cast of_data v
+  return res
+
+/-- Derive a map of module names to built facets from the store. -/
+def collectModuleFacetMap (self : BuildStore)
+(facet : WfName) [DynamicType ModuleData facet α] : NameMap α := Id.run do
+  let mut res := Lean.mkNameMap α
+  for ⟨k, v⟩ in self do
+    if h : k.isModuleKey ∧ k.facet = facet then
+      let of_data := by unfold BuildData; simp [h, eq_dynamic_type]
+      res := res.insert (k.module h.1) <| cast of_data v
+  return res

Lake/CLI/Build.lean

@@ -6,8 +6,6 @@ Authors: Mac Malone
 import Lake.Build
 import Lake.CLI.Error
 
-open Lean (Name)
-
 namespace Lake
 
 def Package.defaultTarget (self : Package) : OpaqueTarget :=

Lake/CLI/Init.lean

@@ -10,7 +10,6 @@ import Lake.Config.Load
 
 namespace Lake
 open Git System
-open Lean (Name)
 
 /-- `elan` toolchain file name -/
 def toolchainFileName : FilePath :=

Lake/CLI/Main.lean

@@ -18,7 +18,7 @@ import Lake.CLI.Build
 import Lake.CLI.Error
 
 open System
-open Lean (Name Json toJson fromJson?)
+open Lean (Json toJson fromJson?)
 
 namespace Lake
 
@@ -213,8 +213,8 @@ def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit
       exit 1
     let ws ← loadWorkspace config
     let ctx ← mkBuildContext ws config.leanInstall config.lakeInstall
-    ws.root.buildImportsAndDeps imports |>.run MonadLog.eio ctx
-    IO.println <| Json.compress <| toJson ws.leanPaths
+    let dynlibs ← ws.root.buildImportsAndDeps imports |>.run MonadLog.eio ctx
+    IO.println <| Json.compress <| toJson {ws.leanPaths with loadDynlibPaths := dynlibs}
   else
     exit noConfigFileCode
 

Lake/Config/Module.lean

@@ -8,14 +8,20 @@ import Lake.Config.Package
 import Lake.Util.Name
 
 namespace Lake
-open System Lean
+open Std System
 
 /-- A buildable Lean module of a `Package`. -/
 structure Module where
   pkg : Package
   name : WfName
   deriving Inhabited
 
+abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
+@[inline] def ModuleSet.empty : ModuleSet := RBTree.empty
+
+abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
+@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
+
 /-- Locate the named module in the package (if it is local to it). -/
 def Package.findModule? (mod : Name) (self : Package) : Option Module :=
   let mod := WfName.ofName mod

Lake/Config/Package.lean

@@ -14,7 +14,6 @@ import Lake.Config.Dependency
 import Lake.Config.Script
 
 open Std System
-open Lean (Name NameMap)
 
 namespace Lake
 

Lake/Config/Resolve.lean

@@ -12,7 +12,6 @@ import Lake.Config.Workspace
 import Lake.Build.Topological
 
 open Std System
-open Lean (Name NameMap)
 
 namespace Lake
 
@@ -122,7 +121,7 @@ def resolveDeps (ws : Workspace) (pkg : Package)
     let pkg ← resolveDep ws pkg dep shouldUpdate
     pkg.dependencies.forM fun dep => discard <| resolve dep
     return pkg
-  let (res, map) ← EStateT.run (mkRBMap _ _ Name.quickCmp) <|
+  let (res, map) ← EStateT.run (mkRBMap _ _ Lean.Name.quickCmp) <|
     pkg.dependencies.forM fun dep => discard <| buildTop Dependency.name resolve dep
   match res with
   | Except.ok _ => return map

Lake/Config/Workspace.lean

@@ -10,7 +10,7 @@ import Lake.Config.Package
 import Lake.Config.Module
 
 open System
-open Lean (Name NameMap LeanPaths)
+open Lean (LeanPaths)
 
 namespace Lake
 

Lake/Util/Name.lean

@@ -10,6 +10,8 @@ open Lean
 
 namespace Lake
 
+export Lean (Name NameMap)
+
 -- # Name Helpers
 
 namespace Name