Allow passing configuration options to the bench command - #372
Conversation
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. |
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.
5366e1a to
bd7ac41
Compare
bd7ac41 to
513232c
Compare
|
@lykimq Thank you very much for the detailed review! I think I addressed all comments with code changes except the last one about the alias for
@Zimmi48 This might be the right way to go. Let's see if anyone has any more feedback first. |
Ping me again when it's time to do it. I'm on vacation so I don't look at my emails but I usually receive push notifications for direct mentions. |
|
Thanks for your work. It is good for me now. :) |
|
Awesome. Thank you so much for all the feedback!
@Zimmi48 I am ready for a test deployment but it's not at all urgent and definitely not worth interrupting your vacation for. Let's pick this back up when you are back? |
|
OK, I'll let you know when I do it. |
|
@Janno I am back from my vacation. I can test-deploy whenever is convenient for you to test. Let me know. |
4 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.)