Lake fails to parse reservoir json correctly when the server responds with an error

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In Lean 4.24.0, lake executes something like

$ curl -s -L --retry 3 https://reservoir.lean-lang.org/api/v1/packages/leanprover-community/mathlib
{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}

for which the output is not valid json (presumably because --retry is concatenating).

At HEAD I believe it executes

$ curl -s -L --retry 3 https://reservoir.lean-lang.org/api/v1/packages/leanprover-community/mathlib-w "%{stderr}%{json}\n"

which writes

{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}

to stdout, and

{"certs":"","conn_id":0,"content_type":"application/json; charset=utf-8","errormsg":null,"exitcode":0,"filename_effective":null,"ftp_entry_path":null,"http_code":500,"http_connect":0,"http_version":"2","local_ip":"172.28.105.251","local_port":45832,"method":"GET","num_certs":0,"num_connects":0,"num_headers":11,"num_redirects":0,"num_retries":3,"proxy_ssl_verify_result":0,"proxy_used":0,"redirect_url":null,"referer":null,"remote_ip":"63.176.8.218","remote_port":443,"response_code":500,"scheme":"https","size_download":58,"size_header":379,"size_request":136,"size_upload":0,"speed_download":5,"speed_upload":0,"ssl_verify_result":0,"time_appconnect":0.000000,"time_connect":0.000000,"time_namelookup":0.000000,"time_posttransfer":0.000176,"time_pretransfer":0.000157,"time_queue":0.000043,"time_redirect":0.000000,"time_starttransfer":10.181835,"time_total":10.181922,"tls_earlydata":0,"url":"https://reservoir.lean-lang.org/api/v1/packages/leanprover-community/mathlib","url.fragment":null,"url.host":"reservoir.lean-lang.org","url.options":null,"url.password":null,"url.path":"/api/v1/packages/leanprover-community/mathlib","url.port":"443","url.query":null,"url.scheme":"https","url.user":null,"url.zoneid":null,"url_effective":"https://reservoir.lean-lang.org/api/v1/packages/leanprover-community/mathlib","urle.fragment":null,"urle.host":"reservoir.lean-lang.org","urle.options":null,"urle.password":null,"urle.path":"/api/v1/packages/leanprover-community/mathlib","urle.port":"443","urle.query":null,"urle.scheme":"https","urle.user":null,"urle.zoneid":null,"urlnum":0,"xfer_id":3,"curl_version":"libcurl/8.16.0 OpenSSL/3.5.2 zlib/1.3.1 brotli/1.1.0 zstd/1.5.7 libidn2/2.3.8 libpsl/0.21.2 libssh2/1.11.1 nghttp2/1.64.0 nghttp3/1.8.0 librtmp/2.3 OpenLDAP/2.6.10"}

to stderr.)

Context

I ran lake init pkg math

Steps to Reproduce

1. Cause a global AWS outage
2. Run lake init pkg math

Expected behavior: Widespread chaos, reported correctly as a server error by lake

Actual behavior: Widespread chaos, reported incorrectly as invalid json

The logs with --verbose are:

31.27 trace: created create-release CI workflow at '.github/workflows/create-release.yml'
31.29 trace: .> git init -q
31.29 info: downloading mathlib `lean-toolchain` file
31.52 trace: .> curl -s -S -f -o lean-toolchain -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain
31.52 info: Pkg: no previous manifest, creating one from scratch
31.52 trace: Pkg: updating 'mathlib' with {}
88.50 error: leanprover-community/mathlib: Reservoir lookup failed; server returned invalid JSON: offset 58: expected end of input
88.50 trace: leanprover-community/mathlib: Reservoir responded with:
88.50 {"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}{"error":{"status":500,"message":"Internal server error"}}
88.50 error: leanprover-community/mathlib: could not materialize package: this may be a transient error or a bug in Lake or Reservoir

Versions

v4.22.0, v4.23.0, v4.24.0

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing lake init pkg math during a server error and trace the Reservoir lookup that reports invalid JSON. Use the verbose output and concatenated responses as the expected failure case; done means Lake reports the server error correctly instead of invalid JSON.