The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Abhishek,

On 28 oct. 2013, at 23:11, Abhishek Anand 
<abhishek.anand.iitg AT gmail.com>
 wrote:

> Hi,
> Debugging universe inconsistencies in large coq developments seems very 
> painful.
> Is there a tool to help with this process?

Not at the moment…

> It seems that the standard way is:
> 
> 1) Go through the thousands of lines that Print Universes outputs, and 
> collect the "relevant ones"
> 
> 2) Map the level numbers to back the occurrences of Type in the coq code
> 
> 3) Reason about the level constraints for the associated typing rules in 
> that code
> 
> Has someone written a tool to partially automate this process and provide a 
> more 
> visual representation of the constraints?
> Ideally, I would like the tool to output a minimal graph that explains the 
> inconsistency 
> and the code associated with all the involved levels. Helpful names instead 
> of numbers as levels would also be useful.

In principle, what you ask for is difficult but not impossible. In my branch 
adding universe polymorphism, definitions/inductives carry not only the 
constraints but also the universe levels they introduced, so you 
could link each global universe level to its place of introduction (it might 
be reused by other definitions 
though). For the minimal graph, the universe inconsistency error carries the 
cycle that would be created, 
so you could easily recreate a minimal graph with just that information to 
display. The main problem is, 
that cycle might result from a combination of constraints whose source (a 
subtyping in some typing derivation) 
is not recorded. However, if a definition f introduces a constraint l < l', 
then it will be declared in the 
universe context associated to f, so you could crawl the global context to 
find out where each atomic 
constraint from the miminal graph comes from: take the minimal graph and 
check if it implies at least one 
constraint l < l' of f, if so, f is part of the "problem". If you're willing 
to work on adding this I'd be 
happy to help.

> (optional question: Wouldn't it be better to have the ability to explicitly 
> provide universe levels(e.g. Nuprl), than to debug a complicated mess of 
> constraints?)

Yes. However, cumulatively is still implicit (subtyping) so you'd still get 
constraints.

Best,
-- Matthieu