feat: lake: detailed Reservoir fetch error (#6231)

This PR improves the errors Lake produces when it fails to fetch a
dependency from Reservoir. If the package is not indexed, it will
produce a suggestion about how to require it from GitHub.

Closes #5330.

src/lake/Lake/Build/Actions.lean

@@ -63,7 +63,7 @@ def compileLeanModule
     unless txt.isEmpty do
       logInfo s!"stdout:\n{txt}"
   unless out.stderr.isEmpty do
-    logInfo s!"stderr:\n{out.stderr}"
+    logInfo s!"stderr:\n{out.stderr.trim}"
   if out.exitCode ≠ 0 then
     error s!"Lean exited with code {out.exitCode}"
 

src/lake/Lake/Load/Materialize.lean

@@ -104,6 +104,25 @@ structure MaterializedDep where
 @[inline] def MaterializedDep.configFile (self : MaterializedDep) :=
   self.manifestEntry.configFile
 
+def pkgNotIndexed (scope name : String) (rev? : Option String := none) : String :=
+  let (leanRev, tomlRev) :=
+    if let some rev := rev? then
+      (s!" @ {repr rev}", s! "\n    rev = {repr rev}")
+    else ("", "")
+s!"{scope}/{name}: package not found on Reservoir.
+
+  If the package is on GitHub, you can add a Git source. For example:
+
+    require ...
+      from git \"https://github.com/{scope}/{name}\"{leanRev}
+
+  or, if using TOML:
+
+    [[require]]
+    git = \"https://github.com/{scope}/{name}\"{tomlRev}
+    ...
+"
+
 /--
 Materializes a configuration dependency.
 For Git dependencies, updates it to the latest input revision.
@@ -131,9 +150,14 @@ def Dependency.materialize
       else
         error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
     let depName := dep.name.toString (escape := false)
-    let some pkg ← Reservoir.fetchPkg? lakeEnv dep.scope depName
-      | error s!"{dep.scope}/{depName}: could not materialize package: \
-        dependency has no explicit source and was not found on Reservoir"
+    let pkg ←
+      match (← Reservoir.fetchPkg? lakeEnv dep.scope depName |>.toLogT) with
+      | .ok (some pkg) => pure pkg
+      | .ok none => error <| pkgNotIndexed dep.scope depName verRev?
+      | .error e =>
+          logError s!"{dep.scope}/{depName}: could not materialize package: \
+            this may be a transient error or a bug in Lake or Reservoir"
+          throw e
     let relPkgDir := relPkgsDir / pkg.name
     match pkg.gitSrc? with
     | some (.git _ url githubUrl? defaultBranch? subDir?) =>