The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,

Debugging universe inconsistencies in large coq developments seems very painful.

Is there a tool to help with this process?

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.

(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?)

Thanks,

-- Abhishek