Stream: coq-community devs & users

Topic: New Travis limits.


view this post on Zulip Théo Zimmermann (Nov 20 2020 at 09:59):

Travis is backtracking on the unlimited build minutes allowance for public projects. Now, we only have 1000 build minutes / month / organization. It is not much, even for a single project running a cron job with 3 jobs that last 10 minutes every day (30310=900 minutes). So it seems time to migrate all coq-community projects to GitHub Actions even if that means dropping Nix testing for now.

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 09:59):

One question is: should we keep the Travis template or should we remove it?

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:10):

I vote for keeping the template but marking it as deprecated/legacy

view this post on Zulip Christian Doczkal (Nov 20 2020 at 10:11):

I agree with @Karl Palmskog . There are likely projects outside of coq-community that use the templates to set up CI and for whom this restriction is not a problem.

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:13):

right, I actually have personal projects where I will be too lazy to switch, so if nothing else I will do the minimum to maintain the Travis template

view this post on Zulip Christian Doczkal (Nov 20 2020 at 10:14):

@Théo Zimmermann , can you point me (us) to the announcement for this? When does this restriction become effective? I'm asking because graph theory is currently using Travis and takes several minutes, and that isn't counting my internal branch relying on fourcolor (for which there isn't an image yet).

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 10:16):

I've received an e-mail today. Then I went to https://travis-ci.com/organizations/coq-community/plan and saw the build credits (one minute on Linux is worth 10 credits and we have 10,000). Can you access this page?

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 10:17):

And the "purchase date" is Nov 20th, so today.

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 10:20):

Note that we can also reach out to Travis support to apply for OSS credits. But our recent experience applying for the OSS program at GitLab for Coq was pretty bad (application was one or two months ago and we still didn't get anything) so I'm wondering if we should bother for Travis.

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:21):

ah, background is described here seemingly: https://www.theregister.com/2020/11/02/travis_ci_pricng/

view this post on Zulip Christian Doczkal (Nov 20 2020 at 10:22):

Well, reaching out to Travis won't hurt, and it might be good to have this option back eventually. After all, there is no guarantee that other options will remain free indefinitely.

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:23):

if you read the article, it seems they are scaling down anything to do with open source (and the background is likely new owners), so I wouldn't hope for too much

view this post on Zulip Christian Doczkal (Nov 20 2020 at 10:27):

Well, asking could allow us to discern how much this is about limiting "abuse" and how much this is about scaling back support for the OSS community. :shrug:

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:29):

seems dystopian that we might be heading towards a future where open source developers pay out of pocket for infrastructure to sustain something they are giving away (somehow reminds me of many conferences/journals going "author pays")

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:34):

instructions for the Travis OSS credit application are here: https://blog.travis-ci.com/2020-11-02-travis-ci-new-billing

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:35):

also, I'm reading their blogpost as: they give you 10k credits once, and that's it, the plan won't renew monthly unless you apply for OSS credits

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:38):

hmm, if I'm right about the 10k-without-renewal it seems wise to switch low-hanging fruit to GitHub Actions right away

view this post on Zulip Karl Palmskog (Nov 20 2020 at 10:40):

also, this gives a somber perspective on Docker: https://www.theregister.com/2020/10/28/docker_pull_rate_limit_1_november/ -- we should probably look in more detail on GitHub Docker caching (even though we didn't run into issues with pulls yet)

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 11:01):

GitHub proposes more than Docker caching, it proposes a Docker registry that we could use (and transparently switch our GitHub Action users to) if the need appeared.

view this post on Zulip Christian Doczkal (Nov 20 2020 at 11:04):

Okay, graph-theory is doing its first GitHub action CI run. This was really as simple as replacing travis with action, calling generate.sh and pushing. :tada:

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 11:07):

Yeah, it's that simple. That's why my first thought was "we move" rather than "we apply for more credits and we wait".

view this post on Zulip Christian Doczkal (Nov 20 2020 at 11:11):

Well, my approach would be: We move and we apply for credits in case GitHub follows suit after a sudden influx of former Travis users...

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 11:51):

in case GitHub follows suit after a sudden influx of former Travis users...

Ah ah! I don't except this to happen any time soon. GitHub created this generous CI offer quite recently and in particular after they were acquired by Microsoft. They play in a whole different league (not the same pressure for profits and a lot more ways of generating revenues).

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 11:53):

Travis used to be the leader in CI but this went down and down and when GitHub announced their CI/CD service, this was the death sentence IMHO.

view this post on Zulip Christian Doczkal (Nov 20 2020 at 11:55):

I didn't say I'm expecting this to happen. On the other hand, given the pittance of credits we currently have for Travis, just a few projects in coq-community transitioning slowly might churn through those credits really quickly. Do you know of projects who rely on features of Travis that have no analog for GitHub actions (e.g., projects using only Nix for CI)?

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

No, I don't think that there are any projects that only test with Nix.

view this post on Zulip Karl Palmskog (Nov 20 2020 at 12:12):

hmm, I've been using Travis to test both regular make and Dune builds at the same time

view this post on Zulip Théo Zimmermann (Nov 20 2020 at 13:44):

You mean that the Travis templates are more flexible?

view this post on Zulip Christian Doczkal (Nov 20 2020 at 13:47):

One issue is that the Travis app has a simple button to enable weekly or nightly builds (cf. https://github.com/coq-community/templates/issues/77)

view this post on Zulip Karl Palmskog (Nov 20 2020 at 16:00):

Théo Zimmermann said:

You mean that the Travis templates are more flexible?

Dune builds were via opam and make builds were via Nix

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 12:10):

We should hurry up the transition: we have already spent 34% of all our credits!

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 12:10):

I'll try to open a few PRs now.

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 12:34):

I'm taking a break. I've only done Paramcoq for now: https://github.com/coq-community/paramcoq/pull/59

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 18:32):

In https://github.com/coq-community/math-classes/pull/93, I got a 403 error during the dev build. I thought it may be spurious so wanted to re-run it to check but it turns out I can only re-run all jobs at once :sad:

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 18:37):

It's fascinating to discover this very active thread where no GitHub team member has ever replied: https://github.community/t/ability-to-rerun-just-a-single-job-in-a-workflow/17234

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 18:37):

I'll ask them about it via the feedback form since they are usually pretty responsive to those messages.

view this post on Zulip Théo Zimmermann (Nov 22 2020 at 18:47):

Update: we've now spent more than half of our free Travis CI allowance.

view this post on Zulip Karl Palmskog (Nov 22 2020 at 19:27):

I will switch all the projects I maintain later today

view this post on Zulip Christian Doczkal (Nov 22 2020 at 22:49):

Théo Zimmermann said:

Update: we've now spent more than half of our free Travis CI allowance.

Do you have any idea which projects are consuming the bulk of these credits, so that we can prioritize those projects?

view this post on Zulip Karl Palmskog (Nov 22 2020 at 22:53):

looks like: corn, lemma-overloading, aac-tactics (I will fix this), math-classes, bertrand. All of these have daily builds.

view this post on Zulip Karl Palmskog (Nov 22 2020 at 22:53):

I can see everything recent at: https://travis-ci.com/github/coq-community (but maybe not available to people who are not owners)

view this post on Zulip Karl Palmskog (Nov 22 2020 at 22:54):

I think we should decide carefully which projects should have daily builds, e.g., I don't think aac-tactics needs one, since it's in Coq's CI

view this post on Zulip Christian Doczkal (Nov 22 2020 at 23:10):

A single build of corn takes a total time of 2h45. One of the owners might want to disable nightly checking for that one ASAP.

view this post on Zulip Karl Palmskog (Nov 22 2020 at 23:11):

sigh, I didn't see the RegLang PR, just looked at master, can you merge yours?

view this post on Zulip Christian Doczkal (Nov 22 2020 at 23:11):

sure, I thought I create a PR and let you push the button

view this post on Zulip Christian Doczkal (Nov 22 2020 at 23:12):

In any event reglang has no periodic builds, so I actually needed to fix something for the dev build to succeed.

view this post on Zulip Karl Palmskog (Nov 22 2020 at 23:12):

CPP reviewing turned out to be a nightmare, so I think you will have to explicitly ping me in for PRs these days...

view this post on Zulip Christian Doczkal (Nov 22 2020 at 23:17):

@Karl Palmskog , can you disable the nightly for corn in the settings? I suppose everything else can wait until the sun is back up.

view this post on Zulip Karl Palmskog (Nov 22 2020 at 23:18):

@Christian Doczkal OK, cron job for corn is gone.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 00:51):

in fact, I removed all cron jobs I could find

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 08:18):

Still, corn receives PRs / commits quite often and each build takes a lot of minutes, so I've opened https://github.com/coq-community/corn/pull/148 to switch it to GitHub Actions.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 08:20):

I'll stop for now. With the cron jobs disabled and the most resource-intensive projects switched, the other projects should have more time to react.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 08:21):

VsCoq uses Travis but each build is about 1 minute, so it can last a bit longer even if it receives frequent PRs.

view this post on Zulip Christian Doczkal (Nov 23 2020 at 09:05):

Théo Zimmermann said:

I'll stop for now. With the cron jobs disabled and the most resource-intensive projects switched, the other projects should have more time to react.

Yes, I guess we can just check the list of coq-community builds on travis from time to time and notify everyone who shows up in this list.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:07):

somewhat amusing:

4 Unique users who are running builds

A user is anyone who triggers the use of the compute resources you will be charged monthly for.

You exceeded the number of users allowed for your plan. Please switch to a bigger plan

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 18:08):

Oh, wow! So we are already hitting hard limits!?

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:08):

this might be a soft limit

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 18:10):

FTR, I've just changed the Travis GitHub App permissions so that it can only be used on the 30 repositories that have already used it in the past (including those that migrated in case of commits being pushed to other branches).

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 18:10):

This means that new coq-community projects cannot use Travis CI.

view this post on Zulip Théo Zimmermann (Nov 23 2020 at 18:10):

It's probably time to document the Travis template as deprecated.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:11):

I agree.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:15):

is there an obvious way to specify multiple opam files in the Actions CI? This was straightforward for Travis, but not so much now.

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:16):

I have started to split some projects into 2-3 opam files since they make sense to package separately

view this post on Zulip Karl Palmskog (Nov 23 2020 at 18:19):

@Erik Martin-Dorel do you maybe have some example of setting up a project to check several name.opam files with the same Docker image using Docker-Coq-Action? This was something we used with Travis in some cases, so would be nice to retain after migrating away from Travis.

view this post on Zulip Christian Doczkal (Nov 23 2020 at 18:45):

Karl Palmskog said:

somewhat amusing:

4 Unique users who are running builds

A user is anyone who triggers the use of the compute resources you will be charged monthly for.

You exceeded the number of users allowed for your plan. Please switch to a bigger plan

I see the first two lines but not the last. But then, I'm not an owner of the organization. Still, even more amusing ...

view this post on Zulip Erik Martin-Dorel (Nov 23 2020 at 18:55):

Karl Palmskog said:

do you maybe have some example of setting up a project to check several name.opam files with the same Docker image using Docker-Coq-Action? This was something we used with Travis in some cases, so would be nice to retain after migrating away from Travis.

there is a similar feature since https://github.com/coq-community/docker-coq-action/releases/tag/v1.1.0
cf. the doc (https://github.com/coq-community/docker-coq-action#opam_file):

Note-2: if this value is a directory (e.g., .), relying on the custom_script default value, the action will install all the *.opam packages stored in this directory.

do you believe this would be enough for your needs?

view this post on Zulip Karl Palmskog (Nov 24 2020 at 04:43):

unfortunately, the default script does not work well when there are multiple opam files. Basically, one needs to be able to specify both:

view this post on Zulip Théo Zimmermann (Nov 24 2020 at 08:45):

Christian Doczkal said:

Karl Palmskog said:

somewhat amusing:

4 Unique users who are running builds

A user is anyone who triggers the use of the compute resources you will be charged monthly for.

You exceeded the number of users allowed for your plan. Please switch to a bigger plan

I see the first two lines but not the last. But then, I'm not an owner of the organization. Still, even more amusing ...

Actually, I also do not see the last line either (even though I'm an owner) but I see this:

Plan information

Free

Unlimited unique users

view this post on Zulip Christian Doczkal (Nov 24 2020 at 08:54):

@Théo Zimmermann , indeed. Also, it looks like the nosedive of the credit counter has been halted. :+1:

view this post on Zulip Karl Palmskog (Nov 24 2020 at 09:08):

sigh, how are we supposed to test non-Dockerized versions of Coq in CI?

view this post on Zulip Karl Palmskog (Nov 24 2020 at 09:09):

with Travis, I could use Nix and just use a GitHub URL

view this post on Zulip Théo Zimmermann (Nov 24 2020 at 09:09):

Hopefully, @Cyril Cohen will come up with a template soon. In the meantime, maybe take a look at what he did in math-comp.

view this post on Zulip Karl Palmskog (Nov 24 2020 at 09:12):

you mean https://github.com/math-comp/math-comp/blob/master/.github/workflows/nix.yml ? A bit too much to wrap my head around, and also seems to be centered around released Coq versions.

view this post on Zulip Cyril Cohen (Nov 24 2020 at 09:24):

for mathcomp you can substitute with any branch, I am supposed to generalize it to Coq

view this post on Zulip Cyril Cohen (Nov 24 2020 at 09:24):

(any branch in any repo)

view this post on Zulip Cyril Cohen (Nov 24 2020 at 09:24):

(or local directory)

view this post on Zulip Erik Martin-Dorel (Nov 25 2020 at 16:42):

Karl Palmskog said:

unfortunately, the default script does not work well when there are multiple opam files. Basically, one needs to be able to specify both:

OK Karl, so I guess you'll need to provide your custom_script (unless the feature request https://github.com/coq-community/docker-coq-action/issues/22#issuecomment-695803544 would be handy for your use case?)

view this post on Zulip Karl Palmskog (Nov 25 2020 at 16:52):

parameterizing on the "pin script" would help a bit for sure, but the ideal would be to just list the stuff to pin

view this post on Zulip Théo Zimmermann (Nov 25 2020 at 18:15):

OK so, it turns out that my attempt at limiting Travis to projects where it was previously installed made it not run any new build (if I believe what I see on VsCoq).

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:56):

A small update on this:

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:57):

Karl was right: the new free plan is a trial plan. The 10,000 build credits is one time only and the plan expires after a year anyway.

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:57):

Cf. https://blog.travis-ci.com/2020-11-02-travis-ci-new-billing

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 16:57):

Travis claims to have heard from the OSS community but actually haven't announced any change: https://blog.travis-ci.com/oss-announcement

view this post on Zulip Théo Zimmermann (Dec 07 2020 at 17:05):

We have very few projects left using Travis:

view this post on Zulip Théo Zimmermann (Dec 08 2020 at 13:55):

Also, here is a quote from the answer received by someone who asked for Travis open source credits:

At the moment, credit allocation for OSS projects is on hold as per directives from management.
We will provide updates once we get additional approval from management.

view this post on Zulip Karl Palmskog (Dec 08 2020 at 13:57):

thanks, good to know

view this post on Zulip Christian Doczkal (Dec 08 2020 at 14:08):

This is really getting from bad to worse. Makes me wonder whether the money they save for no longer supporting OSS projects makes up for the damage to the companies image...


Last updated: Feb 05 2023 at 14:02 UTC