!bench failed during download of pr release

Stream: mathlib4

[Thomas Murrills]

On #7831, I’m testing out a lean4 pr release in mathlib, and it seems to have run into an error while downloading the release. Excerpted from the failure message (see PR):

info: downloading component 'lean'
error: could not download file from 'https://github.com/leanprover/lean4-pr-releases/releases/expanded_assets/pr-release-2728' to '/home/velcom/.elan/tmp/_2astaa07f4xkl6n_file'
info: caused by: error during download
info: caused by: [35] SSL connect error (Recv failure: Connection reset by peer)

(I tried just commenting !bench again, but to no avail.)

Interestingly, this isn’t a general problem: another PR using a lean4 pr release benched just fine just before (#7830).

[Scott Morrison]

Can you install the toolchain locally?

If no, just regenerate the toolchain by touching the Lean4 brnach.

If yes, we might have to summon Sebastian as it would be a speedcenter issue.

[Thomas Murrills]

I’ll try in a bit, as I’m on mobile right now. :) I will note that the mathlib4 PR built just fine with the toolchain (but I’m not sure if that’s the same machine that made the toolchain or what’s going on behind the scenes)

[Thomas Murrills]

Yep, turns out I can install this toolchain locally with no problem.

[Scott Morrison]

Oh, but you didn't push anything in between running !bench, so it is just using the cached failure. Push an empty commit and try again.

[Thomas Murrills]

(For the record, just redoing the bench like this worked; I guess it just needed a jolt. :) )