Stream: Coq Platform devs & users

Topic: ci


view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:54):

I'm not sure I've followed the platform in full, but certainly it needs to be coordinated with the CI and build team

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:55):

I'm getting a feeling [I could be wrong] that the platform may develop its own solutions that would be redundant with some other solutions on the CI / build arena

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:55):

This kind of coordination is very hard tho

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:55):

Well, I'm supposed to be part of the three teams so I can act as a coordinator.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:55):

People is much happier doing their own stuff, instead of discussing with others and eventually told what to do :)

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:56):

Yup, we should try to coordinate, even if we fail

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:56):

But the idea of having the platform developed in a separate repo (which BTW you were the one to propose initially) is to leave more flexibility to the Coq dev team.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:57):

Sure, I am mostly concerned about the technical aspects of the platform

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:57):

FTR, those technical aspects are likely to still evolve very very much

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:57):

even beyond the first alpha release of the platform

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:57):

so indeed the platform should be fully indepedent

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:57):

but be careful not to redo for example parts of the build system

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:58):

well the technical part that I'm concerned with seems pretty stable to me tho

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:58):

and being involved in both the Coq and the OCaml platform projects, I think it should help me have a pretty broad view

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:58):

there are quite a few todos on that side

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:58):

but not a "paradigm shift" I think

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:58):

Well, in any case, the main departure point for the Coq platform from the technical point of view was to use opam, contrary to what is done today.

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:59):

So I guess you can tell this is an improvement.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:00):

Is the OCaml platform going to use opam?

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:00):

Well, as I said, everything is still in a moving state. But it is one of the most credible option, yes.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:01):

Regarding the OCaml platform, we are in close contact with Anil from OCamllabs

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:02):

So coordinating with the main tool maintainers should likely work out.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:02):

[moving this to a new thread]

So @Théo Zimmermann , actually, with the tooling we have, there should be no difference w.r.t. the Coq and OCaml platform actually [in the technical sense] ?

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:03):

It looks like we did it at the same time but with a slighly different name. Let me adjust to use your naming.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:03):

Only thing that seems a bit in the air is what would be the plan for binary distribution like in Windows, we have this package format for jsCoq that would work pretty well for that, would need just a bit more of work to setup the dockerized build setup, CI templates, etc...

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:04):

Emilio Jesús Gallego Arias said:

So Théo Zimmermann , actually, with the tooling we have, there should be no difference w.r.t. the Coq and OCaml platform actually [in the technical sense] ?

Well that was indeed the idea for working on the two at once, at least originally. We'll see how things turn out.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:05):

I'm pretty convinced that should work well, provide coordination challenges can be solved

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:05):

Emilio Jesús Gallego Arias said:

Only thing that seems a bit in the air is what would be the plan for binary distribution like in Windows, we have this package format for jsCoq that would work pretty well for that, would need just a bit more of work to setup the dockerized build setup, CI templates, etc...

That's something that I need to get back to. I haven't looked at it yet, so I cannot really comment.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:06):

So maybe something interesting to know now is what kind of CI / build platform is considered a good choice for Win + Platform

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:06):

Did you folks discuss that yet?

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:07):

What are the limits for Azure / GH actions?

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:07):

I'd like to ged rid of the VM workers ASaP

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:07):

My own impressions is that GH action is an excellent platform, with their 6h timeouts!

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:07):

Oh that sounds pretty good

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:08):

I may split the windows build script in 3 phases [deps, Coq, packages] and add a GH action

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

But, I haven't made myself very clear to our main experimentator (Antonin) who has first used AppVeyor then Travis.

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:08):

Yup, I think Azure/GH Actions is by far the best Win platform

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

Not surprising given that it is provided by Microsoft :P

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:09):

In fact both have the same backend, but somehow I find Azure's lang a bit more understandable for me

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 13:09):

Well, gitlab is also providing native windows stuff, but I guess indeed Microsoft's own platform is a better choice for now

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:10):

I too prefer the configuration language of Azure. However, the integration with GitHub is much better for Actions.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:10):

And the Azure website is a bit complex to browse.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:10):

And I'm not sure the limits are the same. It seems to me that GH Actions might be more generous.

view this post on Zulip Enrico Tassi (Dec 18 2020 at 20:33):

I think I've finished the ci pr, it tests the platform on linux, mac and windows, builds the win64 installer and an experimental snap for linux (uploading to the snap store still fails, and it's large, but is a start).

This pipeline worked, logs and artifacts will stay there for 5 days.
@Michael Soegtrop there are some commits of general interest you may want to review, and the there is a bug wit COQREGTEST on OSX I can't really debug (see the comments in the ci.yml file).

I think I'll merge all commits but the last one (the snap one) next week on the v8.13 branch.

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 20:35):

Many thanks - I will review all the changes. I also have some fixes to the installer generator I will merge over. I just managed to build 64 bit CompCert on 32 bit cygwin - the last missing piece for the 32 bit Windows installer.

view this post on Zulip Michael Soegtrop (Dec 29 2020 at 12:25):

@Enrico Tassi : one question on the smoke test job: Looking at (https://github.com/coq/platform/runs/1621612669?check_suite_focus=true) the CD C:\installer looks bogus. The artifact seems to be downloaded to D:\a\platform\platform and there is a The system cannot find the path specified. error which I think comes from that. Should it be removed or did you have different intentions?

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:21):

It is very fishy, since later coqc.exe runs... Apparently it works, but it is a miracle.

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:21):

The doc of https://github.com/actions/download-artifact tells we can specify a path

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:27):

I also suspect that, on windows worker, things are not exactly as in linux (most examples are on linux, but I went trough quite a few trial/error in specifying a path to upload-artifact). Maybe you could instrument the FOR loop so that we know what the error really is about?

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:28):

Do you think it's CD that fails?

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:31):

Anyway, I don't know why I wrote the FOR loop in the first place. This doc https://github.com/actions/download-artifact#download-path-output gives a nice example of how I should invoke the installer, I guess.

view this post on Zulip Enrico Tassi (Dec 29 2020 at 13:34):

Ok, after reading the whole doc, my impression is that even if the code path that prints the path is the one for downloading all artifacts (hence the directory structure) the installer is download in the current working directory (as in the very first example of the doc). Then CD fails, but the FOR loop still runs and picks it up from CWD.


Last updated: Mar 28 2024 at 11:01 UTC