coq: test and fix duplicate theory prefix in COQPATH bug

[Alizter]

This bug happens when using COQPATH so it won't affect most users. When having two theories A.B and A.C installed, dune will erroneously fail saying that the theory A has been defined twice.

I think the correct fix would be to merge the maps in the case where A has no immediate .vo files and is just a prefix.

[ejgallego]

Good catch @Alizter ! I think indeed it should be enough to merge empty paths when building the DB.

However that's a bit tricky as then the example would need to add two flags, what would happen if a user has:

foo/A/T1
foo/A/T2
...
foo/A/Tn

and

bar/A/U1
bar/A/U2
....
bar/A/Un

will Coq work with -Q bar A -Q foo A ?

[Alizter]

This was caught by nixpkgs by the way. That is the only packaging which uses COQPATH IINM.

[ejgallego]

In fact I'm not sure if Coq's semantics do require to merge even non empty paths.

[Alizter]

The package in question are mathcomp packages. They all get installed under mathcomp.* but in different paths for Nix. There is no problem in user-contrib however.

[ejgallego]

I figured mathcomp would be the culprit, what I wonder is about the case:

foo/A/a.vo
foo/A/B

bar/A/b.vo
bar/A/C

What does Coq expect us to do here?

[Alizter]

That case would not be consistent since the theory would have to both be A and we would be conflicting. The only time we can have A together is if it is a prefix and in that case it will be empty.

So we shouldn't really care what Coq does in that case as we would be breaking the isolated install making it unsound anyway.

[ejgallego]

Mmm, I'm afraid that coqc does accept that case, so I think we should, otherwise we may risk some compat problem. With this layout:

./foo/A/B/b.vo
./foo/A/a.vo
./bar/A/C/d.vo
./bar/A/c.vo

Coq has not problem with:

$ COQPATH=foo:bar coqtop
> From A Require Import a b c d.

However if we do add a duplicate a.v, very funny stuff starts to happen:

./foo/A/B/b.vo
./foo/A/a.vo
./bar/A/C/d.vo
./bar/A/a.vo
./bar/A/c.vo

Then From A Require Import a will pick the one that is first in COQPATH. Maybe that's intended?

Who knows, Coq semantics are messy.

That's a nice testcase actually.

[Alizter]

Yeah I didn't doubt that Coq would accept it, but from the perspective of keeping user-contrib sane, having overlapping theories breaks the contract we make with the user about having a valid user-contrib.

In the future we can enforce all installs to be done as a COQPATH like for OCaml, since then we would have an atomic garuntee. That will also mean theories will need to be picked from packages.

Solving the original issue here by merging empty theory prefixes will give some restriction on valid COQPATHs that we can defo uostream to Coq. COQPATH is rarely used in Coq nowadays so a lack of validation shouldn'g be a guiding principle for us.

[ejgallego]

breaks the contract we make with the user about having a valid user-contrib.

What's the contract we make? Note that the first example for example doesn't seem invalid to me, if the semantics of COQPATH are unionfs alike.

the original issue here by merging empty theory prefixes will give some restriction on valid COQPATHs that we can defo uostream to Coq

If that would work I'd be fine with it, but the "empty theory" restriction makes me afraid that it could be too restrictive in the real world. I'm wary of committing to a particular semantics when several are possible.

Maybe we should clarify the semantics upstream first?

Another semantics that would make sense is to actually merge all COQPATH + user-contrib in union-like way, but duplicate-free. I believe that Haskell works that way?

The use case seems important, as in math-comp, a package wants to extend a namespace, so I'm not sure the empty restriction is important here, as long as there are no conflicts.

[ejgallego]

For 3.8.1 we can indeed filter empty prefixes, but it is not clear how some other setups may work with this restriction only (thinking of compcert + floc + vst) for example.

[Alizter]

I suppose then rather than merging the prefix paths we should try to do as Coq does and select the first candidate. We could emit a warning when this is done.

If we have theories A.B and A.C then a user could put both in a Coq path. If A happens to be nonempty then we choose A of A.B whenever a user depends on a theory A. Otherwise we should be able to merge them no problem.

[Alizter]

I've made it so that we always merge and prefer the first coq path theory.

[ejgallego]

Thanks @Alizter for the patch, it looks good to me; we could maybe improve the test cases to capture some other conflict in COQPATH, as a way of documentation, but I let you decide on that.

[ejgallego]

By the way we should encourage dune users to contribute to inspect and contribute to the dune test suite so their use cases are fully covered.

[Alizter]

So one thing that this does change is the detection of duplicate theories that we had before. I suppose for now this is the best we can do if we want to keep as faithful as possible to Coq semantics, but I worry for our users who might have a silent overload of a theory.

[Alizter]

I won't write any more tests for this since we plan to write a whole bunch of tests soon anyway. #7598