fix: make root module "private" to the package

Author: tydeu

Diff for: Lake/Build/Info.lean

@@ -36,7 +36,7 @@ inductive BuildInfo
 /-! ### Build Key Helper Constructors -/
 
 abbrev Module.mkBuildKey (facet : WfName) (self : Module) : ModuleBuildKey facet :=
-  ⟨⟨none, self.name, facet⟩, rfl, rfl⟩
+  ⟨⟨none, self.keyName, facet⟩, rfl, rfl⟩
 
 abbrev Package.mkBuildKey (facet : WfName) (self : Package) : PackageBuildKey facet :=
   ⟨⟨self.name, none, facet⟩, rfl, rfl⟩

Diff for: Lake/Config/LeanExe.lean

@@ -34,7 +34,7 @@ with a single module (the root).
 -/
 def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig) : LeanLibConfig where
   name := self.name
-  roots := #[self.root]
+  roots := #[]
   libName := self.exeName
   toLeanConfig := self.toLeanConfig
 
@@ -49,8 +49,10 @@ namespace LeanExe
   ⟨self.pkg, self.config.toLeanLibConfig⟩
 
 /-- The executable's root module. -/
-@[inline] def root (self : LeanExe) : Module :=
-  ⟨self.toLeanLib, WfName.ofName self.config.root⟩
+@[inline] def root (self : LeanExe) : Module where
+  lib := self.toLeanLib
+  name := WfName.ofName self.config.root
+  keyName := WfName.ofName self.pkg.name |>.appendName self.config.root
 
 /- Return the the modules root if the name matches, otherwise return none. -/
 def isRoot? (name : Name) (self : LeanExe) : Option Module :=

Diff for: Lake/Config/Module.lean

@@ -13,6 +13,11 @@ open Std System
 structure Module where
   lib : LeanLib
   name : WfName
+  /--
+  The name of the module as a key.
+  Used to create private modules (e.g., executable roots).
+  -/
+  keyName : WfName := name
   deriving Inhabited
 
 abbrev ModuleSet := RBTree Module (·.name.quickCmp ·.name)
@@ -24,14 +29,14 @@ abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
 /-- Locate the named module in the library (if it is buildable and local to it). -/
 def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module :=
   let mod := WfName.ofName mod
-  if self.isBuildableModule mod then some ⟨self, mod⟩ else none
+  if self.isBuildableModule mod then some {lib := self, name := mod} else none
 
 /-- Get an `Array` of the library's modules. -/
 def LeanLib.getModuleArray (self : LeanLib) : IO (Array Module) :=
   (·.2) <$> StateT.run (s := #[]) do
     self.config.globs.forM fun glob => do
       glob.forEachModuleIn self.srcDir fun mod => do
-        modify (·.push ⟨self, mod⟩)
+        modify (·.push {lib := self, name := mod})
 
 namespace Module
 

Diff for: Lake/Util/Name.lean

@@ -174,10 +174,17 @@ instance : ToString WfName := ⟨(·.toString)⟩
 def isPrefixOf : WfName → WfName → Bool
 | ⟨n, _⟩, ⟨n', _⟩ => n.isPrefixOf n'
 
-def append : WfName → WfName → WfName
+protected def append : WfName → WfName → WfName
 | ⟨n, w⟩, ⟨n', w'⟩ => ⟨n.append n', Name.wf_of_append w w'⟩
 
-instance : Append WfName := ⟨append⟩
+instance : Append WfName := ⟨WfName.append⟩
+
+def appendName (n : WfName) : Name → WfName
+| .anonymous => n
+| .str p s _ => mkStr (appendName n p) s
+| .num p v _ => mkNum (appendName n p) v
+
+instance : HAppend WfName Name WfName := ⟨appendName⟩
 
 @[inline] protected def hash : WfName → UInt64
 | ⟨n, _⟩ => n.hash