Hi all, I have a plugin tutorial I want to get in the CI. https://github.com/tlringer/plugin-tutorial or at least the answer guide https://github.com/tlringer/plugin-tutorial/tree/answer-guide. where do I find the process for this? I've never done it since I never manage to catch up to the latest Coq
Is this still up to date? https://github.com/coq/coq/blob/master/dev/ci/README-users.md looks lengthy, hope I have time
the actual process is just
Add a new ci-mydev.sh script to dev/ci; set the corresponding variables in ci-basic-overlay.sh; add the corresponding target to Makefile.ci and a new job to .gitlab-ci.yml so that this new target is run. Have a look at #7656 for an example. Do not hesitate to submit an incomplete pull request if you need help to finish it.
the rest is requirements eg don't break the branch we test etc
I see, OK, I'll start as much as I can on Monday and then submit a PR, maybe incomplete
in this specific case note that we already have a job called plugin:plugin-tutorial
(for the one in the coq repo) so you'll need some other name
makes sense, will consider
Last updated: Oct 13 2024 at 01:02 UTC