Stream: Coq Platform devs & users

Topic: Platform OCaml versions


view this post on Zulip Karl Palmskog (Aug 23 2020 at 23:23):

so it looks like the Unicoq tags for the platform are only compatible with OCaml < 4.08. This means the platform is basically tied to 4.05 or 4.07 versions of OCaml. Does this really make sense? I thought we were aiming for supporting all OCaml versions supported by Coq (8.12.0), which goes from 4.05 up to 4.11.

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 08:03):

Good point @Karl Palmskog! I think this would be worth adding to the list of "unresolved questions" here. Would you do it or shall I?

view this post on Zulip Karl Palmskog (Aug 24 2020 at 08:07):

@Théo Zimmermann feel free to do it

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 08:07):

OK

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 08:24):

In the case of Unicoq though, from what I recall, it is an issue with a bug in Coq that makes it impossible to dynamically link a chain of dependent plugins with OCaml >= 4.08. So it's not really the maintainers' fault. @Emilio Jesús Gallego Arias should be able to tell more.

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 08:29):

@Karl Palmskog There is another package that should be included in the platform and which isn't compatible with the whole range of OCaml versions: it is SerAPI (only compatible with OCaml 4.07 and later).

view this post on Zulip Karl Palmskog (Aug 24 2020 at 08:30):

well, erring towards later versions is better in my book

view this post on Zulip Théo Zimmermann (Aug 24 2020 at 08:31):

Sure. I just meant to highlight that this is not a trivial question. Anyway, I've opened https://github.com/MSoegtropIMC/coq-platform/pull/23 now.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 24 2020 at 09:03):

Yup, there is a bug open regarding the problem Coq's linker has. Actually that's a bit tricky to solve as the Coq linker needs to know dependencies of packages, dune provides integration with findlib to do that.

view this post on Zulip Michael Soegtrop (Aug 26 2020 at 16:06):

So what is the conclusion? In my opinion "the" Coq platform uses a specific version of OCaml, which I plan to be 4.07.1. Of cause the scripts are easy to change to have something else, if packages depending on it are disabled.

So for 8.12.0 I don't see this as a problem, but I think we should work on fixing it for 8.13. Is this realistic?

view this post on Zulip Karl Palmskog (Aug 26 2020 at 16:09):

fine by me to fix 4.07.1 for now, as said in issue. But what should be our goal for 8.13? If 8.13.0 supports 4.05.0 still, should we aim for every package in the platform to support the whole range from OCaml 4.05 to 4.11?

view this post on Zulip Karl Palmskog (Aug 26 2020 at 16:10):

clearly this will take a lot of coordination with both maintainers and Coq devs and release managers, so one might aim for something more modest, like support for 4.07 - 4.10

view this post on Zulip Michael Soegtrop (Aug 26 2020 at 16:21):

I agree that the platform should be reasonably flexible but not push it to the limits, so I tend to agree that 4.07 ... 4.10 seems reasonable.


Last updated: Jan 30 2023 at 12:03 UTC