chore: lake: disable import all check in module disambiguation (#12104)

This PR disables an overlooked check (in #12045) of `import all` during
module disambiguation.
This commit is contained in:
Mac Malone 2026-01-22 13:12:14 -05:00 committed by GitHub
parent f9af240bc4
commit fa2ddf1c56
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

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