-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Using coqbot to run OCaml benchmarks #288
Comments
To provide some pointers. Here is the place where the endpoint for GitHub webhooks is defined: Lines 204 to 210 in 77b3898
Here is the branch of the Lines 330 to 333 in 77b3898
And here is the place where the bench comments for the Coq repository are currently handled: Lines 432 to 470 in 77b3898
Then, the Lines 2810 to 2830 in 77b3898
|
Great to see this progressing! I've created an issue on the OCaml infrastructure tracker for the eventual deployment of such a bot within OCaml for other uses as well: Regarding the plan above specifically for benchmarking, is Coqbot definitely needed for the configuration triggering via a push? Another approach is to just have a |
We discussed the two options in the call. The advantage of a comment would be that it would trigger the bench for one specific version of a PR whereas the label would signal intent to bench continuously each new version (unless we auto-remove the label, which we could also do, because this is something we support for another use case in Coq). The choice to use a label doesn't mean that we cannot use coqbot to implement the triggering, as coqbot can detect label changes thanks to webhooks. On the other hand, if the goal is just to poll which PRs have this label once per day (without really caring of what was the exact state of the PR when it was added), then the method you propose based on a query would work just fine as well. |
The OCaml project has two benchmark suites. One is Sandmark and the other is the ocurrent bench. The OCaml developers would like to have better support for triggering and reporting these benchmarks, and we have discussed some plans with Tarides engineers Shakthi Kanan, Puneeth Chaganti, and Riku Silvola.
Currently, the way of running Sandmark is to edit a configuration file in https://github.com/ocaml-bench/sandmark-nightly-config, to point to a branch that will then be tested every night. There is no reporting mechanism beyond the Sandmark dashboard itself, and developers use screenshots to report results to PR discussions. The ocurrent bench already has support for triggering a bench on a PR with a label and reporting the results as a status check to GitHub, using the ocaml-benchmarks GitHub app. While this could be improved as well, the priority is first to get something for Sandmark.
Ideally, the OCaml developers (and other interested OCaml projects) would use an OCaml-specific bot / GitHub app for this usage, but we decided that using the coqbot-app /
@coqbot
commands would be fine for a prototype.We also decided that it would be better to maintain and deploy the code for these features directly from the upstream coqbot master branch instead of creating a fork or a new bot that would reuse part of the codebase only, but would need to be maintained separately.
Finally, there are the options of deploying two separate bots running on different servers from the same code but using different configuration files (currently https://github.com/coq/bot/blob/master/coqbot-config.toml), or of deploying a single instance that would be able to manage several GitHub apps. In any case, we will start from the single GitHub app (coqbot-app) and the single deployed instance as things are set up today.
@coqbot bench
command or similar for the OCaml repository to trigger Sandmark bench.The idea is that running this command will make coqbot push a commit to https://github.com/ocaml-bench/sandmark-nightly-config to edit the configuration files to include an entry pointing to the archive for the specific commit on which the bench was requested. The bot could take care of removing the entry when the bench results are posted, which could be done as a later step. BTW, how hard would it be to modify the configuration setup of Sandmark so that entries can be added to separate files? (This would make adding and removing configuration entries much easier, with less risk of conflicts.)
This requires adding a call to
curl
in the Sandmark infrastructure so that the bot receives the information that a benchmark has finished and what it needs to print. We would add a dedicated endpoint to the bot, similar to what was done for the auto-minimization feature. The http request would either contain the full information that needs to be reported on GitHub, or the full information could be retrieved by the bot by fetching additional resources.The text was updated successfully, but these errors were encountered: