feat: lake: resolve module clashes on import (#11270)

This PR adds a module resolution procedure to Lake to disambiguate
modules that are defined in multiple packages.

On an `import`, Lake will now check if multiple packages within the
workspace define the module. If so, it will verify that modules have
sufficiently similar definitions (i.e., artifacts with the same content
hashes). If not, Lake will report an error.

This verification is currently only done for direct imports. Transitive
imports are not checked for consistency. An overhaul of transitive
imports will come later.

Author: tydeu

src/lake/Lake/Build/Facets.lean

@@ -74,12 +74,15 @@ public structure ModuleImportInfo where
   allTransTrace : BuildTrace
   /-- Transitive import trace for an `import` of the module without the module system enabled. -/
   legacyTransTrace : BuildTrace
+  deriving Inhabited
 
 /-- **For internal use only.** Information about the imports of this module. -/
 builtin_facet importInfo : Module => ModuleImportInfo
 
 /-- Information useful to importers of a module. -/
 public structure ModuleExportInfo where
+  /-- The trace of the module's source file. -/
+  srcTrace : BuildTrace
   /-- Artifacts directly needed for an `import` of the module with the module system enabled. -/
   arts : ImportArtifacts
   /-- The trace of the module's public olean. -/
@@ -101,6 +104,7 @@ public structure ModuleExportInfo where
   allTransTrace : BuildTrace
   /-- Transitive import trace for an `import` of the module without the module system enabled. -/
   legacyTransTrace : BuildTrace
+  deriving Inhabited
 
 /-- **For internal use only.** Information useful to importers of this module. -/
 builtin_facet exportInfo : Module => ModuleExportInfo

src/lake/Lake/Build/Infos.lean

@@ -67,6 +67,7 @@ public structure ModuleImport extends Import where
 /-- A module's source file path plus its parsed header. -/
 public structure ModuleInput where
   path : FilePath
+  trace : BuildTrace
   header : ModuleHeader
   imports : Array ModuleImport
 

src/lake/Lake/Build/Job/Monad.lean

@@ -230,7 +230,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 -/
 @[inline] public def zipResultWith
   [OptDataKind γ] (f : JobResult α → JobResult β → JobResult γ) (self : Job α) (other : Job β)
-  (prio := Task.Priority.default) (sync := true)
+  (prio := Task.Priority.default) (sync := false)
 : Job γ := Job.ofTask $
   self.task.bind (prio := prio) (sync := true) fun rx =>
   other.task.map (prio := prio) (sync := sync) fun ry =>
@@ -242,7 +242,7 @@ results of `a` and `b`. The job `c` errors if either `a` or `b` error.
 -/
 @[inline] public def zipWith
   [OptDataKind γ] (f : α → β → γ) (self : Job α) (other : Job β)
-  (prio := Task.Priority.default) (sync := true)
+  (prio := Task.Priority.default) (sync := false)
 : Job γ :=
   self.zipResultWith (other := other) (prio := prio) (sync := sync) fun
   | .ok a sa, .ok b sb => .ok (f a b) (sa.merge sb)
@@ -257,7 +257,7 @@ public def add (self : Job α) (other : Job β) : Job α :=
 
 /-- Merges this job with another, discarding both outputs. -/
 public def mix (self : Job α) (other : Job β) : Job Unit :=
-  self.zipWith (fun _ _ => ()) other
+  self.zipWith (sync := true) (fun _ _ => ()) other
 
 /-- Merge a `List` of jobs into one, discarding their outputs. -/
 public def mixList (jobs : List (Job α)) (traceCaption := "<collection>")  : Job Unit :=
@@ -269,10 +269,18 @@ public def mixArray (jobs : Array (Job α)) (traceCaption := "<collection>")  :
 
 /-- Merge a `List` of jobs into one, collecting their outputs into a `List`. -/
 public def collectList (jobs : List (Job α)) (traceCaption := "<collection>") : Job (List α) :=
-  jobs.foldr (zipWith List.cons) (traceRoot [] traceCaption)
+  jobs.foldr (zipWith (sync := true) List.cons) (traceRoot [] traceCaption)
 
 /-- Merge an `Array` of jobs into one, collecting their outputs into an `Array`. -/
 public def collectArray (jobs : Array (Job α)) (traceCaption := "<collection>") : Job (Array α) :=
-  jobs.foldl (zipWith Array.push) (traceRoot (Array.mkEmpty jobs.size) traceCaption)
+  jobs.foldl (zipWith (sync := true) Array.push) (traceRoot (Array.mkEmpty jobs.size) traceCaption)
+
+private instance : Nonempty ({α : Type u} → [Nonempty α] → α) := ⟨Classical.ofNonempty⟩
+
+/-- Merge an `Vector` of jobs into one, collecting their outputs into an `Array`. -/
+public def collectVector {α : Type u} [Nonempty α] (jobs : Vector (Job α) n) (traceCaption := "<collection>") : Job (Vector α n) :=
+  let placeholder := unsafe have : Nonempty α := inferInstance; (unsafeCast () : α)
+  n.fold (init := traceRoot (Vector.replicate n placeholder) traceCaption) fun i h job =>
+    job.zipWith (sync := true) (Vector.set · i · h) jobs[i]
 
 end Job

src/lake/Lake/Build/Module.lean

@@ -30,11 +30,12 @@ Build function definitions for a module's builtin facets.
 private def Module.recFetchInput (mod : Module) : FetchM (Job ModuleInput) := Job.async do
   let path := mod.leanFile
   let contents ← IO.FS.readFile path
-  setTrace {caption := path.toString, mtime := ← getMTime path, hash := .ofText contents}
+  let trace := {caption := path.toString, mtime := ← getMTime path, hash := .ofText contents}
+  setTrace trace
   let header ← Lean.parseImports' contents path.toString
   let imports ← header.imports.mapM fun imp => do
     return ⟨imp, (← findModule? imp.module)⟩
-  return {path, header, imports}
+  return {path, header, imports, trace}
 
 /-- The `ModuleFacetConfig` for the builtin `inputFacet`. -/
 public def Module.inputFacetConfig : ModuleFacetConfig inputFacet :=
@@ -261,25 +262,37 @@ private def ModuleImportInfo.nil (modName : Name) : ModuleImportInfo where
   allTransTrace := .nil s!"{modName} transitive imports (all)"
   legacyTransTrace := .nil s!"{modName} transitive imports (legacy)"
 
+private def ModuleExportInfo.disambiguationHash
+  (self : ModuleExportInfo) (nonModule : Bool) (imp : Import)
+: Hash :=
+  if nonModule then
+    self.legacyTransTrace.hash.mix self.allArtsTrace.hash
+  else if imp.importAll then
+    self.allTransTrace.hash.mix self.allArtsTrace.hash
+  else if imp.isMeta then
+    self.metaTransTrace.hash.mix self.metaArtsTrace.hash
+  else
+    self.transTrace.hash.mix self.artsTrace.hash
+
 private def ModuleImportInfo.addImport
   (info : ModuleImportInfo) (nonModule : Bool)
-  (mod : Module) (imp : Import) (expInfo : ModuleExportInfo)
+  (imp : Import) (expInfo : ModuleExportInfo)
 : ModuleImportInfo :=
   let info :=
     if nonModule then
       {info with
-        directArts := info.directArts.insert mod.name expInfo.allArts
+        directArts := info.directArts.insert imp.module expInfo.allArts
         trace := info.trace.mix expInfo.legacyTransTrace |>.mix expInfo.allArtsTrace.withoutInputs
       }
     else if imp.importAll then
       {info with
-        directArts := info.directArts.insert mod.name expInfo.allArts
+        directArts := info.directArts.insert imp.module expInfo.allArts
         trace := info.trace.mix expInfo.allTransTrace |>.mix expInfo.allArtsTrace.withoutInputs
       }
     else
       let info :=
-        if !info.directArts.contains mod.name then -- do not demote `import all`
-          {info with directArts := info.directArts.insert mod.name expInfo.arts}
+        if !info.directArts.contains imp.module  then -- do not demote `import all`
+          {info with directArts := info.directArts.insert imp.module expInfo.arts}
         else
           info
       if imp.isMeta then
@@ -338,6 +351,12 @@ private def ModuleImportInfo.addImport
   else
     info
 
+private def Package.discriminant (self : Package) :=
+  if self.version == {} then
+    self.name.toString
+  else
+    s!"{self.name}@{self.version}"
+
 private def fetchImportInfo
   (fileName : String) (pkgName modName : Name) (header : ModuleHeader)
 : FetchM (Job ModuleImportInfo) := do
@@ -348,13 +367,51 @@ private def fetchImportInfo
     if modName = imp.module then
       logError s!"{fileName}: module imports itself"
       return .error
-    let some mod ← findModule? imp.module
-      | return s
-    if imp.importAll && !mod.allowImportAll && pkgName != mod.pkg.name then
-      logError s!"{fileName}: cannot 'import all' across packages"
-      return .error
-    let importJob ← mod.exportInfo.fetch
-    return s.zipWith (·.addImport nonModule mod imp ·) importJob
+    let mods ← findModules imp.module
+    let n := mods.size
+    if h : n = 0 then
+      return s
+    else if n = 1 then -- common fast path
+      let mod := mods[0]
+      if imp.importAll && !mod.allowImportAll && pkgName != mod.pkg.name then
+        logError s!"{fileName}: cannot `import all` \
+          the module `{imp.module}` from the package `{mod.pkg.discriminant}`"
+        return .error
+      let importJob ← mod.exportInfo.fetch
+      return s.zipWith (sync := true) (·.addImport nonModule imp ·) importJob
+    else
+      let isImportable (mod) :=
+        mod.allowImportAll || pkgName == mod.pkg.name
+      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
+      expInfosJob.mapM (sync := true) fun expInfos => do
+        let expInfo := expInfos[0]
+        let impHash := expInfo.disambiguationHash nonModule imp
+        let allEquiv := expInfos.toArray.all (start := 1) fun expInfo =>
+          impHash == expInfo.disambiguationHash nonModule imp
+        unless allEquiv do
+          let msg := s!"{fileName}: could not disambiguate the module `{imp.module}`; \
+            multiple packages provide distinct definitions:"
+          let msg := n.fold (init := msg) fun i h s =>
+            let hash := expInfos[i].disambiguationHash nonModule imp
+            s!"{s}\n  {mods[i].pkg.discriminant} (hash: {hash})"
+          error msg
+        return impInfo.addImport nonModule imp expInfo
 
 /-- The `ModuleFacetConfig` for the builtin `importInfoFacet`. -/
 public def Module.importInfoFacetConfig : ModuleFacetConfig importInfoFacet :=
@@ -374,20 +431,21 @@ private def noIRError :=
 /-- Computes the import artifacts and transitive import trace of a module's imports. -/
 private def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportInfo) := do
   (← mod.leanArts.fetch).mapM (sync := true) fun arts => do
-    let header ← (← mod.header.fetch).await
+    let input ← (← mod.input.fetch).await
     let importInfo ← (← mod.importInfo.fetch).await
     let artsTrace := BuildTrace.nil s!"{mod.name}:importArts"
     let metaArtsTrace := BuildTrace.nil s!"{mod.name}:importArts (meta)"
     let allArtsTrace := BuildTrace.nil s!"{mod.name}:importAllArts"
     let olean := arts.olean
-    if header.isModule then
+    if input.header.isModule then
       let some oleanServer := arts.oleanServer?
         | error noServerOLeanError
       let some ir := arts.ir?
         | error noIRError
       let some oleanPrivate := arts.oleanPrivate?
         | error noPrivateOLeanError
       return {
+        srcTrace := input.trace
         arts := .ofArray #[olean.path, ir.path, oleanServer.path]
         artsTrace := artsTrace.mix olean.trace
         metaArtsTrace := metaArtsTrace.mix olean.trace |>.mix ir.trace
@@ -401,6 +459,7 @@ private def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportIn
       }
     else
       return {
+        srcTrace := input.trace
         arts := ⟨#[olean.path]⟩
         artsTrace := artsTrace.mix olean.trace
         metaArtsTrace := metaArtsTrace.mix olean.trace

src/lake/Lake/Config/Monad.lean

@@ -83,6 +83,10 @@ public def findPackage? (name : Name) : m (Option (NPackage name)) :=
 public def findModule? (name : Name) : m (Option Module) :=
   (·.findModule? name) <$> getWorkspace
 
+@[inherit_doc Workspace.findModules, inline]
+public def findModules (name : Name) : m (Array Module) :=
+  (·.findModules name) <$> getWorkspace
+
 @[inherit_doc Workspace.findModuleBySrc?, inline]
 public def findModuleBySrc? (path : FilePath) : m (Option Module) :=
   (·.findModuleBySrc? path) <$> getWorkspace

src/lake/Lake/Config/Package.lean

@@ -131,7 +131,7 @@ namespace Package
 
 /-- The identifier passed to Lean to disambiguate the package's native symbols. -/
 public def id? (self : Package) : Option PkgId :=
-  if self.bootstrap then none else some <| self.name.toString (escape := false)
+  if self.bootstrap then none else some <| self.origName.toString (escape := false)
 
 /-- The package version. -/
 @[inline] public def version (self : Package) : LeanVer  :=

src/lake/Lake/Config/Workspace.lean

@@ -132,6 +132,10 @@ public def isBuildableModule (mod : Name) (self : Workspace) : Bool :=
 public protected def findModule? (mod : Name) (self : Workspace) : Option Module :=
   self.packages.findSome? (·.findModule? mod)
 
+/-- For each package in the workspace, locate the named, buildable, importable, local module. -/
+public protected def findModules (mod : Name) (self : Workspace) : Array Module :=
+  self.packages.filterMap (·.findModule? mod)
+
 /-- Locate the named, buildable, but not necessarily importable, module in the workspace. -/
 public def findTargetModule? (mod : Name) (self : Workspace) : Option Module :=
   self.packages.findSome? (·.findTargetModule? mod)

tests/lake/tests/module/test.sh

@@ -20,7 +20,7 @@ public def foo : String := "bar"
 EOF
 
 # Test cross-package `import all` is prevented by default
-test_err "cannot 'import all' across packages" build ErrorTest.CrossPackageImportAll
+test_err 'cannot `import all` the module' build ErrorTest.CrossPackageImportAll
 # Test cross-package `import all` is allowed when `allowImportAll = true` is set
 test_run build Test.CrossPackageImportAll
 

tests/pkg/mod_clash/Test/ImportSimilar.lean

@@ -0,0 +1,5 @@
+module
+
+import Similar
+
+def testSimilar := similar

tests/pkg/mod_clash/depA/Similar.lean

@@ -0,0 +1,3 @@
+module
+
+public def similar : String := "A"