Stream: Coq devs & plugin devs

Topic: OPAM packages and Dune


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

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

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

and actually should work in all cases for Dune 3.0

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Oct 21 2021 at 05:55):

You could maybe take it over to implement this idea?

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

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

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

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

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

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

There is nothing essential missing

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

Thanks for the reminder of the PR, indeed, I'll continue discussion there

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

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

view this post on Zulip 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: Dec 07 2023 at 14:02 UTC