max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: don't use globs to determine local modules + cleanup

Browse source 
Reasion: globs should be submodules of the roots
This commit is contained in:
tydeu 2021-09-24 01:11:29 -04:00
parent 0f0ea57ef5
commit ba8067f3bd
3 changed files with 8 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Lake/Glob.lean
View file

@ -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

9
Lake/Package.lean
View file

@ -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

2
README.md
View file

@ -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