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