local bench: feedback?

Stream: lean4

[Siddharth Bhat]

I'm running

/home/bollu/work/lean4-contrib/tests/bench$ temci exec --config speedcenter.yaml --out base.yaml

locally to bench some changes I've made. Unfortunatelytemci provides me no feedback of what's going on, so I've been waiting for half an hour with no indication of what's happening :)

1. How long does a bench take locally, on a reasonably powerful laptop?
2. Can I get feedback from temci about what's going on?

[Siddharth Bhat]

I ade some progress, and I run the bench suite. I do see an error however:

Benchmark 1 out of 10 to 10       [------------------------------------]    0%[14:52:01] Program block no. 3 failed: Not a valid benchmarking program output: sum binary sizes:
Benchmark 10 out of 10 to 10      [####################################]  100%
Report for single runs
...

[Sebastian Ullrich]

There is no good error reporting in this case, you have to run https://github.com/leanprover/lean4/blob/8d10197164830e3e8cbc6ed321e5fe920299c162/tests/bench/speedcenter.exec.velcom.yaml#L14 in your terminal and check what's going wrong yourself