Michael Soegtrop (Mar 14 2023 at 08:30): Michael Soegtrop (Mar 14 2023 at 08:30):Since there are issues with OCaml 4.13 on ARM platforms which appear to be fixed in 4.14.1 (there was e.g. a stack overflow in Search with 4.13), we concluded to use 4.14.1. Now one issue is that on Windows the latest available version is 4.14.0 (see https://github.com/fdopen/opam-repository-mingw/tree/opam2/packages/ocaml-variants). So I tend to using 4.14.0 on Windows and 4.14.1 on other platforms. Since the MinGW repo has been officially discontinued (https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users) I am happy that there is 4.14.0.
Are there any objections against 4.14.0 on Windows or in general using a different version on Windows and other platforms?
@Emilio Jesús Gallego Arias
Michael Soegtrop (Mar 14 2023 at 08:34):One alternative would be to get rid of the MinGW repo and make Opam work on WIndows with the main repo, but this might be a bit of effort and I would need some support for this.
Emilio Jesús Gallego Arias (Mar 14 2023 at 15:45):4.14.0 should be fine for win AFAICT
Karl Palmskog (Mar 28 2023 at 07:39):Is there any obvious reason for why 4.14.1 is not available on Windows? I thought they were going to support the 4.14 series for quite some time?
Michael Soegtrop (Mar 28 2023 at 08:14):The reason is that the MinGW opam repo - from which we take Opam and OCaml since there is no other version I am aware of which works on Windows - is officially discontinued since August 2021.
Michael Soegtrop (Mar 28 2023 at 08:15):I tried a few times to pull together a workshop to get an alternative, but it didn't happen so far.
Karl Palmskog (Mar 28 2023 at 08:42):but theoretically, 4.14.1 could be built from sources using MinGW, right?
Michael Soegtrop (Mar 28 2023 at 08:49):I don't know. Last time I tried this is years back and it did not work then. I discussed the topic once with Xavier and he said that the MinGW repo contains patches which are not in a state that they could be merged to the OCaml mainline, but that something along this line is required.
Michael Soegtrop (Mar 28 2023 at 08:50):Maybe things have improved since then and all what needs to be done is merging the opam repos. I don't believe there is anything serious which couldn't be fixed in a day or two, but a few people need to sit together to get it done - say one OCaml maintainer, one Opam maintainer and me.
Karl Palmskog (Mar 28 2023 at 09:03):OK thanks, then I understand better. Unfortunate situation. At least Windows users have WSL2 if they absolutely need 4.14.1.
Michael Soegtrop (Mar 28 2023 at 09:07):I still think we should just organise a work shop and try how far we get, but it is hard to get the people together. I don't know enough about OCaml to do it alone, but maybe there is someone in the Coq team who could spend a day or two on this.
Karl Palmskog (Mar 28 2023 at 09:27):topic for CUDW?
Michael Soegtrop (Mar 28 2023 at 10:42):I didn't plan to join CUDW in person this year and also don't have a portable Windows machine, but for sure we could work remotely on this during CUDW.
Théo Zimmermann (Mar 28 2023 at 11:09):Personally, I have little motivation to get people from the Coq side to work on this while Tarides is promising that opam 2.2 will come soon with Windows support and while allow to progressively get rid of the MinGW repo.
Michael Soegtrop (Mar 28 2023 at 11:09):@Karl Palmskog @Emilio Jesús Gallego Arias : would you be available for trying to setup an OCaml / Opam for Windows without the MinGW repo during CUDW (@Emilio Jesús Gallego Arias for the OCaml side and @Karl Palmskog for the Opam side)? Do you both have Windows Laptops or could you borrow one? I would work from home on this then (I have a Windows machine which can do the relevant part of a Coq Platform build in a few minutes).
Michael Soegtrop (Mar 28 2023 at 11:10):@Théo Zimmermann : I am not sure we will get there without making our own analysis of what is missing.
Karl Palmskog (Mar 28 2023 at 11:11):I will try to be at CUDW and set aside time for these kinds of issues, but unfortunately I don't hold the money purse or have final say.
Emilio Jesús Gallego Arias (Mar 28 2023 at 15:22):Hi @Michael Soegtrop I would be available but I'm unsure about what you are trying to do, how it is related to Diskuv?
Théo Zimmermann (Mar 28 2023 at 16:08):It is not. FWIW, I had a look at Diskuv because I thought it might be interesting for the Platform, but from reading some of the warnings in their doc, I concluded it was not a good use case.
Michael Soegtrop (Mar 28 2023 at 16:23):@Emilio Jesús Gallego Arias : Coq Platform is using for Windows the Opam MinGW repo by fdopen which is discontinued since August 2021. He continued to maintain it, but there is e.g. no OCaml 4.14.1. So we need an alternative - however it looks.
Emilio Jesús Gallego Arias (Mar 28 2023 at 17:06):The official alternative upstream is Diskuv , but if I understand correctly that's not ok for the platform?
Théo Zimmermann (Mar 29 2023 at 08:28):This is not an alternative AFAIU. It is just a wrapper. It also doesn't provide 4.14.1 last I checked.
Emilio Jesús Gallego Arias (Mar 29 2023 at 10:16):Is it a wrapper over what @Théo Zimmermann ?
Théo Zimmermann (Mar 29 2023 at 10:17):AFAIR, it uses opam-mingw internally. But maybe I remember incorrectly.
Emilio Jesús Gallego Arias (Mar 29 2023 at 12:02):Not sure what it does for opam these days, but last time I looked at least the compiler didn't require cygwin
Emilio Jesús Gallego Arias (Mar 29 2023 at 12:05):@Michael Soegtrop I don't think it is likely that I can devote any time to windows work, that's a topic that interests me, but out of reach for some other reasons right now.
Michael Soegtrop (Mar 29 2023 at 16:18):@Emilio Jesús Gallego Arias : the OCaml compiler I produce also doesn't require cygwin - I only require cygwin to build the OCaml compiler, but not to use it.
Emilio Jesús Gallego Arias (Mar 29 2023 at 16:28):I meant mingw , it seems a fully msvc native setup; but I guess the main question for the platform is why does it need its own OCaml distro as oppossed to following OCaml foundation plans for win support?
Paolo Giarrusso (Mar 29 2023 at 16:40):Wanting quick installations? Use anything but Diskuv OCaml! Diskuv OCaml will conduct from-source builds unless it can guarantee (and code sign) the binaries are reproducible. Today that means a lot of compiling.
From https://github.com/diskuv/dkml-installer-ocaml. Would this be a sufficient objection today?
Michael Soegtrop (Mar 31 2023 at 07:39):@Emilio Jesús Gallego Arias : last time I did look into this (about 1 year back) there was an OCaml distribution available for Windows, but no working Opam and it was not possible to use the official OCaml distribution for Windows with Opam. I also discussed this with OCaml and Opam maintainers back then and they confirmed this situation. As far as I can tell the plan is to fix this in Opam 2.2. But I must say that when Opam 2.0 was current, it was said to be fixed in Opam 2.1.
Part of the problem ist that some opam packages we use still need a shell (e.g. use configure scripts) and I am not quite sure how Opam 2.2 shall fix this - we must also work on fixing the packages to use a shell less configure system or provide a sufficiently compliant shell on Windows without cygwin.
Karl Palmskog (Mar 31 2023 at 07:44):part of the reason why people use configure scripts are the limited options for configuration available in opam packages, e.g., I believe one can't define ad-hoc configuration variables that can be set by the user (so people resort to virtual packages like coq-native)
Michael Soegtrop (Mar 31 2023 at 07:48):Yes. My view on the situation is that we should just sit down and construct a prototype Coq Platform so that we see what is needed. Otherwise I have little hope that it will work in the near future. I can do most of the work, but I might need some help with OCaml and Opam changes, and of course discussions about what is the best solution for specific problems.
Théo Zimmermann (Mar 31 2023 at 08:13):Part of the problem ist that some opam packages we use still need a shell (e.g. use configure scripts) and I am not quite sure how Opam 2.2 shall fix this - we must also work on fixing the packages to use a shell less configure system or provide a sufficiently compliant shell on Windows without cygwin.
Opam 2.2 won't solve this.
Karl Palmskog (Mar 31 2023 at 08:16):if we want to solve shell issue more practically in the context of the Platform, would could do something like provide purely Dune-based idioms for what the configure scripts are doing
Karl Palmskog (Mar 31 2023 at 08:17):and assist project maintainers to either completely migrate to Dune, or provide a Dune build specifically for the opam package
Michael Soegtrop (Mar 31 2023 at 10:23):And again, IMHO we really need to sit down and figure out what the issues are.
Michael Soegtrop (Mar 31 2023 at 10:24):It is not obvious what configure scripts do unless one looks at them.
Emilio Jesús Gallego Arias (Mar 31 2023 at 13:15):Wouldn't it make more sense to learn what the OPAM 2.2. plans are first?
Michael Soegtrop (Mar 31 2023 at 13:56):At least last year I didn't have the impression that this is very clear (when it comes to Windows).
Paolo Giarrusso (Mar 31 2023 at 23:35):Given that Cygwin and WSL exist, is this a good use of volunteers' time?
Paolo Giarrusso (Mar 31 2023 at 23:41):(this = porting their build scripts to dune)
Karl Palmskog (Apr 01 2023 at 06:21):we already have the long-standing task to add Dune builds where we can to Coq projects: https://github.com/coq-community/manifesto/issues/87
In the short term, it may not have a high priority to migrate to Dune, but if we can solve both operating system issues and get other benefits such as composable builds, Duniverse, safer parallelism, ... it seems worthwhile to me.
Théo Zimmermann (Apr 02 2023 at 17:08):Dunifying Coq packages sounds like a good use of volunteer time. Any other Windows related fixes does not seem a top priority to me.
Karl Palmskog (Apr 02 2023 at 17:29):we could try to manually add build system info to the Platform package info table. That could be a first step. For example, we could label with "coq_makefile"/"coq_makefile + shell script"/"Dune"/"homegrown Makefile"/...
Ali Caglayan (Apr 03 2023 at 20:39):Regarding coq-native which was mentioned above, Dune 3.6 can auto detect Coq being compiled with -native-conpiler yes (i.e. coq-native) and set the compilation mode accordingly when building a Dune stanza. The user can always override this by giving an explicit mode. This was one of the blockers for the mathcomp people.
Ali Caglayan (Apr 03 2023 at 20:39):Another thing that will make migrating to Dune much easier is with the upcomming 3.8 version which will have composition with installed theories.
Ali Caglayan (Apr 03 2023 at 20:39):The installed theories don't necesserily have to have been installed with Dune either so there will be no restriction to migrating.
Ali Caglayan (Apr 03 2023 at 20:40):But my opinion on package maintence in general is "use Dune if you think it will make your life easier", there is no reason to switch if you don't want to.
Last updated: Jun 03 2023 at 03:01 UTC