Allow passing configuration options to the bench command - #372
Conversation
This change technically changes the semantics of the matching because the new algorithm commits to a `Some` branch before it checks permissions and other conditions. If those fail, we go directly to the failure case instead of trying to parse other commands.
This means instead of `bench native` we now have to write `bench coq_native`. This works because arguments keys without values are mapped to `"yes"` values.
No more than pushing a PR where the script sets those variables and having the bot run it. That's why the bot bench command is only allowed for authorized people. |
|
I am undrafting this. Docs live elsewhere, there is no change in security risk, and judging by the contributing guide, I would need to do some serious work for testing that I do not have time for right now. I wonder if it isn't easier to merge it and revert the merge if anything goes wrong. (Assuming the changes look good to everyone.) |
|
The tests should have been fixed in #375. We could merge this other one first if we want to make sure that everything works fine. |
|
If you want, I can also do a test deployment of this branch so that you can test it in production before we merge. |
3 participants
This should allow writing commands like
bench coq_opam_packages="a b c", eliminating the need to push temporary commits for bench configuration. The native bench branch in the parser is now gone as that can be written asbench coq_nativenow.The commits are hopefully self-explanatory. I took the liberty to restructure the comment parsing code (commit #1) because the old code was quite confusing to me and the control flow seemed odd. We now commit to one command and if argument parsing fails or permissions are missing, we go straight to the error case.
The string parsing and the test cases are generated by LLMs. The rest of the code is handwritten.
The PR is a draft for three reasons:
Passing arbitrary variables to the bench job could be a security concern. I don't know the bench code well enough to say. We might want a whitelist?(EDIT: No change in security risk compared to setting arguments via new commits that change bench.sh)alcotest,ppx_expect) and adding them manually still brings me to a point where some kind of token is required. Disabling all that still produces failures in inline tests that I do not understand.The bench command is entirely undocumented and with it being a bit more complex now I think we need documentation.(EDIT: I found the actual place where the bench command is documented (https://github.com/rocq-prover/rocq/wiki/Benchmarking) and since it is not in this repo, it does not affect the actual code changes.)