Stream: Coq devs & plugin devs

Topic: CI these days


view this post on Zulip Talia Ringer (Oct 28 2022 at 16:32):

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

view this post on Zulip Talia Ringer (Oct 28 2022 at 16:35):

Is this still up to date? https://github.com/coq/coq/blob/master/dev/ci/README-users.md looks lengthy, hope I have time

view this post on Zulip Gaëtan Gilbert (Oct 28 2022 at 16:37):

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

view this post on Zulip Talia Ringer (Oct 28 2022 at 16:38):

I see, OK, I'll start as much as I can on Monday and then submit a PR, maybe incomplete

view this post on Zulip Gaëtan Gilbert (Oct 28 2022 at 16:39):

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

view this post on Zulip Talia Ringer (Oct 28 2022 at 16:39):

makes sense, will consider


Last updated: Feb 06 2023 at 18:03 UTC