Stream: Coq devs & plugin devs

Topic: Building Docker-Coq images more often


view this post on Zulip 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:

view this post on Zulip 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)

view this post on Zulip Erik Martin-Dorel (Sep 29 2020 at 22:46):

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

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.)

view this post on Zulip Cyril Cohen (Sep 29 2020 at 23:11):

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

view this post on Zulip 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:

view this post on Zulip Erik Martin-Dorel (Sep 29 2020 at 23:14):

maybe only private repositories make this fraction increase?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Sep 30 2020 at 09:42):

I'll try to dig it up again.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

− 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...)

view this post on Zulip Karl Palmskog (Sep 30 2020 at 12:44):

argh, potentially more licensing issues

view this post on Zulip 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

view this post on Zulip 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…

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (Oct 12 2020 at 20:28):

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

view this post on Zulip Beta Ziliani (Oct 12 2020 at 20:31):

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

view this post on Zulip Beta Ziliani (Oct 12 2020 at 20:41):

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

view this post on Zulip 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

view this post on Zulip Beta Ziliani (Oct 12 2020 at 21:15):

many thanks Erik!


Last updated: Oct 16 2021 at 01:03 UTC