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?) =>

src/lake/Lake/Load/Resolve.lean

@@ -30,7 +30,6 @@ in their Lake configuration file with
 
   require {newName} from
     git \"https://github.com/leanprover-community/{newName}\"{rev}
-
 "
 
 /--

src/lake/Lake/Reservoir.lean

@@ -172,8 +172,9 @@ def uriEncodeChar (c : Char) (s := "") : String :=
 def uriEncode (s : String) : String :=
   s.foldl (init := "") fun s c => uriEncodeChar c s
 
+/-- Perform a HTTP `GET` request of a URL (using `curl`) and return the body. -/
 def getUrl (url : String) (headers : Array String := #[]) : LogIO String := do
-  let args := #["-s", "-L"]
+  let args := #["-s", "-L", "--retry", "3"] -- intermittent network errors can occur
   let args := headers.foldl (init := args) (· ++ #["-H", ·])
   captureProc {cmd := "curl", args := args.push url}
 
@@ -206,9 +207,9 @@ def Reservoir.fetchPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Optio
   let out ←
     try
       getUrl url Reservoir.lakeHeaders
-    catch _ =>
+    catch e =>
       logError s!"{owner}/{pkg}: Reservoir lookup failed"
-      return none
+      throw e
   match Json.parse out >>= fromJson? with
   | .ok json =>
     match fromJson? json with
@@ -220,11 +221,14 @@ def Reservoir.fetchPkg? (lakeEnv : Lake.Env) (owner pkg : String) : LogIO (Optio
         if status == 404 then
           return none
         else
-          logError s!"{owner}/{pkg}: Reservoir lookup failed: {msg}"
-          return none
+          error s!"{owner}/{pkg}: Reservoir lookup failed: {msg}"
     | .error e =>
+      errorWithLog do
       logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned unsupported JSON: {e}"
-      return none
+      logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}"
+      failure
   | .error e =>
+    errorWithLog do
     logError s!"{owner}/{pkg}: Reservoir lookup failed; server returned invalid JSON: {e}"
-    return none
+    logVerbose s!"{owner}/{pkg}: Reservoir responded with:\n{out.trim}"
+    failure

src/lake/Lake/Util/Log.lean

@@ -130,9 +130,9 @@ protected def LogEntry.toString (self : LogEntry) (useAnsi := false) : String :=
   if useAnsi then
     let {level := lv, message := msg} := self
     let pre := Ansi.chalk lv.ansiColor s!"{lv.toString}:"
-    s!"{pre} {msg.trim}"
+    s!"{pre} {msg}"
   else
-    s!"{self.level}: {self.message.trim}"
+    s!"{self.level}: {self.message}"
 
 instance : ToString LogEntry := ⟨LogEntry.toString⟩
 
@@ -401,7 +401,7 @@ from an `ELogT` (e.g., `LogIO`).
   [Monad m] [MonadLiftT BaseIO m] [MonadLog m] [MonadFinally m] (x : m α)
 : m α := do
   let (out, a) ← IO.FS.withIsolatedStreams x
-  unless out.isEmpty do logInfo s!"stdout/stderr:\n{out}"
+  unless out.isEmpty do logInfo s!"stdout/stderr:\n{out.trim}"
   return a
 
 /-- Throw with the logged error `message`. -/

src/lake/Lake/Util/Proc.lean

@@ -18,9 +18,9 @@ def mkCmdLog (args : IO.Process.SpawnArgs) : String :=
   [Monad m] (out : IO.Process.Output) (log : String → m PUnit)
 : m Unit := do
   unless out.stdout.isEmpty do
-    log s!"stdout:\n{out.stdout}"
+    log s!"stdout:\n{out.stdout.trim}"
   unless out.stderr.isEmpty do
-    log s!"stderr:\n{out.stderr}"
+    log s!"stderr:\n{out.stderr.trim}"
 
 @[inline] def rawProc (args : IO.Process.SpawnArgs) (quiet := false) : LogIO IO.Process.Output := do
   withLogErrorPos do

src/lake/tests/online/test.sh

@@ -8,7 +8,12 @@ export ELAN_TOOLCHAIN=test
 ./clean.sh
 # Tests requiring a package not in the index
 ($LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
-  grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir"
+  grep --color "package not found on Reservoir"
+# Tests a request error
+(RESERVOIR_API_URL=example.com $LAKE -f bogus-dep.toml update 2>&1 && exit 1 || true) |
+  grep --color "server returned invalid JSON"
+(RESERVOIR_API_URL=example.com $LAKE -f bogus-dep.toml update -v 2>&1 && exit 1 || true) |
+  grep --color "Reservoir responded with"
 
 ./clean.sh
 $LAKE -f git.toml update --keep-toolchain