Stream: Coq devs & plugin devs

Topic: Bench?


view this post on Zulip Gaëtan Gilbert (Aug 18 2020 at 11:41):

How does benching work nowadays? for https://github.com/coq/coq/pull/12738

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2020 at 11:44):

The commit can be cherry-picked as 40c856044003a8e7313bc20f21b8bc4e8160c8bc

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2020 at 11:45):

just click on the gear button to launch it and there you go.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Aug 19 2020 at 19:54):

git ls-remote instead of curl

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2020 at 09:34):

So HEAD^ doesn't always work

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2020 at 09:34):

and the merge-base doesn't work for commits that were merged

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2020 at 09:36):

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2020 at 09:38):

It's a bit fragile to rely on the commit message, isn't it?

view this post on Zulip Pierre-Marie Pédrot (Aug 20 2020 at 09:38):

It would be easier if the CI always performed a merge, even if trivial

view this post on Zulip Théo Zimmermann (Aug 20 2020 at 11:47):

We can change this if you want.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Aug 20 2020 at 14:09):

@Théo Zimmermann could you do it? I am not familiar with the bot code

view this post on Zulip Théo Zimmermann (Aug 20 2020 at 16:58):

Yes

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Maxime Dénès (Aug 21 2020 at 09:19):

Yes, that's the hope.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:20):

The bench was merged by mistake and by myself in master...

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:20):

What should be done @Théo Zimmermann @Maxime Dénès ?

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 12:22):

If bad, feel free to revert the bad commit.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:22):

Well, it's not fully functional yet for general consumption.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:22):

It'd need a few tweaks.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:22):

But it's not far from it.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:24):

Since we're now merging unconditionally it should be easier.

view this post on Zulip 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.)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:27):

So we just need to parse the message ?

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 12:27):

Yes.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (Aug 24 2020 at 12:35):

I am writing a PR for the few changes needed in the bench script

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 12:35):

OK the above PR is now merged.


Last updated: Oct 13 2024 at 01:02 UTC