diff --git a/Lake/Glob.lean b/Lake/Glob.lean
new file mode 100644
index 0000000000..58e40a292e
--- /dev/null
+++ b/Lake/Glob.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Data.Name
+import Lean.Elab.Import
+
+open System (FilePath)
+open Lean (Name)
+
+namespace Lake
+
+/--
+  A specification of a set of module names to build.
+-/
+inductive Glob
+  | /-- Builds the specified module name -/
+    one : Name → Glob
+  | /-- Builds the specified module and all submodules -/
+    andSubdirs : Name → Glob
+  | /--
+      Builds all submodules of the specified module,
+      without building the module itself
+    -/
+    subdirs : Name → Glob
+
+instance : Coe Name Glob := ⟨Glob.one⟩
+
+-- TODO(Mario): Rename Lean.modToFilePath.go to modToDir
+def modToDir (base : FilePath) : Name → FilePath
+  | Name.str p h _ => modToDir base p / h
+  | Name.anonymous => base
+  | Name.num p _ _ => panic! "ill-formed import"
+
+partial def directoryTraversal [Monad m] [MonadLiftT IO m]
+  (base : FilePath) (push : FilePath → m PUnit) : m PUnit := do
+  for entry in ← base.readDir do
+    let path := entry.path
+    if (← path.isDir : Bool) then
+      directoryTraversal path push
+    else
+      push path
+
+def onSubdirectoryFilesWithExt [Monad m] [MonadLiftT IO m]
+  (base : FilePath) (ext : String) (push : FilePath → m PUnit) : m PUnit :=
+  directoryTraversal base fun file => do
+    if file.extension == some ext then
+      push file
+
+def Glob.pushFilePaths [Monad m] [MonadLiftT IO m]
+  (base : FilePath) (ext : String) (push : FilePath → m PUnit) :
+  Glob → m PUnit
+  | Glob.one n => push $ modToDir base n |>.withExtension ext
+  | Glob.subdirs n =>
+    let dir := modToDir base n
+    onSubdirectoryFilesWithExt base ext push
+  | Glob.andSubdirs n => do
+    let dir := modToDir base n
+    onSubdirectoryFilesWithExt base ext push
+    push $ dir.withExtension ext
+
+def globsToFilePaths (base : FilePath) (ext : String)
+  (globs : List Glob) : IO (Array FilePath) := do
+  let arr ← IO.mkRef #[]
+  for glob in globs do
+    glob.pushFilePaths base ext fun file => arr.modify (·.push file)
+  arr.get
diff --git a/Lake/Package.lean b/Lake/Package.lean
index 9840da1e19..621d47e432 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -8,6 +8,7 @@ import Lean.Elab.Import
 import Std.Data.HashMap
 import Lake.LeanVersion
 import Lake.BuildTarget
+import Lake.Glob
 
 open Std System
 open Lean (Name)
@@ -180,6 +181,12 @@ structure PackageConfig where
   -/
   libName : String := moduleRoot.toString (escape := false)
 
+  /--
+    The list of modules or module globs to build for the library target.
+    Defaults to building the package's `moduleRoot` (and dependencies).
+  -/
+  libModules : List Glob := [moduleRoot]
+
   /--
     The build subdirectory to which Lake should output the package's static library.
     Defaults to `defaultLibDir` (i.e., `lib`).
@@ -379,6 +386,10 @@ def binFile (self : Package) : FilePath :=
 def libDir (self : Package) : FilePath :=
   self.buildDir / self.config.libDir
 
+/-- The package's `libModules` configuration. -/
+def libModules (self : Package) : List Glob :=
+  self.config.libModules
+
 /-- The package's `libName` configuration. -/
 def staticLibName (self : Package) : FilePath :=
   self.config.libName