Set up a continuous integration

[CohenCyril]

• Travis?
• ci/circleci?
• other?

[strub]

Well, Travis has the benefit to be directly integrated into github.

Le mer. 7 févr. 2018 à 19:34, Cyril Cohen notifications@github.com a écrit :

• Travis?
• ci/circleci?
• other?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/math-comp/analysis/issues/27, or mute the thread https://github.com/notifications/unsubscribe-auth/ABeBnAhApzrxQdSMITI0qJRpfCU0pY-Sks5tSfq2gaJpZM4R9RLD .

[CohenCyril]

and we are lucky not to rely on more than algebra/field in mathcomp, so we should be within the frustrating limit of 50min...

[CohenCyril]

@strub do you mind setting this up?

[strub]

Ok.

Le mer. 7 févr. 2018 à 19:38, Cyril Cohen notifications@github.com a écrit :

@strub https://github.com/strub do you mind setting this up?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/math-comp/analysis/issues/27#issuecomment-363885797, or mute the thread https://github.com/notifications/unsubscribe-auth/ABeBnEKbcDqh_IG07bXR8K7wRI5wx5yCks5tSfu2gaJpZM4R9RLD .

[ejgallego]

For longer builds you want to have a look at what we've done with Circle CI in Coq, in fact once we clean up the scripts I was planning to push it to math-comp. Integration with GH is good.

[strub]

Ok, i’ll have a look.

Le mer. 7 févr. 2018 à 19:43, Emilio Jesús Gallego Arias < notifications@github.com> a écrit :

For longer builds you want to have a look at what we've done with Circle CI in Coq, in fact once we clean up the scripts I was planning to push it to math-comp. Integration with GH is good.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/math-comp/analysis/issues/27#issuecomment-363887099, or mute the thread https://github.com/notifications/unsubscribe-auth/ABeBnHop56STvn4Bgzwwu66IibcuXWCIks5tSfzJgaJpZM4R9RLD .

[CohenCyril]

@ejgallego is it as easy to set up as travis?

[CohenCyril]

@strub Thanks

[ejgallego]

@ejgallego is it as easy to set up as travis?

A bit harder, but can reuse build products from previous stages. So it is possible to build first math-comp and then Feit-Thompson reusing the library from the first build. This is how it looks in Coq now:

https://circleci.com/workflow-run/f304bb71-af15-4df1-a8a9-5d412d0d8d2a

[you'll need an account]

The main downside of Circle is that you have 4 workers for all contributors while in Travis you get 5 for each; I don't think that would be a problem for MC.

[strub]

If you want me to play with Circle CI, some admin. of mathcomp should adhere to a Circle CI plan.

[CohenCyril]

If you want me to play with Circle CI, some admin. of mathcomp should adhere to a Circle CI plan.

@strub done

[strub]

@ejgallego How many containers the Coq project is having?!

[ejgallego]

@strub 4 . The container language is a bit cryptic as it displays as "1" then "3 for OSS projects" Note that documentation is confusing wrt version 1 vs version 2 [you should use v2].

Also, scheduling is a bit confusing at first due to dependencies.

[ejgallego]

Let me know if I can be of help or do you want me to look somewhere.

[strub]

M’y question was more : how much time you need per month for Coq. The 1500 minute limit seems a bit low for a project like Coq.

Le ven. 9 févr. 2018 à 20:21, Emilio Jesús Gallego Arias < notifications@github.com> a écrit :

Let me know if I can be of help or do you want me to look somewhere.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/math-comp/analysis/issues/27#issuecomment-364553711, or mute the thread https://github.com/notifications/unsubscribe-auth/ABeBnCIc0clpbq0rm8sN5619ah2-Ld4Sks5tTKitgaJpZM4R9RLD .

[ejgallego]

M’y question was more : how much time you need per month for Coq. The 1500 minute limit seems a bit low for a project like Coq.

This limit doesn't apply to open source projects as far as we can tell.

[strub]

For me, this is unclear. It seems that they are starting to enforce the limit.

[ejgallego]

I think we discussed that in the Coq channel and the conclusion was that the limit doesn't apply to open source projects, but my memory is not the best maybe @maximedenes @Zimmi48 or @SkySkimmer may remember better.

As far as I can tell, the limit hasn't been enforced in the Coq CI. Note that scheduling of Circle is a bit counterintuitive if you are coming from Travis.

[SkySkimmer]

1500min go by pretty fast for Coq, I think we would have noticed. There was a time I thought we had only 3 jobs and wondered if the 1 (in

The container language is a bit cryptic as it displays as "1" then "3 for OSS projects"

) was out of minutes with the other 3 being unlimited but I never figured out if that was true or just some scheduling artifact with the 4th job not being started where I watched (or some other unrelated thing, who knows).

[SkySkimmer]

For instance https://circleci.com/gh/organizations/SkySkimmer/settings

[strub]

Ok, so I did some research. The pricing plan says nothing about time limits and OSS projects (only that OSS projects get 3 more free containers). Up to October'17, they were not enforcing any time limit (they were only shutting down "abusers"). Starting from October'17, they started to gradually enforce the time limit on private projects. But I wouldn't be surprised that, in 1 or 2 years, they start to enforce it on all projects, the pricing plans being quite clear about the limits.

Anyway, "tant que je gagne, je joue", so I'm currently fine with the current status quo.

[ejgallego]

I agree that the status with CircleCI is clear, but until we don't have a more powerful gitlab + AWS spot instances setup, Circle seems like the easiest way to do a long chain of builds.

I wonder what's missing for Gitlab thou, @SkySkimmer , isn't it the case than gitlab can reuse artifacts from previous builds?

[SkySkimmer]

I wonder what's missing for Gitlab thou, @SkySkimmer , isn't it the case than gitlab can reuse artifacts from previous builds?

It can.

[ejgallego]

Thanks. Yeah so hopefully we can setup a bot someday to push to gitlab and have the testing done there.

[ejgallego]

As I mentioned on gitter I could provide a 32core runner for math-comp/coq if needed.

[Zimmi48]

Yeah so hopefully we can setup a bot someday to push to gitlab and have the testing done there.

That would be definitely worth exploring (sorry for hijacking this thread).

[ejgallego]

@Zimmi48 I don't think that's a hijack at all, I would expect Coq libraries such as mathcomp to use the same system we use in Coq's CI in the medium term.