Christian Doczkal (Apr 08 2021 at 11:07): 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?
Théo Zimmermann (Apr 08 2021 at 11:59):Yes and no.
Théo Zimmermann (Apr 08 2021 at 11:59):There are several repositories with multiple packages (hydra-battles, topology).
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).
Christian Doczkal (Apr 08 2021 at 12:00):Thanks for the pointers, I'll take a look.
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.
Christian Doczkal (Apr 08 2021 at 12:01):And, yes, I know the mathcomp repository, but I was hoping for something easier.
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.
Christian Doczkal (Apr 08 2021 at 12:23):Okay, looking at the two repositories, the approach seems to be to have
_CoqProject file that covers the whole repository (to cater for IDEs like Emacs/ProofGeneral)dune files in each of the subdiretories, defining the package associated to their enclosing directory."dune" "build" "-p" name, and rely on dune to find package name inside the source tree, and build it. Christian Doczkal (Apr 08 2021 at 12:23):Am I missing something?
Théo Zimmermann (Apr 08 2021 at 12:34):Indeed, dune is important to properly handle the multi-package aspect.
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.
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.
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.
Théo Zimmermann (Apr 08 2021 at 12:56):As for Nix, yes it's a good use case.
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.
Théo Zimmermann (Apr 08 2021 at 12:56):The doc is far from complete yet, but I could help you set things up.
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.
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
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
Emilio Jesús Gallego Arias (Apr 08 2021 at 13:59):that's a big problem
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 whenbar.foois installed in user-contrib
Can you elaborate on this? How is this resolved and how should this be resolved?
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?
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.
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.
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.
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
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".
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.
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.
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.
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.
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.
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: Jun 03 2023 at 18:01 UTC