Zulip Chat Archive
Stream: lean4
Topic: speedcenter runs on master
Eric Wieser (Jul 27 2023 at 09:37):
@Sebastian Ullrich, would it be possible to benchmark http://speedcenter.informatik.kit.edu/mathlib4/run-detail/e7b27246-a3e6-496a-b552-ff4b45c7236e/36dc67fae274ac0187a9f20899e41fbc8c903c8e so that it shows up in the graph?
Sebastian Ullrich (Jul 27 2023 at 10:14):
@Eric Wieser It was in the queue at position 14 (which may or may not mean that it gets benchmarked after a finite amount of time). I bumped it up now.
Sebastian Ullrich (Jul 27 2023 at 10:16):
We will hopefully be able to move the speedcenter to FRO infrastructure soon after which we can think about further enhancements and speedups
Eric Wieser (Jul 27 2023 at 11:08):
One thing that currently comes to mind is a that !bench in PRs often prints "nothing to compare against"; perhaps it could benchmark the base commit of a PR as well to ensure that a useful comparison can be made?
Sebastian Ullrich (Jul 27 2023 at 11:11):
Yes, it should bump up the base commit if it's still queued
Eric Wieser (Jul 27 2023 at 11:16):
Are you describing a feature idea or the current expected behavior?
Sebastian Ullrich (Jul 27 2023 at 11:51):
Eric Wieser said:
Are you describing a feature idea or the current expected behavior?
The former
Kevin Buzzard (Jul 27 2023 at 12:46):
@Sebastian Ullrich I've been spamming !bench in my recent PRs because they've been specifically about trying to speed things up. Is this OK?
Kevin Buzzard (Jul 27 2023 at 12:47):
Also is it cheap to run !bench lots of times on one commit, hoping that at some point it will compare it to the last time it diverged from master?
Sebastian Ullrich (Jul 27 2023 at 12:47):
It will delay benchmarking commits on master, but that's already happening even without !bench :)
Sebastian Ullrich (Jul 27 2023 at 12:47):
Kevin Buzzard said:
Also is it cheap to run
!benchlots of times on one commit, hoping that at some point it will compare it to the last time it diverged frommaster?
Yes, though you can also take a look at the queue and search for the master commit there
Eric Wieser (Jul 27 2023 at 12:50):
Is there a reason that only admins can bump an entry up the queue? Can't I do it anyway by making an empty PR on the commit I want as a baseline and running !bench on that?
Notification Bot (Jul 27 2023 at 12:51):
15 messages were moved here from #lean4 > slowness in ring theory file by Eric Wieser.
Eric Wieser (Jul 27 2023 at 12:53):
(maybe this now belongs in #mathlib4 or #general?)
Sebastian Ullrich (Jul 27 2023 at 12:58):
Well that would require touching the Java code
Eric Wieser (Jul 27 2023 at 13:00):
Could we teach !bench to work as a per-commit comment (such as on https://github.com/leanprover-community/mathlib4/commit/758b7d6b19adfc8a0d12be3eafb48507e2e859e5#commitcomment-122855390) without touching the java code?
Sebastian Ullrich (Jul 27 2023 at 13:06):
No, that's somewhere in https://github.com/IPDSnelting/velcom/blob/main/backend/backend/src/main/java/de/aaaaaaah/velcom/backend/listener/github/GithubPrInteractor.java
Last updated: Dec 20 2023 at 11:08 UTC