refactor: import Lake.Util.* from Lake (#10371)

This PR explicitly imports `Lake.Util` submodules in `Lake`, ensuring
Lake utilities are consistently available by default in configuration
files.

It also simplifies the Lake globs for the core build to ensure all Lake
submodules are built (even if they are not imported).
This commit is contained in:
Mac Malone 2025-09-13 09:56:54 -04:00 committed by GitHub
parent 2bbf5db04f
commit ed5dc328d9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 41 additions and 8 deletions

View file

@ -11,4 +11,5 @@ public import Lake.CLI.Actions
public import Lake.Config
public import Lake.DSL
public import Lake.Toml
public import Lake.Util
public import Lake.Version

38
src/lake/Lake/Util.lean Normal file
View file

@ -0,0 +1,38 @@
/-
Copyright (c) 2025 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
module
prelude
public import Lake.Util.Binder
public import Lake.Util.Casing
public import Lake.Util.Cli
public import Lake.Util.Cycle
public import Lake.Util.Date
public import Lake.Util.EquipT
public import Lake.Util.Error
public import Lake.Util.EStateT
public import Lake.Util.Exit
public import Lake.Util.Family
public import Lake.Util.FilePath
public import Lake.Util.Git
public import Lake.Util.IO
public import Lake.Util.JsonObject
public import Lake.Util.Lift
public import Lake.Util.Lock
public import Lake.Util.Log
public import Lake.Util.MainM
public import Lake.Util.Message
public import Lake.Util.Name
public import Lake.Util.NativeLib
public import Lake.Util.Opaque
public import Lake.Util.OrderedTagAttribute
public import Lake.Util.OrdHashSet
public import Lake.Util.Proc
public import Lake.Util.RBArray
public import Lake.Util.Store
public import Lake.Util.StoreInsts
public import Lake.Util.Task
public import Lake.Util.Version

View file

@ -62,14 +62,8 @@ globs = [
[[lean_lib]]
name = "Lake"
srcDir = "lake"
globs = [
# Lake API imported by configuration files
"Lake",
# API only imported by `LakeMain` and the `lake` CLI
"Lake.CLI", "Lake.Load",
# Additional utilities which may not be imported
"Lake.Util.+",
]
# Build Lake and all its submodules (which may not be imported elsewhere)
globs = ["Lake.*"]
libName = "${LAKE_LIB_PREFIX}Lake"
defaultFacets = ["static", "static.export"]