From ba8067f3bd200a2c40ac2d7d694f510947ed0737 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 24 Sep 2021 01:11:29 -0400
Subject: [PATCH] refactor: don't use globs to determine local modules +
 cleanup

Reasion: globs should be submodules of the roots
---
 Lake/Glob.lean    | 6 +++---
 Lake/Package.lean | 9 ++++-----
 README.md         | 2 +-
 3 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/Lake/Glob.lean b/Lake/Glob.lean
index 61e3a86ef8..b4e85ef53e 100644
--- a/Lake/Glob.lean
+++ b/Lake/Glob.lean
@@ -12,7 +12,7 @@ namespace Lake
 
 /-- A specification of a set of module names. -/
 inductive Glob
-| /-- Selects the specified module name. -/
+| /-- Selects just the specified module name. -/
   one : Name → Glob
 | /--
     Selects all submodules of the specified module,
@@ -26,8 +26,8 @@ instance : Coe Name Glob := ⟨Glob.one⟩
 
 def Glob.matches (m : Name) : (self : Glob) → Bool
 | one n => n == m
-| submodules n => n.isPrefixOf m
-| andSubmodules n => n == m || n.isPrefixOf m
+| submodules n => n.isPrefixOf m && n != m
+| andSubmodules n => n.isPrefixOf m
 
 -- TODO(Mario): Rename Lean.modToFilePath.go to modToDir
 def modToDir (base : FilePath) : Name → FilePath
diff --git a/Lake/Package.lean b/Lake/Package.lean
index 7a5b2e1841..0c2a8d8850 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -160,11 +160,11 @@ structure PackageConfig where
   libRoots : Array Name := #[name.capitalize]
 
   /--
-    An `Array` of additional module `Glob`s to include in the package.
-    Defaults to singular globs of the module's `libRoots`.
+    An `Array` of module `Glob`s to build for the package's library.
+    Defaults to a `Glob.one` of each of the module's `libRoots`.
 
     Submodule globs build every source file within their directory.
-    Local imports of said files (i.e., fellow modules of the package) are
+    Local imports of glob'ed files (i.e., fellow modules of the package) are
     also recursively built.
   -/
   libGlobs : Array Glob := libRoots.map Glob.one
@@ -334,8 +334,7 @@ def libGlobs (self : Package) : Array Glob :=
 
 /-- Whether the given module is local to the package. -/
 def isLocalModule (mod : Name) (self : Package) : Bool :=
-  self.libRoots.any (fun root => root.isPrefixOf mod) ||
-  self.libGlobs.any (fun glob => glob.matches mod)
+  self.libRoots.any fun root => root.isPrefixOf mod
 
 /-- Get an `Array` of the package's module. -/
 def getModuleArray (self : Package) : IO (Array Name) := do
diff --git a/README.md b/README.md
index f431878316..24b32395bc 100644
--- a/README.md
+++ b/README.md
@@ -78,7 +78,7 @@ Lake provides a large assortment of configuration options for packages.
 * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.
 * `oleanDir`: The build subdirectory to which Lake should output the package's `.olean` files. Defaults to `lib`.
 * `libRoots`: The root module(s) of the package. Imports relative to this root (e.g., `Pkg.Foo`) are considered part of the package. Defaults to a single root of the package's uppercase `name`.
-* `libGlobs`: An `Array` of additional module `Glob`s to include in the package. Defaults to singular globs of the module's `libRoots`. Submodule globs build every source file within their directory. Local imports of said files (i.e., fellow modules of the package) are also recursively built.
+* `libGlobs`: An `Array` of module `Glob`s to build for the package's library. Defaults to a `Glob.one` of each of the module's `libRoots`. Submodule globs build every source file within their directory. Local imports of glob'ed files (i.e., fellow modules of the package) are also recursively built.
 * `leanArgs`: An `Array` of additional arguments to pass to `lean` while compiling Lean source files.
 
 ### Library / Binary Compilation