feat: lake: warn on mismatch pkg name and require name

see #2324
This commit is contained in:
tydeu 2023-08-02 17:02:20 -04:00 committed by Mac Malone
parent 35bad47c1b
commit bb8259b9af

View file

@ -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 ·)}