Add CircleCI template

[liyishuai]

Resolve #1

Todo

• Test compatibility with existing projects
• Update generate.sh

[Zimmi48]

It seems to me that there are differences with the other CI templates that should not be specific to CircleCI like the use of extra-dev and the coinstability testing. Should we also add these to the other templates? cc @erikmd

[erikmd]

Hi @Zimmi48 @liyishuai (sorry for late reply)

It seems to me that there are differences with the other CI templates that should not be specific to CircleCI like the use of extra-dev

Indeed. Actually the extra-dev repo (as well as core-dev) is already included in coqorg/coq:dev based images, while coqorg/coq:latest and other stable images only contain released.

I see no objection of adding extra-dev as well in other templates (e.g. in this PR as well) because I guess the master branch of some coq-community repos could have some dependency in extra-dev (even if maybe this situation did not occur up to now).

and the coinstability testing. Should we also add these to the other templates?

Regarding coinstability testing:

1. if we want to merge that feature, indeed the templates for Travis/CircleCI/GitHub-Actions should be consistent and updated accordingly.
2. However I'm a bit split on merging this feature, because unlike e.g. Coq's CI, this test is not really "reproducible", as (i) the packages to be tested are not specified, (ii) if one of an un-specified coinstallable package is not compatible and no release comes up to fix the build test, basically the build will always fail.

So I'd suggest to:

• add a line opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev in all templates (I suggest to add the --set-default CLI flag)
• remove the code if ! [ -z "$PACKAGES" ]; then opam install -t $PACKAGES; fi (or at least, comment-out this code and document its drawbacks)

[erikmd]

Also, as mentioned in the original post, the script generate.sh should be updated accordingly

[Zimmi48]

Is this yet another subtle difference between this template and the other CI templates?

[erikmd]

I think so… Maybe adding this git submodule part is unneeded for the default coq-community templates? at least for the time being (IMHO the three CI templates should be as close as possible semantically one from the other, and later on other PRs could just as well add features that enhance them, in a row?)

[liyishuai]

Travis CI clones Git submodules by default. I've added submodule for GitHub Actions.

[erikmd]

OK! have you checked that this is exactly that command triggered by Travis for git submodule cloning?

(I'm not very submodule-savvy, but e.g. this blog https://mgalgs.github.io/2014/07/03/git-submodule-update-init-remote-recursive-considered-harmful.html mentions the following commands: git submodule update --init --recursive; git submodule update --remote)

[liyishuai]

Travis uses git submodule update --init --recursive. Should I just drop --remote?

[erikmd]

Maybe yes − this option is documented here:
https://git-scm.com/docs/git-submodule#Documentation/git-submodule.txt---remote ;
it appears to be related to remote-tracking branches (which would be a bit off-topic in the context of CI builds?)

[erikmd]

and this complies with the doc of GitLab CI as well:
https://docs.gitlab.com/ee/ci/git_submodules.html#using-git-submodules-in-your-ci-jobs
so git submodule update --init --recursive seems the way to go

[erikmd]

(actually the GItLab CI page I mentioned suggests two lines)

git submodule sync --recursive
git submodule update --init --recursive

[erikmd]

Good idea, the fact to add an option ci_test_dependants

@liyishuai do you plan to add a similar script in Travis / GitHub Actions templates? or in a later PR.

[liyishuai]

@liyishuai do you plan to add a similar script in Travis / GitHub Actions templates? or in a later PR.

Added to Travis.
For GitHub Actions, we need to:

1. Add option for testing dependants in https://github.com/coq-community/docker-coq-action
2. Configure the option via ci_test_dependants.

[erikmd]

Hi @liyishuai

For GitHub Actions, we need to:

1. Add option for testing dependants in https://github.com/coq-community/docker-coq-action
2. Configure the option via ci_test_dependants.

Good point. So this can be done in a later PR maybe, indeed

[erikmd]

@liyishuai the PR LGTM, thanks! (you just might want to further simplify the opam-list command to PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,), but that's a detail)