refactor: reverse pkg/lib search & no exe roots in import (leanprover…

…#2937)

Closes leanprover#2548.

Later packages and libraries in the dependency tree are now preferred
over earlier ones. That is, the later ones "shadow" the earlier ones.
Such an ordering is more consistent with how declarations generally work
in programming languages.

This will break any package that relied on the previous ordering.

Also includes a related fix to `findModule?` that mistakenly treated
executable roots as importable.

src/lake/Lake/CLI/Build.lean

@@ -103,7 +103,7 @@ def resolveTargetInPackage (ws : Workspace)
     Array.singleton <$> resolveExternLibTarget lib facet
   else if let some lib := pkg.findLeanLib? target then
     resolveLibTarget ws lib facet
-  else if let some mod := pkg.findModule? target then
+  else if let some mod := pkg.findTargetModule? target then
     Array.singleton <$> resolveModuleTarget ws mod facet
   else
     throw <| CliError.missingTarget pkg.name (target.toString false)
@@ -131,7 +131,7 @@ def resolveTargetInWorkspace (ws : Workspace)
     resolveLibTarget ws lib facet
   else if let some pkg := ws.findPackage? target then
     resolvePackageTarget ws pkg facet
-  else if let some mod := ws.findModule? target then
+  else if let some mod := ws.findTargetModule? target then
     Array.singleton <$> resolveModuleTarget ws mod facet
   else
     throw <| CliError.unknownTarget target
@@ -147,7 +147,7 @@ def resolveTargetBaseSpec
       resolvePackageTarget ws pkg facet
     else if spec.startsWith "+" then
       let mod := spec.drop 1 |>.toName
-      if let some mod := ws.findModule? mod then
+      if let some mod := ws.findTargetModule? mod then
         Array.singleton <$> resolveModuleTarget ws mod facet
       else
         throw <| CliError.unknownModule mod
@@ -160,7 +160,7 @@ def resolveTargetBaseSpec
       resolvePackageTarget ws pkg facet
     else if targetSpec.startsWith "+" then
       let mod := targetSpec.drop 1 |>.toName
-      if let some mod := pkg.findModule? mod then
+      if let some mod := pkg.findTargetModule? mod then
         Array.singleton <$> resolveModuleTarget ws mod facet
       else
         throw <| CliError.unknownModule mod

src/lake/Lake/Config/LeanExe.lean

@@ -89,8 +89,6 @@ That is, the package's `weakLinkArgs` plus the executable's  `weakLinkArgs`.
 
 end LeanExe
 
-/-- Locate the named module in the package (if it is buildable and local to it). -/
-def Package.findModule? (mod : Name) (self : Package) : Option Module :=
-  self.leanExes.findSome? (·.isRoot? mod) <|>
-  self.leanLibs.findSome? (·.findModule? mod)
-
+/-- Locate the named, buildable, but not necessarily importable, module in the package. -/
+def Package.findTargetModule? (mod : Name) (self : Package) : Option Module :=
+  self.leanExes.findSomeRev? (·.isRoot? mod) <|> self.findModule? mod

src/lake/Lake/Config/Module.lean

@@ -32,10 +32,17 @@ abbrev OrdModuleSet := OrdHashSet Module
 abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name)
 @[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty
 
-/-- Locate the named module in the library (if it is buildable and local to it). -/
+/--
+Locate the named, buildable module in the library
+(which implies it is local and importable).
+-/
 def LeanLib.findModule? (mod : Name) (self : LeanLib) : Option Module :=
   if self.isBuildableModule mod then some {lib := self, name := mod} else none
 
+/--  Locate the named, buildable, importable, local module in the package.  -/
+def Package.findModule? (mod : Name) (self : Package) : Option Module :=
+  self.leanLibs.findSomeRev? (·.findModule? mod)
+
 /-- Get an `Array` of the library's modules (as specified by its globs). -/
 def LeanLib.getModuleArray (self : LeanLib) : IO (Array Module) :=
   (·.2) <$> StateT.run (s := #[]) do

src/lake/Lake/Config/Workspace.lean

@@ -76,7 +76,7 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace :=
 
 /-- Try to find a script in the workspace with the given name. -/
 def findScript? (script : Name) (self : Workspace) : Option Script :=
-  self.packages.findSome? (·.scripts.find? script)
+  self.packages.findSomeRev? (·.scripts.find? script)
 
 /-- Check if the module is local to any package in the workspace. -/
 def isLocalModule (mod : Name) (self : Workspace) : Bool :=
@@ -86,25 +86,29 @@ def isLocalModule (mod : Name) (self : Workspace) : Bool :=
 def isBuildableModule (mod : Name) (self : Workspace) : Bool :=
   self.packages.any fun pkg => pkg.isBuildableModule mod
 
-/-- Locate the named module in the workspace (if it is local to it). -/
+/-- Locate the named, buildable, importable, local module in the workspace. -/
 def findModule? (mod : Name) (self : Workspace) : Option Module :=
-  self.packages.findSome? (·.findModule? mod)
+  self.packages.findSomeRev? (·.findModule? mod)
+
+/-- Locate the named, buildable, but not necessarily importable, module in the workspace. -/
+def findTargetModule? (mod : Name) (self : Workspace) : Option Module :=
+  self.packages.findSomeRev? (·.findTargetModule? mod)
 
 /-- Try to find a Lean library in the workspace with the given name. -/
 def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib :=
-  self.packages.findSome? fun pkg => pkg.findLeanLib? name
+  self.packages.findSomeRev? fun pkg => pkg.findLeanLib? name
 
 /-- Try to find a Lean executable in the workspace with the given name. -/
 def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe :=
-  self.packages.findSome? fun pkg => pkg.findLeanExe? name
+  self.packages.findSomeRev? fun pkg => pkg.findLeanExe? name
 
 /-- Try to find an external library in the workspace with the given name. -/
 def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
-  self.packages.findSome? fun pkg => pkg.findExternLib? name
+  self.packages.findSomeRev? fun pkg => pkg.findExternLib? name
 
 /-- Try to find a target configuration in the workspace with the given name. -/
 def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) :=
-  self.packages.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
+  self.packages.findSomeRev? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
 
 /-- Add a module facet to the workspace. -/
 def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=

src/lake/tests/order/Y.lean

@@ -0,0 +1 @@
+def main := IO.println "root"

src/lake/tests/order/bar/Y.lean

@@ -0,0 +1 @@
+def main := IO.println "foo"

src/lake/tests/order/bar/lakefile.lean

@@ -1,7 +1,8 @@
 import Lake
 open Lake DSL
 
-package bar
-
-lean_lib X where
+package bar where
   moreLeanArgs := #["-DmaxHeartbeats=555000"]
+
+lean_lib X
+lean_exe Y

src/lake/tests/order/foo/Y.lean

@@ -0,0 +1 @@
+def main := IO.println "bar"

src/lake/tests/order/foo/lakefile.lean

@@ -1,7 +1,8 @@
 import Lake
 open Lake DSL
 
-package foo
+package foo where
+  moreLeanArgs := #["-DmaxHeartbeats=555000"]
 
-lean_lib X where
-  moreLeanArgs := #["-DmaxHeartbeats=111000"]
+lean_lib X
+lean_exe Y

src/lake/tests/order/lakefile.lean

@@ -1,15 +1,19 @@
 import Lake
 open Lake DSL
 
-package order
+package order where
+  moreLeanArgs := #["-DmaxHeartbeats=666000"]
+
+lean_exe Y
+
 require foo from "foo"
 require bar from "bar"
 
-lean_lib A.B where
-  moreLeanArgs := #["-DmaxHeartbeats=333000"]
+lean_lib A where
+  moreLeanArgs := #["-DmaxHeartbeats=222000"]
 
 lean_lib A.B.C where
   moreLeanArgs := #["-DmaxHeartbeats=444000"]
 
-lean_lib A where
-  moreLeanArgs := #["-DmaxHeartbeats=222000"]
+lean_lib A.B where
+  moreLeanArgs := #["-DmaxHeartbeats=333000"]

src/lake/tests/order/test.sh

@@ -7,12 +7,16 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 # Tests that the order in which libraries are declared and required
 # is properly preserved and effects which configuration is used for a module.
+# Later packages and libraries in the dependency tree shadow earlier ones.
+# https://github.com/leanprover/lean4/issues/2548
 
 $LAKE update
 $LAKE build +A -v | grep 222000
 $LAKE build +A.B -v | grep 333000
 $LAKE build +A.B.C -v | grep 333000
-$LAKE build +X -v | grep 111000
+$LAKE build +X -v | grep 555000
+$LAKE build +Y -v | grep 666000
+$LAKE exe Y | grep root
 
 # Tests that `lake update` does not reorder packages in the manifest
 # (if there have been no changes to the order in the configuration)