Building Docker-Coq images more often · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Building Docker-Coq images more often

Beta Ziliani (Sep 28 2020 at 18:39):

Théo Zimmermann said:

Well in fact, we could certainly auto-trigger a build on https://gitlab.com/coq-community/docker-coq every time master is updated (this was not done initially because the build used to be on Docker Hub). There is no garbage collection issue because this is always overriding the same tag on Docker Hub (tag dev, see https://hub.docker.com/r/coqorg/coq/tags). cc Erik Martin-Dorel (seems something worth doing)

If you ever do that, please let us know! :pray:

Erik Martin-Dorel (Sep 29 2020 at 22:43):

Beta Ziliani said:

Théo Zimmermann said:

Well in fact, we could certainly auto-trigger a build on https://gitlab.com/coq-community/docker-coq every time master is updated (this was not done initially because the build used to be on Docker Hub). There is no garbage collection issue because this is always overriding the same tag on Docker Hub (tag dev, see https://hub.docker.com/r/coqorg/coq/tags). cc Erik Martin-Dorel (seems something worth doing)

If you ever do that, please let us know! :pray:

Hi, sorry the for late reply, but as said @Théo Zimmermann, since coqorg/coq images are now fully built and pushed from GitLab CI (using docker-keeper, see https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/Docker.20images.20for.20the.20Coq.20Platform/near/209683530 for details), what you request definitely looks feasible!
maybe we could arrange some video-call with @Théo Zimmermann in the upcoming days to figure out how to plug coqbot and these gitlab repositories? (e.g. next Monday? or at another time)

Erik Martin-Dorel (Sep 29 2020 at 22:46):

BTW I have one further suggestion, and one question to raise:

Given that some other Docker images rely on coqorg/coq:dev (typicallymathcomp/mathcomp:latest-coq-dev (when applicable)), the feature you suggested above could be extended to automatically trigger another pipeline building mathcomp/mathcomp:latest-coq-dev immediately after the pipeline for building coqorg/coq:dev finished?
I realize this month, I received some e-mail from GitLab (excerpt below, maybe some of you also received this and already discussed this topic?) which implies the free tier for GitLab CI will be restricted a bit:

Effective October 1, 2020, GitLab will update the CI/CD minute limit for GitLab.com free tier.
As GitLab has grown over the years, we’re incredibly humbled by the number of users who choose to use our free platform. As the adoption of our free product has scaled, so have the underlying costs to support it. As we are committed to continue to support the free product for the larger community, we need to implement further CI/CD limits on GitLab.com. This change is only applicable to free GitLab.com users—current GitLab.com paid tiers and all self-managed GitLab tiers will remain unchanged.
CI/CD Minutes
We are updating the CI/CD minutes limit in the Free tier to 400 minutes per group per month, with the ability to purchase additional CI/CD minutes at $10 for 1000 minutes (valid for a year). […]

→ out of curiosity, @Théo Zimmermann and @Cyril Cohen, as you have the owner rights on these GitLab organizations, could you take a look at the following URLs to see what is the current quota/usage as of September, 30?

Actually I guess the current quota is already way beyond these 400 minutes, but purchasing 1000 or 2000 minutes for a year looks cheap anyway.
(And IMHO it seems a good plan to use GitLab further for these CI infrastructures, as the .gitlab-ci.yml features are very mature… Just to give a tiny example, the .gitlab-ci.yml inclusion feature (used e.g. in docker-keeper repos, cf. https://gitlab.com/coq-community/docker-coq/-/blob/master/.gitlab-ci.yml#L1) has no GitHub Actions counterpart, for the time being.)

Cyril Cohen (Sep 29 2020 at 23:11):

@Erik Martin-Dorel I'm not sure what you are asking... usage.png

Erik Martin-Dorel (Sep 29 2020 at 23:13):

Thanks @Cyril Cohen! I was asking the _ / 2000 minutes info which is indeed included in your screenshot, thanks. but I'm puzzled to see that it is 0 minutes :thinking:

Erik Martin-Dorel (Sep 29 2020 at 23:14):

maybe only private repositories make this fraction increase?

Théo Zimmermann (Sep 30 2020 at 09:38):

Hi @Erik Martin-Dorel, yes let's plan a meeting next week. Monday is possible although I will probably have another meeting with @Hugo Herbelin and @Emilio Jesús Gallego Arias on Monday but I don't know yet at what time.

Théo Zimmermann (Sep 30 2020 at 09:41):

Your question on pipeline minutes is indeed something that we have discussed with Coq developers during some recent Coq Calls. According to information that I found on GitLab's forum, it was planned to also apply to public repositories but may not be immediate because of the bug that makes public repositories not show any pipeline usage (as shown by Cyril).

Théo Zimmermann (Sep 30 2020 at 09:41):

Anyway, Matthieu has applied for the open source program for the Coq organization but AFAIK we haven't heard back from them yet.

Gaëtan Gilbert (Sep 30 2020 at 09:42):

According to information that I found on GitLab's forum, it was planned to also apply to public repositories

I didn't see anything conclusive that way, do you have a reference?

Théo Zimmermann (Sep 30 2020 at 09:42):

I'll try to dig it up again.

Théo Zimmermann (Sep 30 2020 at 09:46):

The limits are applicable for public projects as well, as highlighted in the FAQ.

(https://forum.gitlab.com/t/ci-cd-minutes-for-free-tier/40241/15)

Théo Zimmermann (Sep 30 2020 at 09:49):

I believe that due to a known bug 3, public projects’ CI minutes are not being counted. This gives us some time to think through the open source contribution story in regards to the new CI minute change. That means that only Free accounts with private projects will see an immediate impact to their CI minutes.

(https://forum.gitlab.com/t/ci-cd-minutes-for-free-tier/40241/43)

Théo Zimmermann (Sep 30 2020 at 10:05):

Théo Zimmermann said:

Anyway, Matthieu has applied for the open source program for the Coq organization but AFAIK we haven't heard back from them yet.

Actually, we've just been upgraded apparently.

Erik Martin-Dorel (Sep 30 2020 at 12:16):

Théo Zimmermann said:

Hi Erik Martin-Dorel, yes let's plan a meeting next week. Monday is possible although I will probably have another meeting with Hugo Herbelin and Emilio Jesús Gallego Arias on Monday but I don't know yet at what time.

OK, no worries! (I had proposed this day as I have otherwise 6h teaching slots roughly all other days on next week; so just let me know by PM when you have more insight on your schedule)

Erik Martin-Dorel (Sep 30 2020 at 12:23):

Théo Zimmermann said:

Théo Zimmermann said:

Anyway, Matthieu has applied for the open source program for the Coq organization but AFAIK we haven't heard back from them yet.

Actually, we've just been upgraded apparently.

Great! and do you think one should apply likewise for gitlab.com/coq-community and gitlab.com/math-comp from now on? or would you say there is no hurry, given the "known bug" you mentioned (https://gitlab.com/gitlab-org/gitlab/-/issues/243722), related to this MR (https://gitlab.com/gitlab-com/www-gitlab-com/-/merge_requests/63307)?

This FAQ update acknowledges that the bug means that public projects will not see a change in CI minutes, and that we will make an additional announcement and provide at least 8 weeks notice, as per @kencjohnston's comment in the bug: https://gitlab.com/gitlab-org/gitlab/-/issues/243722#note_416630076

BTW according to https://about.gitlab.com/solutions/open-source/program/ the conditions of the open source program are:

Requirements

OSI-approved open source license (https://opensource.org/licenses/category) -- All of the code you host in this GitLab group must be published under OSI-approved licenses

Non-profit -- Your organization must not seek to make a profit. Accepting donations to sustain your efforts is ok

Publicly visible -- Your GitLab.com group or self-hosted instance and your source code must be publicly visible and publicly available

− and the program would thus provide 50,000 CI minutes.

(In particular I don't know if the "OSI-approved" criterion would raise a concern for some licenses such as CeCILL-B...)

Karl Palmskog (Sep 30 2020 at 12:44):

argh, potentially more licensing issues

Karl Palmskog (Sep 30 2020 at 12:46):

we also have some documentation under CC-0, which is not OSI, so it all comes down to how lenient they are with the licensing criteria stuff

Erik Martin-Dorel (Sep 30 2020 at 12:56):

Hi @Karl Palmskog, yes indeed.
But regarding CC-0, even if it is not technically an "open source license" (it is rather a "copyright waiver" than a license as mentions e.g. this thread https://academia.stackexchange.com/questions/116401/publishing-data-under-creative-commons-license-cc0-or-cc-by/116439#116439), I guess it wouldn't raise an issue for a coq-community application to this program, as CC-0 is anyway at the opposite spectrum of copyrighted closed-source licenses…

Théo Zimmermann (Oct 12 2020 at 13:51):

@Beta Ziliani Docker-Coq images are now rebuilt at every push to Coq master. If you wish, you can check the status of the latest build (to see if it has already completed) at https://gitlab.com/coq-community/docker-coq/-/pipelines.

Théo Zimmermann (Oct 12 2020 at 13:51):

The math-comp Docker images should provide the same frequent update cycle soon (work-in-progress by @Erik Martin-Dorel).

Beta Ziliani (Oct 12 2020 at 17:31):

Thanks @Théo Zimmermann ! Unfortunatelly, something is missing or I need more info: "coqc not found". Is it in a particular space I should know? (You can check our .travis.yml file here, and the failing job here).

Théo Zimmermann (Oct 12 2020 at 20:28):

@Beta Ziliani You forgot to switch from the base image to the coq one.

Beta Ziliani (Oct 12 2020 at 20:31):

oh sorry, should that be coqorg/coq:dev:latest?

Beta Ziliani (Oct 12 2020 at 20:41):

OK, I know that's not how to refer to it. coqorg/coq:latest?

Erik Martin-Dorel (Oct 12 2020 at 21:13):

@Beta Ziliani the exact syntax for using docker-coq images is:

coqorg/coq:$tag

and the possible values of $tag are documented here:

in particular, $tag = latest → the latest stable release (Coq 8.12.0)
$tag = dev → the master version of coq

you might also be interested in the Travis CI / GitLab CI / GitHub Actions templates documented here:

https://github.com/coq-community/docker-coq/wiki/CI-setup

Beta Ziliani (Oct 12 2020 at 21:15):

many thanks Erik!

Last updated: Dec 07 2023 at 14:02 UTC