The Coq mailing list

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

I'm writing such a tool for my Coq plugin : https://github.com/aa755/nbcoq

Given a universe level (e.g. Top.13), is there a way to get the name of the definition that contains it?

For example, if Print prod returns:

Inductive prod (A : Type (* Coq.Init.Datatypes.39 *))

          (B : Type (* Coq.Init.Datatypes.40 *))

            : Type (* max(Coq.Init.Datatypes.39, Coq.Init.Datatypes.40) *) :=

    pair : A -> B -> A # B

 

Then the query for Coq.Init.Datatypes.40 should return Coq.Init.Datatypes.prod

If coqtop supports such queries, writing this tool would be much easier for me.

Thanks,

-- Abhishek

On Mon, Oct 28, 2013 at 6:11 PM, 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?

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