WIP: Docker-based CI

[anton-trunov]

Trying to fix #245. I added https://github.com/math-comp/odd-order to CI. I did a quick hack, so I'd appreciate if someone reviewed this PR.

• In particular, I'd love to learn a good way of finding the source of failure if a library stops compiling with an updated mathcomp version. Right now one would have to scroll back through the log.
• What other libraries should be added to CI? I'd like to have at least https://github.com/imdea-software/fcsl-pcm and https://github.com/coq-community/lemma-overloading, as I'm a maintainer for those (and these are covered by Coq's or coq-community's CI). Also, quickchick, coquelicot, and iris-lambda-rust seem to be good candidates, as those are covered by Coq's CI.

CC @erikmd @ejgallego (and just in case, @Zimmi48).

TODO:

• introduce build stages
• add https://github.com/math-comp/odd-order
• add https://github.com/math-comp/fourcolor
• add https://github.com/imdea-software/fcsl-pcm
• add https://github.com/coq-community/lemma-overloading
• add https://github.com/math-comp/analysis

[ejgallego]

This is a good start, however you should use build stages:

• in build stage "base" build mathcomp and push a docker image math-comp:dev etc... that is docked on top of the Coq one but has math-comp installed. You may need to push an image named with the hash of the commit to avoid races.
• in the test stage, you can indeed then test the proposed CIs in paralell.

That would work well for merging IMHO; once done we could study how to factor the versioning. For now you could use a bash array indexed by Coq version if you need version-specific pins.

[ejgallego]

See the docs at https://docs.travis-ci.com/user/build-stages/share-docker-image/

I am not sure if this would work for pull requests tho, I forgot how the permission model works for this.

[ejgallego]

Yup indeed this won't work for pull requests :S I got used to gitlab where we workaround that.

[erikmd]

@anton-trunov thanks for working on this.
So to sum up, the plan of this PR and #245 is to make Travis build at the same time math-comp/math-comp and most math-comp libs, to have some regression testing feedback within the main repo, like Coq's main repo.

(Afterwards, this could be complemented with some distribution of math-comp stable docker images for which I gave some suggestions in #243, but of course these two things are a bit orthogonal. Also I believe @CohenCyril was also interested in experimenting this stuff)

As suggested by @ejgallego you should definitely use some build stages to implement this, cf. https://docs.travis-ci.com/user/build-stages, and indeed Travis CI does not have a Docker registry per se, so you could try to push to Docker Hub or so, but it also seems to me this wouldn't be possible for fork branches, due to the need for (encrypted) private tokens to login into the registry, which can only be decrypted from upstream branches builds, not fork builds.

However I think this is not blocking to achieve what we want: you could have 2 stages "build" and "test":

• a stage "build" obtained by turning the docker run + docker exec (first part) command into a single docker build --pull -t mathcomp:dev . command, relying on a Dockerfile similar to that of docker-coq-travis-ci-demo-2
• a stage "test" obtained by turning the docker exec (second part) command into docker run -d -i --init --name=OddOrder (…) mathcomp:dev then docker exec OddOrder /bin/bash --login -c "(…)" (and likewise for other libs to test-build).

Then, it is one of two things:

1. either the two jobs benefit from Docker's cache and the mathcomp:dev image will be available
2. or the docker run (…) says Unable to find image 'mathcomp:dev' locally, so you should adapt the configuration to manually enable caching without using a Docker registry, relying for example on the commands docker save and docker load.

FYI there are some references on the net documenting ways to address point 2. above:

• https://stackoverflow.com/a/41975912/9164010
• https://stackoverflow.com/a/35374332/9164010
• http://rundef.com/fast-travis-ci-docker-build
• https://giorgos.sealabs.net/docker-cache-on-travis-and-docker-112.html
• https://medium.com/mobileforgood/patterns-for-continuous-integration-with-docker-on-travis-ci-71857fff14c5 (but this latter reference uses docker build --pull --cache-from "$IMAGE_NAME" --tag "$IMAGE_NAME" . and docker push "${IMAGE_NAME}:${version}" so it requires a Docker registry)

[erikmd]

@ejgallego I guess one of your suggestions (copied below) was dealing with the naming convention of the "mathcomp:dev" image (if it is pushed on Docker Hub at some point) but just to be sure could you give a small example of what you meant here by "bash array indexed by Coq version"?

once done we could study how to factor the versioning. For now you could use a bash array indexed by Coq version if you need version-specific pins.

[ejgallego]

@erikmd thanks a lot for the links! Oh indeed using the cache could be great! It has to be done with care as to trigger the proper rebuild when it is needed, but indeed could work very well in the end.

What I meant about the array is that for example imagine project odd-order that requires a different version for Coq 8.8 and Coq 8.9, then, indeed we could tweak the variables of the matrix to denote Coq version and store the git ref in an array.

[ggonthier]

You should also add math_comp/fourcolor as that's also a stable (and sizeable) development.

[anton-trunov]

Will do. I added a TODO list to the original post trying to summarize all the suggestions. Feel free to edit the list adding new items or removing the ones you'd prefer not to test.

[Zimmi48]

@ejgallego @erikmd If you really want to use stages and push a docker image for math-comp in the first stage, then I strongly encouraged ditching Travis here and using GitLab CI instead. The experience with Coq has been very positive.

[anton-trunov]

I strongly encouraged ditching Travis here and using GitLab CI instead

@Zimmi48 Does one need a Gitlab organization for this?

[erikmd]

@Zimmi48 thanks for your feedback! actually I guess the plan consists in both:

1. building a Docker image of math-comp master only once for each master commit, then publish it on Docker Hub or so, and reuse it for subsequent jobs;
2. building a Docker image of each math-comp PR branch, then reuse it for subsequent jobs.

as point 2. doesn't require to push the first Docker image somewhere (the cache could be used to communicate inter-stages) this approach could be feasible using Travis.

However it's true that GitLab CI's Docker support is excellent (the configuration file obtained in the end would certainly be simpler than with Travis, and point 2. above regarding PRs could also be extended with a docker push or so to keep somewhere the Docker image that passed tests, improving reproducibility in case of failed or successful build), so it could indeed be a fruitful move!

[erikmd]

Hi @ejgallego! you said about the approach of using staged builds with several docker images:

this won't work for pull requests :S I got used to gitlab where we workaround that.

but out of curiosity, do you rely on some dedicated tool for that (related maybe to coqbot), or do you just use a standard GitLab CI feature mentioned in its documentation?

[anton-trunov]

Ok, the docs say that as the first step one should do the following:

In GitLab create a CI/CD for external repo project and select GitHub.

Where do we do this? I guess (@CohenCyril or @gares or @amahboubi) could create a new GitLab organization for this? Or is there some generic org for Coq-related project? Any pointers would be much appreciated.

[CohenCyril]

Where do we do this? I guess (@CohenCyril or @gares or @amahboubi) could create a new GitLab organization for this? Or is there some generic org for Coq-related project? Any pointers would be much appreciated.

@erikmd @anton-trunov @amahboubi @gares Should I create a math-comp group on http://gitlab.inria.fr?

[erikmd]

Should I create a math-comp group on http://gitlab.inria.fr?

@CohenCyril I don't know for sure, but it seemed to me that @Zimmi48's suggestion was to create that group on https://gitlab.com/ to benefit from its GitLab CI runners? (like https://gitlab.com/coq/coq)

[erikmd]

BTW (in anticipation of #243) you could create a mathcomp organization on Docker Hub as well?
(indeed hyphens are not allowed there… but it seems https://hub.docker.com/u/mathcomp is still available)

[Zimmi48]

Indeed, I had not thought of the possibility of using the cache of Travis. In the old days when we started using Travis (almost 2 years ago), it was not possible to share the cache between stages.

[erikmd]

Hi @Zimmi48

Indeed, I had not thought of the possibility of using the cache of Travis. In the old days when we started using Travis (almost 2 years ago), it was not possible to share the cache between stages.

OK! Note anyway that I did not experimented the references mentioned in my comment and in particular if this approach would now be applicable between different stages of the same Travis build.
(And Travis' doc doesn't seem to indicate whether this is the case or not…)

In any case, relying on gitlab.com CI seems a good choice.

BTW @Zimmi48 @ejgallego are you aware of specific limitations regarding the CI time of standard runners on gitlab.com CI?

[ejgallego]

BTW @Zimmi48 @ejgallego are you aware of specific limitations regarding the CI time of standard runners on gitlab.com CI?

No time limitations that should be relevant for math-comp.

Indeed I am not sure how caches do work wrt stages.

[ejgallego]

Caches do seem to work well with stages; another note: gitlab's CI registry allows to get a deploy-only token for read-only access.

[CohenCyril]

@CohenCyril I don't know for sure, but it seemed to me that @Zimmi48's suggestion was to create that group on https://gitlab.com/ to benefit from its GitLab CI runners? (like https://gitlab.com/coq/coq)

Done: https://gitlab.inria.fr/math-comp

EDIT: Sorry! I did not read carefully. Mistake corrected

[erikmd]

Regarding Emilio's answer to my question about GitLab CI time limitations

No time limitations that should be relevant for math-comp.

I've looked at https://about.gitlab.com/solutions/github/ and https://about.gitlab.com/pricing/#gitlab-com and it's not clear for me if we'd benefit from 2,000 CI pipeline minutes or 50,000 CI pipeline minutes…

Out of curiosity, could @Zimmi48 or @ejgallego take a look at the following page to see if that info would be available for https://gitlab.com/coq/coq ?
https://gitlab.com/groups/coq/-/pipeline_quota

[ejgallego]

Open source projects have no limitations but no guaranteed shared runners either. In practice it works very well as the on-demand approach means that backlog is caught up quickly.

Also it is fairly easy to add your own runners, in Coq we have a machine that helps in times of reduced worker availability.

[erikmd]

Just not to forget and to follow-up the discussion at the visio meeting, you may want to create an organization at https://gitlab.com/math-comp as well.

(see also that docs link mentioned by @anton-trunov:
https://docs.gitlab.com/ee/ci/ci_cd_for_external_repos/github_integration.html)

Cc @CohenCyril

[Zimmi48]

Indeed, as explained by @erikmd the proposal was to create the organization on gitlab.com not on Inria's GitLab.

[CohenCyril]

@erikmd @Zimmi48 done

[erikmd]

Hi @anton-trunov! did you perform more experiments regarding the migration/setup of mathcomp's CI on GitLab? otherwise I can propose to look at this tonight (relying on the GitLab CI config example that I recently simplified to avoid the sed hack). However, I am not sure I could add additional commits to this PR #256, so maybe it's better to create another PR(?)

[anton-trunov]

@erikmd I was intermittently reading the docs and experimenting with CI on IMDEA's internal Gitlab, since I have the necessary rights there, but I haven't finished yet. Feel free to take over this PR any time, though.

[erikmd]

Thanks @anton-trunov! so I resumed my experiments as well, diving in GitLab's doc and in some examples of CI setup including that of Coq.
Cyril gave me access to the CI-dedicated org https://gitlab.com/math-comp and I expect to have a working configuration for branch builds soon, but I think we'll need Théo and Emilio's help to fully configure the builds for GitHub PRs... I'll let you informed ASAP.

[Zimmi48]

OK, I might not be very reactive though, but I'll try to help if I can.

[anton-trunov]

Superseded by #266