From ed5dc328d98e5799c148c8834690fe95aa8a079f Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sat, 13 Sep 2025 09:56:54 -0400
Subject: [PATCH] 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).
---
 src/lake/Lake.lean      |  1 +
 src/lake/Lake/Util.lean | 38 ++++++++++++++++++++++++++++++++++++++
 src/lakefile.toml.in    | 10 ++--------
 3 files changed, 41 insertions(+), 8 deletions(-)
 create mode 100644 src/lake/Lake/Util.lean

diff --git a/src/lake/Lake.lean b/src/lake/Lake.lean
index c25043d844..820e1a63fb 100644
--- a/src/lake/Lake.lean
+++ b/src/lake/Lake.lean
@@ -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
diff --git a/src/lake/Lake/Util.lean b/src/lake/Lake/Util.lean
new file mode 100644
index 0000000000..d80e643c29
--- /dev/null
+++ b/src/lake/Lake/Util.lean
@@ -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
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index b9e8381092..a95ce9377c 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -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"]