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.
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?
@Théo Zimmermann feel free to do it
OK
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.
@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).
well, erring towards later versions is better in my book
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.
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.
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?
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?
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
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: Oct 13 2024 at 01:02 UTC