Hi folks, actually @Rudi Grinberg gave me an idea on how to actually split our packages using dune even for 8.14
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
and actually should work in all cases for Dune 3.0
that idea arose in the discussion with @Erik Martin-Dorel and @Pierre Roux to fix the multinomials package
That's a good idea, but maybe a bit late now that we have released 8.14.0 to opam?
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).
And we could start testing this as of today by splitting the coq.dev
package in core-dev
.
Note that there is already the open and unfinished PR: https://github.com/coq/opam-coq-archive/pull/1801
You could maybe take it over to implement this idea?
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.
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.
Sure, that's just the end goal, not the current state of affair with the coq-native OPAM package.
Yeah split packages have some interesting issues, for now I'm thinking about the support for the coq-native package
@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
There is nothing essential missing
Thanks for the reminder of the PR, indeed, I'll continue discussion there
Not my call. If this is compatible with the policy of opam-repository maintainers, that's fine with me.
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.
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