Christian Doczkal (Apr 16 2021 at 11:19): Christian Doczkal (Apr 16 2021 at 11:19):I have a library where a small part depends on a fairly heavy dependency and most users of this library will not need this part. Is there a clean/established way to use the OPAM depopts: field to build that part only if the aforementioned dependency is already installed? I would like to avoid converting my repository into a multi-package repository until the support for this (e.g., by dune or coq-community/templates) has improved.
Enrico Tassi (Apr 16 2021 at 11:25):I'm not so sure I understand your question. Coq itself uses a depopt https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.13.1/opam
Christian Doczkal (Apr 16 2021 at 11:43):@Enrico Tassi Well, some people consider "automagic" dependencies to be very dirty. This is why package managers like macports (variants) or Gentoo's portage (USE-flags) have more predictable mechanisms for this.
Christian Doczkal (Apr 16 2021 at 11:53):Besides, if one want's to build with dune, what's the preferred way to disable building some files? I guess for make-based projects one can simply append a few lines to the _CoqProject file.
Enrico Tassi (Apr 16 2021 at 11:55):if one want's to build with dune
I've no clue. AFAIK dune devs don't like disjunction. I think they have a select statement to pick one module over another if a library is there, but I don't know it if can be used for Coq
Enrico Tassi (Apr 16 2021 at 11:55):CC @Emilio Jesús Gallego Arias
Enrico Tassi (Apr 16 2021 at 11:56):I guess for make-based projects one can simply append a few lines to the _CoqProject file.
You can also pass extra arguments to coq_makefile, as in coq_makefile -f _CoqProj -o Makefile foo.v {coq-fourcolor:installed}
Enrico Tassi (Apr 16 2021 at 11:57):I mean, all arguments to coq_makefile are "appended" to the _CoqProject. If you call it from opam you can use it's way of filtering options to pass/drop these arguments
Enrico Tassi (Apr 16 2021 at 11:58):said all that, I'd still go for a multi-package repo ;-)
Christian Doczkal (Apr 16 2021 at 11:59):Fair enough, but I think I will want to quickly get the right _CoqProject file, as I will still want to have IDE support for editing these files. So maybe it's time to write a minimalist configure.
Christian Doczkal (Apr 16 2021 at 12:00):I am planning to go multi-package eventually, but I don't feel like doing so right now.
Emilio Jesús Gallego Arias (Apr 16 2021 at 14:31):Dune does indeed support (optional) for OCaml libraries and (enabled_if $cond) for (coq.theory ...) statements; tho the latter is not very useful as it doesn't really allow to depend on generated conditions yet (Dune 2.x is frozen, Dune 3.x does rework the build system so this is possible)
Emilio Jesús Gallego Arias (Apr 16 2021 at 14:32):I was not aware that Dune devs didn't like disjunction tho; AFAICT there is no particular problem with it other than the current limitation of how dynamic the build graph can be, which are indeed planned to be much improved in 3.0
Emilio Jesús Gallego Arias (Apr 16 2021 at 14:33):Having (optional) work for Coq theories could be done for Dune 2.9 I think, then you can have that parts built only iff all the dependencies are satisfied.
Last updated: Apr 19 2024 at 10:02 UTC