Emilio Jesús Gallego Arias (Oct 20 2021 at 19:58): Emilio Jesús Gallego Arias (Oct 20 2021 at 19:58):Hi folks, actually @Rudi Grinberg gave me an idea on how to actually split our packages using dune even for 8.14
Emilio Jesús Gallego Arias (Oct 20 2021 at 19:58):The idea is easy, have ./configure modify theories/dune to add (mode native) ; this doesn't work super well when we use the implicit configure rule, but for packages, where we always call configure, it is actually fine
Emilio Jesús Gallego Arias (Oct 20 2021 at 19:58):and actually should work in all cases for Dune 3.0
Emilio Jesús Gallego Arias (Oct 20 2021 at 19:59):that idea arose in the discussion with @Erik Martin-Dorel and @Pierre Roux to fix the multinomials package
Théo Zimmermann (Oct 21 2021 at 05:53):That's a good idea, but maybe a bit late now that we have released 8.14.0 to opam?
Théo Zimmermann (Oct 21 2021 at 05:53):OTOH, this could be a good strategy for 8.15 (since I don't expect the situation with respect to the legacy Makefile will be much improved then).
Théo Zimmermann (Oct 21 2021 at 05:54):And we could start testing this as of today by splitting the coq.dev package in core-dev.
Théo Zimmermann (Oct 21 2021 at 05:55):Note that there is already the open and unfinished PR: https://github.com/coq/opam-coq-archive/pull/1801
Théo Zimmermann (Oct 21 2021 at 05:55):You could maybe take it over to implement this idea?
Pierre Roux (Oct 21 2021 at 07:43):For the packages of Coq itself, that sounds a good idea.
Although, once dune 3.0 will be there and working properly with the native configuration declared by coqc, I'm not sure I understand how the stdlib package should be any different from any other package, but maybe I'm missing something as I'm definitely not a dune expert.
Théo Zimmermann (Oct 21 2021 at 07:44):with the native configuration declared by coqc
What do you mean by this? I thought that the end goal would be to have split packages for native.
Pierre Roux (Oct 21 2021 at 07:48):Sure, that's just the end goal, not the current state of affair with the coq-native OPAM package.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:21):Yeah split packages have some interesting issues, for now I'm thinking about the support for the coq-native package
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:21):@Théo Zimmermann , this is purely a packaging issue, indeed we should try in coq-opam-archive first, but would we be happy with the result, we could package 8.14 that way
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:22):There is nothing essential missing
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:22):Thanks for the reminder of the PR, indeed, I'll continue discussion there
Théo Zimmermann (Oct 21 2021 at 13:22):Not my call. If this is compatible with the policy of opam-repository maintainers, that's fine with me.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:26):Théo Zimmermann said:
Not my call. If this is compatible with the policy of opam-repository maintainers, that's fine with me.
As far as I can tell it is up to us, I think indeed they would appreciate the split actually.
Emilio Jesús Gallego Arias (Oct 21 2021 at 13:26):For some cases [for example dune CI testing] people want a coq-light package that only includes the prelude [not sure how to do that yet, but I mean, that's a step]
Last updated: May 28 2023 at 13:30 UTC