Stream: Coq users

Topic: Did INSTALLDEFAULTROOT stop working in 8.15?


view this post on Zulip Ana de Almeida Borges (Apr 23 2022 at 12:07):

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?

view this post on Zulip Enrico Tassi (Apr 23 2022 at 12:18):

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?

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:31):

"no common logical root" is how you emulate compositional builds using coq_makefile.

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:33):

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.

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:33):

(but I'll stop here in case I'm sidetracking the conversation)

view this post on Zulip Mireia González Bedmar (Apr 23 2022 at 13:57):

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.

view this post on Zulip Karl Palmskog (Apr 24 2022 at 11:03):

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.

view this post on Zulip Mireia González Bedmar (Apr 24 2022 at 12:58):

Thank you! Your advice is very helpful. We'll definitely get rid of the submodule structure ASAP.

view this post on Zulip Karl Palmskog (Apr 24 2022 at 13:19):

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.

view this post on Zulip Ralf Jung (May 13 2022 at 08:00):

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

view this post on Zulip Ralf Jung (May 13 2022 at 08:00):

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). for now we went with the latter option.

view this post on Zulip Paolo Giarrusso (May 13 2022 at 08:14):

Proper Coq warnings can be disabled, is there any chance this can be disabled as well?

view this post on Zulip Meven Lennon-Bertrand (Mar 22 2023 at 17:29):

I am considering using the same setting of using a standalone Coq repo as a git submodule. Basically, we are currently developing in parallel a general-purpose library and a second, more specialized one that uses the first, and git submodules seem like a good solution to be able to do that. As far as I can tell from this discussion, this is a discouraged setting. Why is that? What would be an alternative solution? If you put such a solution in place in a public repo @Ana de Almeida Borges @Mireia González Bedmar , I would be very glad if you could link to it to see how you set things up :)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2023 at 18:09):

@Meven Lennon-Bertrand I use such kind of setups since a long time (in fact I developed Dune Coq support to ease my jsCoq build problems); they work reasonably well but there are some catches, happy to follow up in the Dune stream if you are interested

view this post on Zulip Ana de Almeida Borges (Mar 22 2023 at 18:12):

That was pretty much our situation as well. We gave up on using git submodules and went the mono-repo way. You can see our repo here: https://gitlab.com/formalv/formalv, but we took inspiration from mathcomp, so you can also check out https://github.com/math-comp/math-comp. I think we hadn't really internalized that you can define several different opam packages per git repo. With that, we didn't feel the need to separate the repos anymore.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 22 2023 at 18:13):

Note that I maybe misunderstood Meven, I often add Coq itself as a submodule, so I can update Coq, then work on Coq files with my custom Coq

view this post on Zulip Meven Lennon-Bertrand (Mar 23 2023 at 10:02):

Ana de Almeida Borges said:

That was pretty much our situation as well. We gave up on using git submodules and went the mono-repo way. You can see our repo here: https://gitlab.com/formalv/formalv, but we took inspiration from mathcomp, so you can also check out https://github.com/math-comp/math-comp. I think we hadn't really internalized that you can define several different opam packages per git repo. With that, we didn't feel the need to separate the repos anymore.

Thanks, I'll have a look! But unfortunately in my case people contributing to the two repos are somewhat disjoint, so I'm not sure I can convince them to merge the repos just to make maintenance more robust.

view this post on Zulip Meven Lennon-Bertrand (Mar 23 2023 at 10:03):

Emilio Jesús Gallego Arias said:

Note that I maybe misunderstood Meven, I often add Coq itself as a submodule, so I can update Coq, then work on Coq files with my custom Coq

My case is somewhat different, it is about having two different Coq developments, not OCaml code.

view this post on Zulip Paolo Giarrusso (Mar 23 2023 at 11:25):

Okay so by "Coq repo as a submodule" you don't mean "coq/coq as a submodule"

view this post on Zulip Paolo Giarrusso (Mar 23 2023 at 11:27):

And AFAICT this thread isn't really about issues with git submodules, just about composing their builds with coq_makefile and using that in an opam package

view this post on Zulip Paolo Giarrusso (Mar 23 2023 at 11:29):

Using dune for packaging (and CoqProject just for building) works better; Karl's message about Hydras & Co explains how to set that up.

view this post on Zulip Meven Lennon-Bertrand (Mar 23 2023 at 12:21):

Ha, I see! For now, opam packaging is still quite far away, so if the issue is with how this interacts with submodules, it is not a problem yet.

view this post on Zulip Meven Lennon-Bertrand (Mar 23 2023 at 12:21):

Paolo Giarrusso said:

Okay so by "Coq repo as a submodule" you don't mean "coq/coq as a submodule"

No, indeed, my original question was unclear. I meant "a Coq formalization as a submodule of another Coq formalization"


Last updated: Jun 15 2024 at 23:01 UTC