CircleCI template

[liyishuai]

The script in coq-ext-lib is quite generic. Is it worth a template here?

[Zimmi48]

I guess it would, although the question is whether we want to have just one standard recommendation, or many supported alternatives? (One potential upcoming alternative is GitHub Actions, but none of us has tried yet as far as I am aware.) What made you prefer CircleCI to Travis BTW?

[liyishuai]

CircleCI allows me to run customized testing script within Docker, which is more convenient than sending commands to Docker:

templates/.travis.yml.mustache

Lines 24 to 28 in 70012e3

	docker exec COQ /bin/bash --login -c "
	export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
	set -ex
	sudo chown -R coq:coq /home/coq/${CONTRIB_NAME}
	opam install ${CONTRIB_NAME} -v -y -j ${NJOBS}

In QuickChick we managed to do without Docker, but had to install Coq manually, which takes a long time, and its caching is always out of control.
I've also tried GitHub Actions, resulting in frustrations, as it doesn't support starting from a Coq docker.

[erikmd]

@liyishuai

CircleCI allows me to run customized testing script within Docker, which is more convenient than sending commands to Docker:

But if I understand correctly what you mean by "customized testing script", it seems to me that this feature is directly available the Travis-CI+Docker setup?

I mean, in the suggested template for Travis CI (using docker run), you can definitely put any customized Bash script, e.g. with if-then-else, variables, etc. (cf. e.g. this snippet)

Admittedly, there is a bit of boilerplate (namely the enclosing docker run command) but on the other hand:

• you have more control over the docker run command itself, if e.g. you want to pass extra -v or -e CLI options (cf. related doc)

• the boilerplate itself is not "minimal" in Circle CI itself, as each command is prepended with:

    - run:
        name: Install dependencies
        command: (…)
  

  while it would just be in the Travis-CI+Docker setup:

      : Install dependencies
      (…)
  

  and in the GitLab-CI setup:

    - ': Install dependencies'
    - (…)
  

[erikmd]

As pointed out by @Zimmi48,

the question is whether we want to have just one standard recommendation, or many supported alternatives?

A few thoughts on that:

• if we decide to add the Circle CI config as an official recommended template, the GitLab CI config should probably be added as well (cf. my previous comment)
• the three alternatives considered here (Travis CI, Circle CI and GitLab CI) are very similar (once you know the availability of the underlying Docker images, the conf file is easy to adapt when you are familiar with the syntax of the considered CI platform)
• AFAIK the integration of Travis CI with GitHub is simpler for the moment (e.g. no need to setup a GitLab CI mirror)
• To follow-up @liyishuai's comment I don't know if GitHub plans to make it possible to use Docker images from GitHub Actions… (but when this will be the case, maybe this alternative will be even more natural than Travis CI)
• When a Coq project maintainer wants to pick a CI solution from this repo, maybe it'd be more effective to recommend only two solutions (Nix, and opam+docker-coq) rather than recommending 4 solutions?

Anyway, if the final decision is just to keep these two recommendations as is, note that one might also want to submit a GitLab CI template and a Circle CI template in the respective templates catalog of these platforms themselves? :)

• https://circleci.com/docs/2.0/tutorials/
• https://docs.gitlab.com/ce/ci/examples/

(But I don't know if they would accept incorporating one such template for Coq projects.)

[erikmd]

Also FYI @clarus recently published a nice blog article that elaborates on the Travis-CI+Docker setup:

http://coq-blog.clarus.me/continuous-testing-for-coq-projects.html

[liyishuai]

Now I agree that the Travis boilerplate is no worse than CircleCI, but it should be even better: coq-community/manifesto#70. The current solution is still more complex than existing Languages supported by Travis.

[erikmd]

Hi @liyishuai,
I see what you mean :) but I now remember I had encountered some open issue in the Travis CI project, which would precisely improve on that situation (regarding "custom Docker images)… without needing extra effort from the language maintainers themselves.

So I will post the link in the issue you mention (not here because #1 specifically deals with Circle CI ;)

[Zimmi48]

When a Coq project maintainer wants to pick a CI solution from this repo, maybe it'd be more effective to recommend only two solutions (Nix, and opam+docker-coq) rather than recommending 4 solutions?

Note that the CI service / provider (Travis, GitLab CI, CircleCI, GitHub Actions) and the way it is used (via Docker and opam, or via Nix) are two mostly orthogonal things that could lead to as many as 8 solutions (not counting the many alternatives, such as using an Ubuntu ppa, that have been used in other projects so far).

[Zimmi48]

@liyishuai Following #26, would you like to add a CircleCI template that gets generated whenever circleci is true?

[liyishuai]

Yes I'll try to make one. It would require an extra field in supported_coq_versions formatted as Docker tags.

[erikmd]

Yes I'll try to make one. It would require an extra field in supported_coq_versions formatted as Docker tags.

or maybe some interpolation would be enough? I mean, like this:

templates/.travis.yml.mustache

Line 54 in f4859eb

- COQ_IMAGE=coqorg/coq:{{ version }}

[liyishuai]

templates/.travis.yml.mustache

Line 54 in f4859eb

- COQ_IMAGE=coqorg/coq:{{ version }}

Great I'll use this one.