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:
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)
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.)
@Erik Martin-Dorel I'm not sure what you are asking... usage.png
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:
maybe only private repositories make this fraction increase?
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.
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).
Anyway, Matthieu has applied for the open source program for the Coq organization but AFAIK we haven't heard back from them yet.
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?
I'll try to dig it up again.
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)
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 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.
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)
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...)
argh, potentially more licensing issues
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
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…
@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.
The math-comp Docker images should provide the same frequent update cycle soon (work-in-progress by @Erik Martin-Dorel).
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).
@Beta Ziliani You forgot to switch from the base image to the coq one.
oh sorry, should that be coqorg/coq:dev:latest
?
OK, I know that's not how to refer to it. coqorg/coq:latest
?
@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
many thanks Erik!
Last updated: Jun 04 2023 at 19:30 UTC