Emilio Jesús Gallego Arias (May 29 2020 at 12:54): 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
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
Emilio Jesús Gallego Arias (May 29 2020 at 12:55):This kind of coordination is very hard tho
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.
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 :)
Emilio Jesús Gallego Arias (May 29 2020 at 12:56):Yup, we should try to coordinate, even if we fail
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.
Emilio Jesús Gallego Arias (May 29 2020 at 12:57):Sure, I am mostly concerned about the technical aspects of the platform
Théo Zimmermann (May 29 2020 at 12:57):FTR, those technical aspects are likely to still evolve very very much
Théo Zimmermann (May 29 2020 at 12:57):even beyond the first alpha release of the platform
Emilio Jesús Gallego Arias (May 29 2020 at 12:57):so indeed the platform should be fully indepedent
Emilio Jesús Gallego Arias (May 29 2020 at 12:57):but be careful not to redo for example parts of the build system
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
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
Emilio Jesús Gallego Arias (May 29 2020 at 12:58):there are quite a few todos on that side
Emilio Jesús Gallego Arias (May 29 2020 at 12:58):but not a "paradigm shift" I think
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.
Théo Zimmermann (May 29 2020 at 12:59):So I guess you can tell this is an improvement.
Emilio Jesús Gallego Arias (May 29 2020 at 13:00):Is the OCaml platform going to use opam?
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.
Théo Zimmermann (May 29 2020 at 13:01):Regarding the OCaml platform, we are in close contact with Anil from OCamllabs
Théo Zimmermann (May 29 2020 at 13:02):So coordinating with the main tool maintainers should likely work out.
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] ?
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.
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...
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.
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
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.
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
Emilio Jesús Gallego Arias (May 29 2020 at 13:06):Did you folks discuss that yet?
Emilio Jesús Gallego Arias (May 29 2020 at 13:07):What are the limits for Azure / GH actions?
Emilio Jesús Gallego Arias (May 29 2020 at 13:07):I'd like to ged rid of the VM workers ASaP
Théo Zimmermann (May 29 2020 at 13:07):My own impressions is that GH action is an excellent platform, with their 6h timeouts!
Emilio Jesús Gallego Arias (May 29 2020 at 13:07):Oh that sounds pretty good
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
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.
Emilio Jesús Gallego Arias (May 29 2020 at 13:08):Yup, I think Azure/GH Actions is by far the best Win platform
Théo Zimmermann (May 29 2020 at 13:08):Not surprising given that it is provided by Microsoft :P
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
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
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.
Théo Zimmermann (May 29 2020 at 13:10):And the Azure website is a bit complex to browse.
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.
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.
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.
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?
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.
Enrico Tassi (Dec 29 2020 at 13:21):The doc of https://github.com/actions/download-artifact tells we can specify a path
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?
Enrico Tassi (Dec 29 2020 at 13:28):Do you think it's CD that fails?
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.
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: Jun 03 2023 at 04:30 UTC