Stream: coq-community devs & users

Topic: multi-package repositories


view this post on Zulip Christian Doczkal (Apr 08 2021 at 11:07):

Are there some multi-package repositories in coq-community and/or is there some support for this from the coq-community templates?

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 11:59):

Yes and no.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 11:59):

There are several repositories with multiple packages (hydra-battles, topology).

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:00):

And still no support from the templates despite this being an important use case (also preventing their use in math-comp's main repo which is also multi-packages).

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:00):

Thanks for the pointers, I'll take a look.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:01):

I was planning to add an issue to start a discussion about that, but feel free to do that yourself.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:01):

And, yes, I know the mathcomp repository, but I was hoping for something easier.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:03):

Théo Zimmermann said:

I was planning to add an issue to start a discussion about that, but feel free to do that yourself.

I'm not 100% sure I will end up creating a multi-package repository, so go ahead and start the discussion. If you CC me, I'll probably join the discussion.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:23):

Okay, looking at the two repositories, the approach seems to be to have

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:23):

Am I missing something?

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:34):

Indeed, dune is important to properly handle the multi-package aspect.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:35):

Another thing that you may have missed is the CI scripts (GitHub Actions) which had to be customized.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 12:54):

Indeed, thanks. For Docker-based CI, this seems to be fairly straightforward though. I guess I'll also want to switch to nix. The whole point of the this split is that part of my development depends on another development with long compile time, so I would like to profit from this being cached. Although I remember that there were also caching tricks for docker-based CI.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:55):

The caching tricks for Docker CI amount to building your own Docker images, but this is very well documented and easy to do with Erik's tools.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:56):

As for Nix, yes it's a good use case.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:56):

The coq-nix-toolbox available in coq-community is supposed to work for multi-package repositories.

view this post on Zulip Théo Zimmermann (Apr 08 2021 at 12:56):

The doc is far from complete yet, but I could help you set things up.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 13:53):

Théo Zimmermann said:

The doc is far from complete yet, but I could help you set things up.

Thank you for the offer, I may ping you once I get to that point. Probably not this week though, maybe much later. Shaving time off CI runs is not the most urgent thing to do.

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 13:57):

dune will help a lot for multi-package setups but I still need to tweak some support, you have an example here https://github.com/math-comp/math-comp/pull/316

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 13:59):

main thing missing is that indeed Dune doesn't resolve (theories bar.foo) properly when bar.foo is installed in user-contrib

view this post on Zulip Emilio Jesús Gallego Arias (Apr 08 2021 at 13:59):

that's a big problem

view this post on Zulip Christian Doczkal (Apr 09 2021 at 08:09):

Emilio Jesús Gallego Arias said:

main thing missing is that indeed Dune doesn't resolve (theories bar.foo) properly when bar.foo is installed in user-contrib

Can you elaborate on this? How is this resolved and how should this be resolved?

view this post on Zulip MackieLoeffel (Apr 09 2021 at 08:19):

I am also interested in this as I am currently running into this problem when trying to use dune for a multipackage repository. Is there an issue for this somewhere?

view this post on Zulip Christian Doczkal (Apr 09 2021 at 08:35):

I don't even know what "this" problem is. I'm still trying to see that would be required to split the package for my development into two packages. From the looks of it, coq-community/topology has a working setup.

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 12:55):

I've seen this point in issues, but the summary is that "composable builds" work well as long as all packages live together with a single dune-project; if you install a dependency you must modify a few lines in the dune files.

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 12:59):

@Christian Doczkal AFAICT, dune build in that repo will fail; you'll have to install the zorn-lemma part before building the topology part.

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 12:59):

and I suspect after any change to zorn-lemma you'd need a clean rebuild of topology to be sound

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:00):

but that's not the fault of that repo, because dune forces you to choose statically between "separate builds" and "compositional builds".

view this post on Zulip Paolo Giarrusso (Apr 09 2021 at 13:03):

in a compositional dune build you'd have proper cross-project dependency tracking, as if the two projects were unified, without the build configs knowing much about each other _except_ that https://github.com/coq-community/topology/blob/master/theories/Topology/dune would need (theory ZornsLemma) to declare its dependency on the other half.

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 13:06):

Basically, the solution that @Karl Palmskog came up with is to rely on Dune for the opam packages, but still rely on coq_makefile for the actual daily dev.

view this post on Zulip Christian Doczkal (Apr 09 2021 at 13:43):

Well, I'm totally okay with separate builds and/or continuing to use coq_makefile for for development. My main concern is to separate my library into a part that relies only on (parts of) mathcomp and the part that relies on coq-fourcolor, which takes 10min to build, even on my fairly up-to-date Laptop with an i7. People shouldn't have to install this, if they don't need anything that relies on it.

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 13:45):

One issue with continuing to use coq_makefile for day to day development is that you don't have a good way to build only one package out of the repository.

view this post on Zulip Théo Zimmermann (Apr 09 2021 at 13:45):

But if you are actually concerned about the users when they install the package, then Dune does solve the issue.

view this post on Zulip Christian Doczkal (Apr 09 2021 at 13:51):

Well, I could turn the original package into meta-package that installs everything. Not sure why one would want to have a monolithic package.


Last updated: Feb 05 2023 at 14:02 UTC