Speed center error

Stream: lean4

[Michael Stoll]

I was trying to benchmark #12778 just now. The bot said "The entire run failed." (even though the PR passes CI). When I click on the benchmark results link, I see the following near the beginning:

############
## Stderr ##
############
+ temci exec --config ./scripts/bench/temci-config.yml
[2024-10-09 07:18:15,942] Program block no. 1 failed: Unexpected return code 2, expected 0
[2024-10-09 07:18:15,944] output

and this near the end:

~Mathlib| 10629114116s
Build completed successfully.
env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib

[2024-10-09 07:18:15,950] error

could not execute external process '././.lake/packages/batteries/.lake/build/bin/runLinter'
make: *** [GNUmakefile:16: lint] Error 255

 Performance counter stats for '/tmp/tmpajb_vg3c':

    11,273,900,198      instructions:u

       0.986736516 seconds time elapsed

       1.322799000 seconds user
       1.829209000 seconds sys



Command exited with non-zero status 1
19328.41user 1222.75system 16:09.54elapsed 2119%CPU (0avgtext+0avgdata 3991408maxresident)k
0inputs+11887744outputs (68642major+327574582minor)pagefaults 0swaps

############
## Reason ##
############
The benchmark script terminated with a non-zero exit code (1)!

So it looks like it built Mathlib OK, but failed to lint?
@Sebastian Ullrich

[Sebastian Ullrich]

See #mathlib4 > mathlib4 speedcenter