How does benching work nowadays? for https://github.com/coq/coq/pull/12738
You have to push a dedicated commit atop of your PR and run the bench manually in the ensuing CI.
Ideally the PR adding the bench infra should be merged so that we don't have to do that by hand.
(Also I don't know how to properly get the master branch hash from CI side, so there is one variable that needs to be hardcoded in the patch.)
The commit can be cherry-picked as 40c856044003a8e7313bc20f21b8bc4e8160c8bc
and you need to change old_coq_commit to the current master in dev/bench/gitlab.sh
then when the CI starts on the relevant PR, there should be a manual job in the first stage
just click on the gear button to launch it and there you go.
Also I don't know how to properly get the master branch hash from CI side, so there is one variable that needs to be hardcoded in the patch.
curl -s https://api.github.com/repos/coq/coq/git/refs/heads/master | jq '.object.sha'
?
But you don't want master, do you, you want the base commit of the PR, no?
You probably just want to merge https://github.com/coq/coq-bench/pull/91/files into the script, though, right? This does all the work for you, and communicates with coqbot to boot. You probably just want to remove the lines involving jenkins-cli.jar, which are just for setting the job title
Note that, unfortunately, the coqbot-side infrastructure is not yet in place for displaying benching results, as the bench is sort-of in limbo. I've just asked for the coqbot-side infratructure to be worked on, though, in https://github.com/coq/bot/issues/8#issuecomment-676627854
git ls-remote instead of curl
But you don't want master, do you, you want the base commit of the PR, no?
No, actually, I need to find the head of the branch to be tested before the merge performed by the CI.
But for some reason, sometimes the CI does a full-fledged merge and sometimes it does nothing if the merge is trivial
So HEAD^ doesn't always work
and the merge-base doesn't work for commits that were merged
so, to summarize, I need a command to find a particular commit that works in two cases
If the commit message says "bot merge ..." then it's a bot merge
otherwise master (at time of push) is ancestor
It's a bit fragile to rely on the commit message, isn't it?
It would be easier if the CI always performed a merge, even if trivial
We can change this if you want.
Pierre-Marie Pédrot said:
It would be easier if the CI always performed a merge, even if trivial
sounds good
@Théo Zimmermann could you do it? I am not familiar with the bot code
Yes
It'd be good after this tweak if we could get a rough version of the bench script in the repo
it's a bit cumbersome to have to push commits atop of PRs to run benches currenty
Yes, that's the hope.
The bench was merged by mistake and by myself in master...
What should be done @Théo Zimmermann @Maxime Dénès ?
I have not been following this issue closely, so I have no idea if it's a bad thing or not (except that if it is useful, it would have been better in a separate PR).
If bad, feel free to revert the bad commit.
Well, it's not fully functional yet for general consumption.
It'd need a few tweaks.
But it's not far from it.
Is it better to revert, at the risk of merging it again by mystake, or should we simply commit the tweaks as an additional PR?
Maybe we can try to go for the tweaks, and if we fail to do quickly, then revert
Right. Essentially the only thing to do is to find the two commits needed for comparison.
Since we're now merging unconditionally it should be easier.
(Also I am not sure we should pick the merge HEAD as the commit for comparison.)
(The situation arose recently, where the bench would not be giving the right information since master now contained performance tweaks that were not there in the merge base)
Note that this code is not breaking anything, right now it's mostly sitting there so it's not going to be problematic per se.
@Pierre-Marie Pédrot The auto-merge commit gives you info on the PR head and the commit it was merged into.
So it seems to me that this should be the two commits that you need to use.
So we just need to parse the message ?
Yes.
However, be aware that the first attempt at always creating a merge commit was unsuccessful and is fixed in https://github.com/coq/bot/pull/91 (not yet merged)
I asked @Julien Coolen to test the PR before merging but if it is pressing we can merge now (I'm pretty sure it will work).
I am writing a PR for the few changes needed in the bench script
OK the above PR is now merged.
Last updated: Oct 13 2024 at 01:02 UTC