From fa2ddf1c567c247d3133930a3747152b8060398f Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 22 Jan 2026 13:12:14 -0500
Subject: [PATCH] chore: lake: disable `import all` check in module
 disambiguation (#12104)

This PR disables an overlooked check (in #12045) of `import all` during
module disambiguation.
---
 src/lake/Lake/Build/Module.lean | 34 +++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 49240b8adf..81997d353a 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -357,6 +357,7 @@ private def Package.discriminant (self : Package) :=
   else
     s!"{self.prettyName}@{self.version}"
 
+set_option linter.unusedVariables.funArgs false in
 private def fetchImportInfo
   (fileName : String) (pkgName modName : Name) (header : ModuleHeader)
 : FetchM (Job ModuleImportInfo) := do
@@ -381,22 +382,23 @@ private def fetchImportInfo
       let importJob ← mod.exportInfo.fetch
       return s.zipWith (sync := true) (·.addImport nonModule imp ·) importJob
     else
-      let isImportable (mod) :=
-        mod.allowImportAll || pkgName == mod.pkg.keyName
-      let allImportable :=
-        if imp.importAll then
-          mods.all isImportable
-        else true
-      unless allImportable do
-        let msg := s!"{fileName}: cannot `import all` the module `{imp.module}` \
-          from the following packages:"
-        let msg := mods.foldl (init := msg) fun msg mod =>
-          if isImportable mod then
-            msg
-          else
-            s!"{msg}\n  {mod.pkg.discriminant}"
-        logError msg
-        return .error
+      -- Remark: We've decided to disable this check for now
+      -- let isImportable (mod) :=
+      --   mod.allowImportAll || pkgName == mod.pkg.keyName
+      -- let allImportable :=
+      --   if imp.importAll then
+      --     mods.all isImportable
+      --   else true
+      -- unless allImportable do
+      --   let msg := s!"{fileName}: cannot `import all` the module `{imp.module}` \
+      --     from the following packages:"
+      --   let msg := mods.foldl (init := msg) fun msg mod =>
+      --     if isImportable mod then
+      --       msg
+      --     else
+      --       s!"{msg}\n  {mod.pkg.discriminant}"
+      --   logError msg
+      --   return .error
       let mods : Vector Module n := .mk mods rfl
       let expInfosJob ← Job.collectVector <$> mods.mapM (·.exportInfo.fetch)
       s.bindM (sync := true) fun impInfo => do