feature(coq): support for interproject composition of theories

[Alizter]

• error messages for missing transitive deps
• error messages for private OCaml libs used as plugins for public theories
• allow_private_deps check
• delay library resolution errors until build time
• restore boot support

[ejgallego]

See my tree in my personal repos, it was at some point close to be done.

[rgrinberg]

@Alizter better not to use find in tests. If you need particular files to exist, use shell tests for that.

[rgrinberg]

@ejgallego ready for review I believe.

[ejgallego]

A couple of things:

• this should bump coq lang to 0.4 (0.3 should disable inter scope composition, for compat)
• missing doc
• missing changes entry

[ejgallego]

After a first quick review, this good in general, will be a game changer! Gonna do some deeper testing tho.

[ejgallego]

It seems we are close to be here, I found a small bug which you can reproduce using the https://github.com/ejgallego/coq-universe/ repos (do make universe)

when the boot library is in scope -boot has to be passed to coqdep.

[ejgallego]

Yeah, it seems that when compiling math-comp, the boot library is not detected properly.

[ejgallego]

It is possible to add a test for this, I can write it, but the idea is that the test setups a theory that has prefix Coq and includes the module Init.Prelude.v , then a regular Coq composed theory.

[Alizter]

@ejgallego Looks like -boot is being passed correctly. However I noticed that the theories inside mathcomp don't declare Coq as a theories dependency. That is going to have to be done in order to compose with a local copy of coq.

[ejgallego]

@ejgallego Looks like -boot is being passed correctly. However I noticed that the theories inside mathcomp don't declare Coq as a theories dependency. That is going to have to be done in order to compose with a local copy of coq.

I don't see -boot being passed correctly. I'll post a build log where the problem is evident.

Regarding the second point, I see there is already code in this PR to handle that case.

[Alizter]

@ejgallego Ah, do you mean that -boot needs to be passed everywhere?

[ejgallego]

If the boot library is in scope, indeed you need to disable the automatic search path and let dune handle that, so yes, boot needs to be passed. Note that the code already is trying to do that when computing the flags.

[ejgallego]

Lib.t contains lazy values and possibly error values that are hard to compare and reason about.

Sorry I was not precise, I mean that why we can't just use Coq_lib_name.t ? Don't we have the properties that these are unique, and thus injective?

[ejgallego]

We should open an issue in Coq Universe w.r.t. doc building by the way, I think all we need is a @coqdoc alias :) and a few tweaks.

By the way, not a requirement, but I'd be cool to add a test coqdoc-compose even if broken.

[rgrinberg]

Sorry I was not precise, I mean that why we can't just use Coq_lib_name.t ? Don't we have the properties that these are unique, and thus injective?

For the closure it wouldn't matter (if we fix that validation issue), but I still think it's better to use the one equality function we defined as well behaved.

[ejgallego]

For the closure it wouldn't matter (if we fix that validation issue), but I still think it's better to use the one equality function we defined as well behaved.

Yes, we need to use a well-defined equality function. But that's the point I don't understand, why is

Coq_lib.equal t1 t2 = t1.name = t2.name && t1.path = t2.path

better behaved than

Coq_lib.equal t1 t2 = t1.name = t2.name

?

I'm Ok with identifying Coq theories as a pair of (name,path), however we need to make this clearer in the code then, as for most purposes, the code assumes that Coq theories are identified only by name. Does it make sense?

I'd be suprising for a user of Coq_lib that equals fail when the names are the same, wouldn't it?

[rgrinberg]

Well, consider this setup:

$ mkdir a b
$ touch {a,b}/dune-project
$ echo "(coq.theory (name a))" > {a,b}/dune

Today this already works and has useful applications. Here we have two theories with the same name but we surely don't want Coq_lib.equal to tell us they're equivalent.

[ejgallego]

Today this already works and has useful applications. Here we have two theories with the same name but we surely don't want Coq_lib.equal to tell us they're equivalent.

Indeed, the example makes sense with private libs. The thing is that if I am correct, we have no user for Coq_lib.equal so we can't really know if that's OK or not, except for the closure computation, but there, the name only is OK.

So that's what got me confused, I was thinking that the more fancy compare was due to an actual use case.

[rgrinberg]

Actually, we also use it to make sure we use the same boot lib everywhere.

OK or not, except for the closure computation, but there, the name only is OK.

It's only OK if we introduce the validation I mentioned earlier. Without it, the closure will report cycles instead of giving us a proper error that we're linking two different libraries with the same name.

[Alizter]

Unfortunately, coqdoc doesn't take the -boot option!

The sooner we rid ourselves of (no) -boot the better.

So to fix this, we can pass -coqlib with the location of Coq_lib.boot , if that one is present.

We can do this.

We should open an issue in Coq Universe w.r.t. doc building by the way, I think all we need is a @coqdoc alias :) and a few tweaks.

The @doc and @doc-latex aliases should already work.

[Alizter]

@rgrinberg @ejgallego I did some further refactoring in a separate commit, please review and I will squash with the rest.

We should merge this soon, or else I will keep adding patches. :-)

[rgrinberg]

@Alizter okay, but we need to add a test case for #5784 (comment) first.

It demonstrates a real issue Emilio pointed out. It doesn't necessarily needs to be addressed right now, since we are not yet sure whether it should be dune or coqc giving the error.

[Alizter]

@rgrinberg Added a test.

[ejgallego]

The @doc and @doc-latex aliases should already work.

Oh, that's great! Let's add this Coq's Universe CI and deploy the artifact 😈

[ejgallego]

Congrats on this great milestone!