The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, Sep 03, 2015 at 07:23:09PM -0700, Gregory Malecha wrote:
> Hello --
> 
> I'm working on a development trying to track down a universe inconsistency
> and I've run into difficulties tracking it down. I have a blank file and do:
> 
> Require Import foo.
> Require Import bar.
> 
> Here I get a universe inconsistency when including bar.
> 
> So I include the text of foo verbatim and run it, I get a universe
> inconsistency. I included contents of foo to find the minimal amount that
> is necessary to retain the universe inconsistency. So now I have,
> 
> (* a bunch of stuff included from foo *)
> Require Import bar. (* <<--- universe inconsistency here *)
> 
> Now I repeat the process on bar. But when I inline the contents of bar and
> evaluate it, Coq accepts all of the definitions without a universe
> inconsistency.
> 
> Is this expected behavior? Are there extra checks that are occuring when
> importing a file that are not processed when the definitions are done
> inline? Is there some reason why inlining should make universes consistent?

Is this related to your work on making vm_compute and universe
polymorphism work correctly in 8.5, or it is an unrelated problem you
are trying to pin down?

To my knowledge, all universes related optimizations (like coalescing
two universes that could be distinct, i.e. imposing an extra constraint
to lower the number of universes) are done only at Qed time, so there
should be no extra check/optimization going on when you save a .vo or
require it.  I know that universes names are still unstable (i.e. they
depend on the file name they appear in).  Still, to my knowledge, this
should only affect pretty printing, not logical consistency (still this
may make your debugging harder...).

Could you share foo and bar?

Also, I guess coqdev would be a more appropriate venue for bugs
concerning 8.5.

Best,
-- 
Enrico Tassi