diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean index 28ae124fc6b0..afb7bdb5384c 100644 --- a/src/lake/Lake/Build/Actions.lean +++ b/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}" diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index 4882a4af9750..66fc3d0fafc2 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/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?) => diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index fcbd367c38e7..9d4888aae026 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/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} - " /-- diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean index f2d72fb47093..2ed295344164 100644 --- a/src/lake/Lake/Reservoir.lean +++ b/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 diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index cc8a5fcd113a..8ed7f1123ce2 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/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`. -/ diff --git a/src/lake/Lake/Util/Proc.lean b/src/lake/Lake/Util/Proc.lean index f40f70d92345..89cc5989eb64 100644 --- a/src/lake/Lake/Util/Proc.lean +++ b/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 diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh index 50ef0c2fd7b6..5c0b11d9361c 100755 --- a/src/lake/tests/online/test.sh +++ b/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