coq
opam-repository-mingw will be discontinued as of Aug 2021
https://fdopen.github.io/opam-repository-mingw/2021/02/26/repo-discontinued/ Are you aware of this? How does it affect us?
Ah thanks - I didn't see this!
How is the state of INRIA's effort for better OCaml support on Windows?
It wouldn't be much work to fix all packages we need so that they work on Windows on the main opam repo, but I am still using a binary ocaml and opam delivery from that repo. But then I did build this from sources before and could do so again.
We don't depend on depext for cygwin - instead we install all required packages upfront.
I see that this is finished before the repo is out of maintenance.
How is the state of INRIA's effort for better OCaml support on Windows?
This effort was initiated by @yurug, who is not at Inria anymore (he's moved to Nomadic Labs) but he's probably still a member of the board of the OCaml Foundation.
But now, as far as I know, this effort is mostly led by OCaml Labs. Maybe @avsm can inform us of the progress and plans.
Yes, I agree with Théo: @avsm is currently the most knowledgable about this important project.
Yann Régis-Gianas
On Mon, Apr 19, 2021 at 8:43 PM Théo Zimmermann @.***> wrote:
How is the state of INRIA's effort for better OCaml support on Windows?
This effort was initiated by @yurug https://github.com/yurug, who is not at Inria anymore (he's moved to Nomadic Labs) but he's probably still a member of the board of the OCaml Foundation.
But now, as far as I know, this effort is mostly led by OCaml Labs. Maybe @avsm https://github.com/avsm can inform us of the progress and plans.
— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq/platform/issues/92#issuecomment-822691304, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADNQ37KE3UQUM33KMNX2PTTJR2WBANCNFSM4ZLFEX6A .
So how shall we proceed? Wait or just get it done? What needs to be done is:
- fix the opam OCaml packages, so that they work on Windows (cygwin MinGW cross)
- fix all other opam packages we need in the main opam repo - from an opam point of view there is no good reason to keep a separate repo. Opam has sufficient logic to make packages work on all platforms.
- Have some way to create a MinGW on Cygwin cross opam, preferably make this a Cygwin package
Did I forget anything?
Maybe we should do a test of all opam packages and for those which don't compile on Windows set corresponding availability information and then fix those we need.
An update: https://discuss.ocaml.org/t/ann-ocaml-opam-images-for-docker-for-windows/8179 And a related discussion: https://discuss.ocaml.org/t/ocaml-for-windows-installation-confusion/8105
I should have cc-ed @MisterDA since he has kept working on Windows support for OCaml (now at Tarides).
Opam 2.1, soon to be released, will have improved support for Windows. We expect to be able to migrate completely to opam 2.1 and opam-repository, maybe with a few rough edges at the beginning, but it should work. Setting the availability (or non-availability) of packages on Windows is a good start (and iirc the way we envision), but I personally fear people may forget to port and test their packages on Windows. My next step at Tarides is to make ocaml-ci and opam-repo-ci work on Windows so that we may test OCaml projects and the opam repository at scale.
If you have a Docker file building binaries of Coq and packages on Linux, you may want to port it to Windows with the new images, or try writing a pipeline with ocurrent.
If you have a Docker file building binaries of Coq and packages on Linux, you may want to port it to Windows with the new images.
That would be a great way of improving reproducibility indeed! (And speed too, since I expect this should be faster than installing Cygwin every time the pipeline runs.)
It has its pros and cons. Installing Cygwin is quite fast (about 10 min on CI servers) and this way we also test current cygwin. Since (advanced) users are supposed to install it this way, it makes sense to also test it. Since the 10min is not significant compared to the 2..3 hours it takes, I am not sure using docker is really an advantage.
Apologies. I totally missed the previous pings on this issue (my GitHub notifications are flooded, so a direct ping to [email protected] works better if it's important).
@MSoegtropIMC using Docker in this pipeline would let us hook it into further downstream pipelines much more easily. We currently have an ocaml-ci which is zero-configuration for OCaml projects, and extending it to a coq-ci would not be a difficult prospect for individual repositories. Similarly, the opam-repo-ci could also be extended for the Coq repository.
@avsm : I don't say that having docker doesn't make sense at all. I just say that in the main Coq Platform CI we should have tests which are as close as possible to what users experience and this means direct installation of Cygwin in every run. In Coq Platform I want to see breaks by Cygwin changes asap.
It might well be that in other places docker does make sense. E.g. in many environments one would prefer to isolate CI from changes in cygwin and update only say each quarter.
Our images are rebuilt each week, so we get Cygwin changes weekly. You could rebuild more often if you wanted to catch Cygwin changes more often, or even use Cygwin test repo (however I don't know if all packages go through Cygwin test repo), but I this last case I don't think you could achieve that simply by being based on our images.
@MSoegtropIMC wrote:
I just say that in the main Coq Platform CI we should have tests which are as close as possible to what users experience and this means direct installation of Cygwin in every run.
Totally agree. But isn't the Docker experience as close as possible to what users experience on a fresh install? As @MisterDA notes, our base images are refreshed from upstream Microsoft ones regularly, so it matches the experience of a fresh installation.
This, of course, assumes that the Docker environment is equivalent to a Windows native one that users would use. That's generally held true over the past few years, but there's no telling what can happen in the exciting world of Windows Insiders :-)
@MisterDA : in my experience it is a good idea to test Cygwin daily because then it is easier to find out what changed. It doesn't break regularly, but it does break. As I said, I don't really see the value in saving 10 minutes of a 2..3 hours build and making things more complicated - say finding out when docker was built and what cygwin package versions went in there or say making a patch with a different cygwin package version.
And as I said, for different purposes the decision is frequently for Docker.
Understood. If you already have a hand-crafted setup that works, there's certainly no need to disturb it.
I meanwhile updated Coq Platform to support opam 2.1.
Do you think it would make sense to do some sort of 1 day hackaton on the topic and see where we end up?