Closed JasonGross closed 4 years ago
Now that pendulum has jq, should we merge this? I've updated the build configuration, so I think merging this won't break anything. Then someone needs to write the coqbot infrastructure to deal with this.
@ejgallego Can you review/approve/merge this? (Or give me permissions?) I believe it's ready for merge.
@ejgallego Can you review/approve/merge this? (Or give me permissions?) I believe it's ready for merge.
@JasonGross I gave you permission [in a kind of hacky way, I need to work more on the setup]
Anyways I'll merge myself as not to delay this more, thanks for the work!
Closes #84 Closes coq/bot#8
Before this can be merged, I need to add
coq_pr_number
andcoq_pr_comment_id
fields to the parameterized build. I'm waiting to do this until I get reviews on / indications of support for this PR.@Zimmi48 please advise on how to talk to coqbot appropriately
For integration in the other direction (step 2 of https://github.com/coq/bot/issues/8#issuecomment-621530793), we need to check off "Trigger builds remotely (e.g., from scripts)" under "Build Triggers", generate an "Authentication Token" and then have coqbot post(?) to
https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/buildWithParameters?token=$TOKEN&cause=coqbot&coq_pr_number=$PR_NUMBER&coq_pr_comment_id=$COMMENT_ID
, I believe.