From the 8.15 changelog:
Added: coq_makefile now takes the -docroot option as alternative to the INSTALLCOQDOCROOT variable (#14558, by Stéphane Desarzens, with help from Jim Fehrle and Enrico Tassi).
I interpret this as meaning that in 8.15 both INSTALLCOQDOCROOT
and -docroot
would work, but it doesn't seem to be the case?
I'm not sure how to pass options to coq_makefile
outside of the _CoqProject
, so what I did was include
INSTALLDEFAULTROOT = ...
in the _CoqProject
, and similarly with INSTALLCOQDOCROOT
.
The former gets rid of the "no common logical root" warning in 8.14 but not 8.15; the latter doesn't get rid of the warning in either.
Adding -docroot ...
instead gets rid of the warning in 8.15, but of course it is not available at all in 8.14.
Is there any way of avoiding the warning in both Coq versions?
I don't know, but I'm not aware of any use case for a project eith no common logical root. Would you mind sharing yours?
"no common logical root" is how you emulate compositional builds using coq_makefile
.
If your stack involves 3 libraries with prefixes a
, b
and c
, and you are changing interfaces and testing the changes, the "recommended" workflow of "installing a, then b, then c" is just silly, since it provides no dependency tracking across libraries.
(but I'll stop here in case I'm sidetracking the conversation)
Hey, I'm from Ana's team. To reply to @Enrico Tassi We are about to release 2 libraries (well, 3, but 2 is enough to illustrate). Let's call them A
and B
. B
uses A
as a dependency. Eventually we want to publish them as opam packages and install independently, but our schedule for publishing the code is tight, so temporarily we have A
as a git submodule of B
. Our _CoqProject
for B
looks like this:
-R theories B
-R A_submodule/theories A
theories/B_file.v
theories/another_B_file.v
Hence there's no common logical root. Maybe this is not the way to go about this situation? It's the first time we write a composed _CoqProject
so maybe there's a better way which hopefully prevents the issue with the root.
if you want to build two projects without shared namespace from the same _CoqProject
, there is to my knowledge no way around the "no default root" warning. The warning is useful since it implies that nobody should do any kind of opam packaging that uses that _CoqProject
file, in any way.
My recommendation is that, if you want to keep the git submodule setup (which I would advise not to do, i.e., get rid of it ASAP), you should define your opam packages using Dune - that is, the opam packages issue dune
build commands.
This is the approach we use in the Hydras & Co. project, which hosts multiple packages of which some are independent. _CoqProject
is only for local development use, and all packaging is handled by opam + Dune.
Thank you! Your advice is very helpful. We'll definitely get rid of the submodule structure ASAP.
if you get rid of submodules, you can do the usual opam packaging with:
build: [make "-j%{jobs}"]
install: [make "install"]
which then implicitly uses _CoqProject
and usually coq_makefile
.
But I only recommend this for respositories hosting a single Coq package. Dune is better at handling multi-package repos.
Enrico Tassi said:
I don't know, but I'm not aware of any use case for a project eith no common logical root. Would you mind sharing yours?
we also have "no common logical root" for our Iris tutorials, e.g. https://gitlab.mpi-sws.org/iris/tutorial-popl21
and we now have the same problem as @Ana de Almeida Borges -- either we stop supporting Coq 8.14 (not good for a tutorial where we want to have low barrier to entry) or make
shows obscure warnings (not good for a tutorial either)
Proper Coq warnings can be disabled, is there any chance this can be disabled as well?
Last updated: Feb 06 2023 at 11:03 UTC