Gaëtan Gilbert (Aug 18 2020 at 11:41): Gaëtan Gilbert (Aug 18 2020 at 11:41):How does benching work nowadays? for https://github.com/coq/coq/pull/12738
Pierre-Marie Pédrot (Aug 18 2020 at 11:42):You have to push a dedicated commit atop of your PR and run the bench manually in the ensuing CI.
Pierre-Marie Pédrot (Aug 18 2020 at 11:42):Ideally the PR adding the bench infra should be merged so that we don't have to do that by hand.
Pierre-Marie Pédrot (Aug 18 2020 at 11:43):(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.)
Pierre-Marie Pédrot (Aug 18 2020 at 11:44):The commit can be cherry-picked as 40c856044003a8e7313bc20f21b8bc4e8160c8bc
Pierre-Marie Pédrot (Aug 18 2020 at 11:44):and you need to change old_coq_commit to the current master in dev/bench/gitlab.sh
Pierre-Marie Pédrot (Aug 18 2020 at 11:45):then when the CI starts on the relevant PR, there should be a manual job in the first stage
Pierre-Marie Pédrot (Aug 18 2020 at 11:45):just click on the gear button to launch it and there you go.
Jason Gross (Aug 19 2020 at 19:46):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
Jason Gross (Aug 19 2020 at 19:53):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
Gaëtan Gilbert (Aug 19 2020 at 19:54):git ls-remote instead of curl
Pierre-Marie Pédrot (Aug 20 2020 at 09:33):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.
Pierre-Marie Pédrot (Aug 20 2020 at 09:34):But for some reason, sometimes the CI does a full-fledged merge and sometimes it does nothing if the merge is trivial
Pierre-Marie Pédrot (Aug 20 2020 at 09:34):So HEAD^ doesn't always work
Pierre-Marie Pédrot (Aug 20 2020 at 09:34):and the merge-base doesn't work for commits that were merged
Pierre-Marie Pédrot (Aug 20 2020 at 09:35):so, to summarize, I need a command to find a particular commit that works in two cases
Pierre-Marie Pédrot (Aug 20 2020 at 09:36): Gaëtan Gilbert (Aug 20 2020 at 09:37):If the commit message says "bot merge ..." then it's a bot merge
otherwise master (at time of push) is ancestor
Pierre-Marie Pédrot (Aug 20 2020 at 09:38):It's a bit fragile to rely on the commit message, isn't it?
Pierre-Marie Pédrot (Aug 20 2020 at 09:38):It would be easier if the CI always performed a merge, even if trivial
Théo Zimmermann (Aug 20 2020 at 11:47):We can change this if you want.
Gaëtan Gilbert (Aug 20 2020 at 14:09):Pierre-Marie Pédrot said:
It would be easier if the CI always performed a merge, even if trivial
sounds good
Gaëtan Gilbert (Aug 20 2020 at 14:09):@Théo Zimmermann could you do it? I am not familiar with the bot code
Théo Zimmermann (Aug 20 2020 at 16:58):Yes
Pierre-Marie Pédrot (Aug 20 2020 at 17:11):It'd be good after this tweak if we could get a rough version of the bench script in the repo
Pierre-Marie Pédrot (Aug 20 2020 at 17:12):it's a bit cumbersome to have to push commits atop of PRs to run benches currenty
Maxime Dénès (Aug 21 2020 at 09:19):Yes, that's the hope.
Pierre-Marie Pédrot (Aug 24 2020 at 12:20):The bench was merged by mistake and by myself in master...
Pierre-Marie Pédrot (Aug 24 2020 at 12:20):What should be done @Théo Zimmermann @Maxime Dénès ?
Théo Zimmermann (Aug 24 2020 at 12:21):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).
Théo Zimmermann (Aug 24 2020 at 12:22):If bad, feel free to revert the bad commit.
Pierre-Marie Pédrot (Aug 24 2020 at 12:22):Well, it's not fully functional yet for general consumption.
Pierre-Marie Pédrot (Aug 24 2020 at 12:22):It'd need a few tweaks.
Pierre-Marie Pédrot (Aug 24 2020 at 12:22):But it's not far from it.
Pierre-Marie Pédrot (Aug 24 2020 at 12:23):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?
Maxime Dénès (Aug 24 2020 at 12:23):Maybe we can try to go for the tweaks, and if we fail to do quickly, then revert
Pierre-Marie Pédrot (Aug 24 2020 at 12:24):Right. Essentially the only thing to do is to find the two commits needed for comparison.
Pierre-Marie Pédrot (Aug 24 2020 at 12:24):Since we're now merging unconditionally it should be easier.
Pierre-Marie Pédrot (Aug 24 2020 at 12:25):(Also I am not sure we should pick the merge HEAD as the commit for comparison.)
Pierre-Marie Pédrot (Aug 24 2020 at 12:25):(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)
Pierre-Marie Pédrot (Aug 24 2020 at 12:26):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.
Théo Zimmermann (Aug 24 2020 at 12:26):@Pierre-Marie Pédrot The auto-merge commit gives you info on the PR head and the commit it was merged into.
Théo Zimmermann (Aug 24 2020 at 12:26):So it seems to me that this should be the two commits that you need to use.
Pierre-Marie Pédrot (Aug 24 2020 at 12:27):So we just need to parse the message ?
Théo Zimmermann (Aug 24 2020 at 12:27):Yes.
Théo Zimmermann (Aug 24 2020 at 12:27):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)
Théo Zimmermann (Aug 24 2020 at 12:28):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).
Pierre-Marie Pédrot (Aug 24 2020 at 12:35):I am writing a PR for the few changes needed in the bench script
Théo Zimmermann (Aug 24 2020 at 12:35):OK the above PR is now merged.
Last updated: Apr 20 2024 at 07:01 UTC