@coqbot could automatically run benchmarks about bot

[ejgallego]

For now, I will try to improve the Jenkins script, and replace some parts with my own OCaml code; hopefully that code will serve for a future setup.

[ejgallego]

@Zimmi48 see coq/coq-bench#41 and for example coq/coq-bench#40

I do have still plans to work a bit on it; however it is proving difficult to setup even a basic communication with the people at INRIA [then they will complain "you didn't update us on your plans"]

So basically I'd like to rewrite the bench script, integrate it with coqfind the coq package format and add a few whistles; then, in which servers to run it is another question, but IMHO fairly orthogonal.

The new script should produce detailed timing data in a machine-friendly format.

Tho, I was planning to do more extensive testing and indeed bench every commit to the master branch too; but yeah, we need to know what hardware do we have first.

[Zimmi48]

What people at INRIA are you talking about? The IT services or people from the Coq team in Sophia?
The hardware is "pendulum", which is in Sophia IIUC (maybe @gares can confirm).
It is currently a worker for Jenkins but we could make it a worker for GitLab CI. I'd like to avoid messing with Jenkins if I can.
I'd personally like to kill both Jenkins and https://github.com/coq/coq-bench but I'm not going to be spending much time on this, so whoever maintains that stuff will have to decide.
Finally, just a small remark: your pings in coq/coq-bench#41 are pretty useless because https://github.com/coq/coq-bench has zero watchers ATM (a pretty good reason for wanting to kill it IMHO).

[ejgallego]

What people at INRIA are you talking about?

I was a bit kidding, I mean the maintainers of the coq-bench repository which officially seems to be an empty set; we are in the process of fixing that. Thanks for your observation about the zero watchers.

There is a problem there indeed.

I'd personally like to kill both Jenkins and https://github.com/coq/coq-bench but I'm not going to be spending much time on this, so whoever maintains that stuff will have to decide.

Oh interesting, what would you use then? I am not sure Gitlab would work for benchmarking sadly.

[Zimmi48]

Oh interesting, what would you use then? I am not sure Gitlab would work for benchmarking sadly.

I suppose we don't need much: the GitLab CI config can add something that you only run through the interface / API and not on every branch. It would use a special runner (pendulum). It would need a larger timeout (if it can be set by job). It would call the coq-bench script (that you'll have hopefully improved in the meantime). It could store the HTML results as artifacts. Just food for thought.

[Zimmi48]

Given that the benchmarking infrastructure is going to stay on Jenkins, I will only be able to implement the @coqbot support if someone tells me exactly what request I need to do to start a benchmark with parameters. For the reporting back part, I have no idea if Jenkins has webhook support. The other, maybe simpler solution would be that the benchmark script itself sends a request to @coqbot with the message to report back to the PR.

[gares]

Pendulum is in Maxime s office

[ejgallego]

Given that the benchmarking infrastructure is going to stay on Jenkins,

Not necessarily, we could move to any other system if we want. But it should be something that is kinda bar as not to create even more noise.

The script is getting more modular these days an it already runs on travis.

I will only be able to implement the @coqbot support if someone tells me exactly what request I need to do to start a benchmark with parameters. For the reporting back part, I have no idea if Jenkins has webhook support. The other, maybe simpler solution would be that the benchmark script itself sends a request to @coqbot with the message to report back to the PR.

This is doable if you'd like.

[Zimmi48]

The reporting back part is probably the easiest to write: just make the script send a POST request to https://coqbot.herokuapp.com/pendulum/<pr-num> with the text of the comment to post in the body of the request. You just need to add a parameter so that the person starting the script can tell what the PR number is.

[JasonGross]

if someone tells me exactly what request I need to do to start a benchmark with parameters.

I've described in coq/coq-bench#84 how to initiate a job based on just the default values and the PR number. I'm not sure how to initiate such jobs from the web; does someone else know?

For the reporting back part, I have no idea if Jenkins has webhook support. The other, maybe simpler solution would be that the benchmark script itself sends a request to @coqbot with the message to report back to the PR.

I think perhaps the ideal workflow is this:

1. a user adds needs: benchmarking

2. coqbot notices this, adds a comment saying "Benchmarking in progress", sends a request to create a job with default parameters + the PR number + some unique identifier for the "benchmarking in progress" comment to pendulum, and (hopefully) gets back the build number N

3. coqbot updates the comment to say Benchmarking queued, log eventually available [here](https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/$N/console)

4. When the job starts running on pendulum, a request gets sent to coqbot to update the comment (presumably with both the comment id and the build number), which will then read Benchmarking in progress, log available [here](https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/$N/console)

5. Every time a package finishes and there's an updated table available, the bench script sends a request to coqbot to update the comment to be either

   Benchmarking in progress, log available [here](https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/$N/console)
   ```
   $(render_results.ml ....)
   ```
   

   if there are still more packages, or else, if the build has completed, to be

   Benchmarking log available [here](https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/$N/console)
   ```
   $(render_results.ml ....)
   ```
   

   in which case coqbot should remove the needs: benchmarking label. Perhaps the comment should also contain a line like "The following developments failed to install: ..." if any developments failed.

Thoughts on this workflow?

[JasonGross]

Ah, apparently we can trigger builds remotely if we check the relevant box:

Use the following URL to trigger build remotely: JENKINS_URL/view/opam/job/benchmark-part-of-the-branch/build?token=TOKEN_NAME or /buildWithParameters?token=TOKEN_NAME
Optionally append &cause=Cause+Text to provide text that will be included in the recorded build cause.

[Zimmi48]

Workflow sounds reasonable to me.

[JasonGross]

This should be re-opened, as it's not quite done (the coqbot side of things hasn't been implemented)

[Zimmi48]

GitHub is fighting against us!

[Zimmi48]

@JasonGross My intern @jtcoolen is going to start looking into this issue soon. Could you please summarize what you implemented on your side and what needs to be done on @coqbot's side?

[JasonGross]

Sure, though there might be some interaction with @maximedenes' coq/coq#12581 (migrating the bench to gitlab).

First, coq/coq-bench#91 needs to be merged (by @ejgallego? (pending on a more robust CI config?))

What's implemented already (or will be once that PR is merged, but you can see the code in, e.g., coq/coq-bench@24f0b0c):

• When a bench is triggered with the environment variable coq_pr_number set, the fields new_coq_repository, new_coq_commit, old_coq_repository, and old_coq_commit are automatically set (and overwritten); the other variables (new_ocaml_switch, new_coq_opam_archive_git_uri, new_coq_opam_archive_git_branch, old_ocaml_switch, old_coq_repository, old_coq_opam_archive_git_uri, old_coq_opam_archive_git_branch, num_of_iterations, and coq_opam_packages) should have their default values passed.
• If coq_pr_comment_id is set, then whenever an individual package is done, the bench will tell coqbot to update that particular comment by issuing:

curl -X POST --data-binary "${coq_pr_number}${nl}${coq_pr_comment_id}${nl}${comment_text}" "${coqbot_url_prefix}/update-comment"

• If coq_pr_comment_id is not set, then, only once, when the benchmarking completes, the script will tell coqbot to make a new comment by issuing

curl -X POST --data-binary "${coq_pr_number}${nl}${comment_text}" "${coqbot_url_prefix}/new-comment"

• Regardless of whether or not coq_pr_comment_id is set, when the benchmarking is done, the benchmarking script will tell coqbot that the benchmarking run has completed (allowing it to remove a stale needs: benchmarking label) by issuing

curl -X POST --data-binary "${coq_pr_number}" "${coqbot_url_prefix}/benchmarking-done"

What needs to be implemented in coqbot:

• When a user attaches needs: benchmarking to a PR, coqbot should post a comment on the issue saying something like "Benchmarking being queued by @coqbot", retrieve the id of that comment so that it can later edit it, and queue up a benchmarking job setting coq_pr_number and coq_pr_comment_id. Optionally include a link to the benchmarking job status in the comment.
  • Depending on what workflow is desired, coqbot can also either remove needs: benchmarking or replace it with a benchmarking in progress label or just leave the labels alone.
• Listening to the url https://coqbot.herokuapp.com/pendulum/update-comment for a POST request with body of coq_pr_number, newline, coq_pr_comment_id, newline, and then the text of the comment. It should update the comment it previously created with the given id with the new text given to it.
• Listening to the url https://coqbot.herokuapp.com/pendulum/new-comment for a POST request with the body coq_pr_number, newline, comment text. It should create a new comment on the given PR with the given text.
• Listening to the url https://coqbot.herokuapp.com/pendulum/benchmarking-done for a POST request with the body coq_pr_number. It should remove the needs: benchmarking/benchmarking in progress/whatever label from the PR.

[Zimmi48]

OK thanks for the summary. The first step is indeed dependent on whether the bench is running on Jenkins or GitLab, so let's wait to see where coq/coq#12581 goes before addressing this.

[ejgallego]

I will take care of the bench PR ASAP.

[JasonGross]

@Zimmi48 @jtcoolen could you implement the bits of this that involving listening to messages sent by the benchmarking job and commenting on the PR? This should not depend on whether the jobs eventually get run on GitLab or Jenkins?

[Zimmi48]

Given that the bot already reports about jobs run on GitLab CI and will soon do so through the Checks tab, wouldn't it make sense to just use this Checks tab as well to display the results of the benchmark (instead of posting a comment) and to rely on the GitLab webhooks instead of adding new endpoints that the bench script would need to trigger explicitly?

[SkySkimmer]

The comment should make the result table visible without readers having to go through the log

[Zimmi48]

The Checks tab allows displaying whatever we want. It could be the table (auto-extracted from the log).