From bb8259b9af85fcf657e68d75641fa59fd360350a Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 2 Aug 2023 17:02:20 -0400
Subject: [PATCH] feat: lake: warn on mismatch pkg name and require name

see #2324
---
 src/lake/Lake/Load/Main.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index a9a5df6ffb..14a3bc7525 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -63,6 +63,8 @@ def buildUpdatedManifest (ws : Workspace) : LogIO Manifest := do
             return pkg
           else
             let depPkg ← loadDepPackage ws.dir result pkg.leanOpts dep.options
+            if depPkg.name ≠ dep.name then
+              logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
             modifyThe (NameMap Package) (·.insert dep.name depPkg)
             return depPkg
         return {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)}