Stream: Coq Platform devs & users

Topic: 2021.09: anything left to do?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:44):

IMO the opam repo (for windows) is not up to date

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:44):

it happened last time as well

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:44):

it syncs a few days later, no?

view this post on Zulip Michael Soegtrop (Oct 19 2021 at 13:44):

Well officially it won't sync ever again.

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:44):

I mean, the main repo, not the coq specific ones

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:45):

oh...

view this post on Zulip Michael Soegtrop (Oct 19 2021 at 13:45):

Yes, I mean the MinGW opam repo - it is no longer supported sine August.

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:45):

ouch, so what do we use now?

view this post on Zulip Michael Soegtrop (Oct 19 2021 at 13:45):

But no big deal - I can put it into the Coq Platform local patch repo.

view this post on Zulip Enrico Tassi (Oct 19 2021 at 13:46):

ok, but I mean, in the long term for windows... what is the plan then?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ...)

view this post on Zulip Michael Soegtrop (Oct 19 2021 at 13:51):

Cross support should be in 2.1 already.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Oct 19 2021 at 13:53):

Anyway, for the time being I will put the package into the Coq Platform local repo.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2021 at 13:54):

which supports windows well

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2021 at 13:55):

but was overwhelming at the time

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2021 at 14:00):

but indeed, packages will have to be fixed

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2021 at 14:00):

to use a protable setup

view this post on Zulip 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.

view this post on Zulip 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: Jan 30 2023 at 11:03 UTC