Benchmarking broken

Stream: mathlib4

[Ruben Van de Velde]

Since #19594 http://speed.lean-fro.org/mathlib4/run-detail/2ef0ba51-4a55-445a-b42d-9ed400f0f048

CC @Kim Morrison

[Kim Morrison]

#19649, hopefully?

[Ruben Van de Velde]

Different error: http://speed.lean-fro.org/mathlib4/run-detail/db4949fc-ca9c-41ef-b00c-8c0606c8c7e3

[Sebastian Ullrich]

I think the correct fix is on nightly-testing: #18354

[Kim Morrison]

Thanks. Trying again with #19656.

[Edward van de Meent]

broken again, seems to be related to the c compiler issue

[Edward van de Meent]

see this run

[Edward van de Meent]

it seems to try to build some executables defined in Batteries, and fails

[Edward van de Meent]

also this run. seems to try to build batteries' runLinter executable after building all of mathlib, and fail doing so?

[Kevin Buzzard]

I wanted to benchmark #20518 (branch blizzard_inc/fieldify_algebraMap), not because I have suspicions, but because it changes the definition of Algebra which is used everywhere, and typeclass inference is (as far as I am concerned) very unpredictable sometimes. Having failed to benchmark it several times because I think the bot was down, I then tried again when it was back up (but got the error The entire run failed. even though there's a green tick) and then I figured I'd try merging master, so I tried both merging this branch into master (#20571) and master into this branch (#20607) but both times I got the message "Found no runs to compare against". Am I doing something wrong or are there still problems with benchmarking?

[Matthew Ballard]

I think the bot just needs to catch up to the commit you branched off of master from.

[Matthew Ballard]

Then they can be manually compared. (Also I would 100% be benchmarking this change too.)

[Edward van de Meent]

btw, should i just merge master into the branch then?