Michael Soegtrop (Oct 19 2021 at 12:54): Michael Soegtrop (Oct 19 2021 at 12:54):I currently have PR (https://github.com/coq/platform/pull/155) running to update to Coq 8.14.0.
The things I see left to do are:
Do you see any important issues left?
Michael Soegtrop (Oct 19 2021 at 13:34):@Karl Palmskog : I have packages for Mtac2 and Unicoq which work for 8.14 in Coq Platform, but I won't push them (unless you want me) because for Unicoq it is not a tagged version. The Mtac2 package is fine, but it won't pass CI without UniCoq.
Michael Soegtrop (Oct 19 2021 at 13:42):@Karl Palmskog : can you please have a look at the Windows errors at (https://github.com/coq/platform/pull/155/checks?check_run_id=3939263734). I don't get this. Does opam tell me that Coq 8.14.0 is not supported on Windows? If yes, why? If no, what does opam tell me here?
Enrico Tassi (Oct 19 2021 at 13:44):IMO the opam repo (for windows) is not up to date
Enrico Tassi (Oct 19 2021 at 13:44):it happened last time as well
Enrico Tassi (Oct 19 2021 at 13:44):it syncs a few days later, no?
Michael Soegtrop (Oct 19 2021 at 13:44):Well officially it won't sync ever again.
Enrico Tassi (Oct 19 2021 at 13:44):I mean, the main repo, not the coq specific ones
Enrico Tassi (Oct 19 2021 at 13:45):oh...
Michael Soegtrop (Oct 19 2021 at 13:45):Yes, I mean the MinGW opam repo - it is no longer supported sine August.
Enrico Tassi (Oct 19 2021 at 13:45):ouch, so what do we use now?
Michael Soegtrop (Oct 19 2021 at 13:45):But no big deal - I can put it into the Coq Platform local patch repo.
Enrico Tassi (Oct 19 2021 at 13:46):ok, but I mean, in the long term for windows... what is the plan then?
Michael Soegtrop (Oct 19 2021 at 13:46):Theoretically opam 2.1 should support cross compiling MinGW on cygwin and the repos could be merged. It is just so that nobody did this as yet.
Michael Soegtrop (Oct 19 2021 at 13:48):I am discussing this with @Théo Zimmermann since a while. I guess I need to take care of it if I want it to happen. I wanted to invite the opam players for a hackaton or so using the Coq Platform as a prototype project. But after 2021.09.
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:49):opam 2.2. is supposed to have native windows support, but until then the situation is a bit murky, tho the fdopen repos still sees the occassional update
Michael Soegtrop (Oct 19 2021 at 13:50):Not sure what "native support" means. You mean compile without cygwin? This is not likely to work (some coq packages use autotools ...)
Michael Soegtrop (Oct 19 2021 at 13:51):Cross support should be in 2.1 already.
Enrico Tassi (Oct 19 2021 at 13:51):Michael Soegtrop said:
I am discussing this with Théo Zimmermann since a while. I guess I need to take care of it if I want it to happen. I wanted to invite the opam players for a hackaton or so using the Coq Platform as a prototype project. But after 2021.09.
If you want to come to the warm south of France, I can ask for rooms here at Inria
Michael Soegtrop (Oct 19 2021 at 13:52):If you want to come to the warm south of France, I can ask for rooms here at Inria
I would rather do it remotely - it should either be relatively quick (1..2 days) or not work.
Michael Soegtrop (Oct 19 2021 at 13:53):Anyway, for the time being I will put the package into the Coq Platform local repo.
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:54):@Michael Soegtrop indeed if you read the reasons the mingw repos is being dropped is due to many packages using dune
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:54):which supports windows well
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:54):I think indeed having a separate repos was not a good idea, much better if the fixes go into the main one
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:55):but was overwhelming at the time
Michael Soegtrop (Oct 19 2021 at 13:55):@Emilio Jesús Gallego Arias : indeed I think opam was always flexible enough to handle this in one repo - having a patched up opam executable would have been sufficient.
Michael Soegtrop (Oct 19 2021 at 13:57):But the main issue I see with a full native opam is that we still have packages which do use stuff like autotools which is impossible on Windows without cygwin. So I would stick with cygwin cross MinGW until some future.
Emilio Jesús Gallego Arias (Oct 19 2021 at 13:59):there are not so many packages that use autotools, bash use is probably a bigger offender
Emilio Jesús Gallego Arias (Oct 19 2021 at 14:00):but indeed, packages will have to be fixed
Enrico Tassi (Oct 19 2021 at 14:00):Indeed, and it is not just a matter of autotools/make vs dune, you need perl, C++, gtk headers... in other words for depext to work you need some sort of non-ocaml package manager
Emilio Jesús Gallego Arias (Oct 19 2021 at 14:00):to use a protable setup
Michael Soegtrop (Oct 19 2021 at 14:01):IMHO a fully native environment is more of a long term goal - say 2 years. We should approach it in steps.
Théo Zimmermann (Oct 19 2021 at 14:11):Good Windows support in opam 2.2 was announced more than a year ago (during the previous OCaml workshop), but I think that due to the delay in stabilizing opam 2.1, what was planned for opam 2.2 landed in 2.1 in the end.
Last updated: Jun 03 2023 at 03:01 UTC