The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

What does "strongly" mean in SCC?

-Jason

On Jan 23, 2014 12:18 PM, "Abhishek Anand" <abhishek.anand.iitg AT gmail.com> wrote:

We ran into a universe inconsistency in version 8.4pl2 and tried to debug it using this netbeans-plugin-tool

that I wrote. 

To recap, it parses the constraints output by Print Universes and makes a graph

out of it with equality edges a bidirectional and a<b and a<= b denoted by the edge a <---b

Then I add the violated constraint( the one that cannot be enforced) that is mentioned the error message at Qed time and

find the strongly connected component(SCC) that contains the nodes in the violated constraint.

To our surprise, there were no strict edges(denoting constraints of the form a<b)  in the above mentioned SCC.

It could be a bug in my code.

I just wanted to confirm that following the above algorithm, I should see at least one strict edge in the SCC

and moreover, there should be a simple cycle (in the SCC) that consists of the nodes in the violated constraint and at least one strict edge.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, Nov 9, 2013 at 7:20 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks Jason, Pierre and Matthieu.

Matthieu :

 No, the code do parse the constraints, compute SCC(strongly connected components) and visualize constraint graphs do not use any netbeans libraries.

They use the following free libraries:

http://jung.sourceforge.net/index.html (for graph visualization and layout)

http://jgrapht.org/ (for SCC computation)

All the relevant code is in https://github.com/aa755/nbcoq/blob/master/src/coq/cqDataObject.java

In particular, the class Constraint is used to represent constraints.

void showTopUnivs()

is the entry point for the code that displays all constraints involving levels which start with "Top."

 void debugUnivInconsistency()

is the entry point for the code which displays the SCC containing the constraint that cannot be enforced.

If you need any help in using my code, feel free to ask.

Regards, 

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Nov 8, 2013 at 6:01 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

Hi Abhishek,

  Awesome! I want that! Does it rely on netbeans heavily?

Le 7 nov. 2013 à 19:20, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

> Thanks Pierre and Matthieu.
> So far, viewing the graph of constraints sufficed.
> A constraint of the form a<=b or a<b is shown as an edge
> a <------b.
> (Strict constraints are shown in a  separate color.)
> Equalities are shown an undirected edges.
> I am using the stable release of coq(non-universe polymorphic).
> In this version(8.4pl2), the error mentions only the constraint that cannot be enforced (say c<=d).
> I add this constraint as an edge in the graph and find the strongly connected component which contains c(or d).
> This subgraph must contain any problematic cycle involving c (or d)
> As  Matthieu mentioned, a problematic cycle is one with at least one strict inequality.
> I think that viewing the constraints graphically helps.
> There is an option to view the constraints between levels in current file even when there is no error.
> I pushed these changes to the plugin repo. A video demo can be found at:
> http://www.cs.cornell.edu/~aa755/ConstraintsSmall.avi
>
> If I get time, I might make this tool fully automated by writing the part that collects the
> code relevant to the problematic constraints.
> I'm not sure how to use  Declaremods.iter_all_segments, or Search.generic_search.
> I guess these are not commands which can be sent to coqtop. Somehow, these functions need to
> be exported via coqtop?
> Getting access to coqtop's current state might also be useful for providing better "code-assistance" in my plugin.
> (I already use Locate to implement "Jump to Definition")
>
> I think I understand why implicit cumulativity forces Coq to maintain constraints.
> Is it possible to have an option of disabling implicit cumulativity in some definitions and having
> an Agda-like construct for explcitly raising the universe level of a type?

Not yet, but that should be possible in the new version, as soon as we can all agree on a syntax for
universe instantiation…

> Finally, is there a formal description of the way universe polymorphism is being implemented in Coq?
> I think I understand how it works in Agda. Polymorphic definitions have their universe levels universally quantified.
> I can't relate the Agda way to the way Coq gets away by hiding the levels.

This is mostly the same. In current Coq, they are universally quantified globally (except for arities of inductives
where it is a mix of local and global). In universe polymorphic mode it can additionally be local quantification for
a particular definition/inductive. The closest to what is being implemented is Harper and Pollack’s paper as Jason
mentioned.

> Is the type checking complete w.r.t the analysis of universe levels?
> In other words, if some polymorphic definitions in Coq fails to typecheck in Coq,
> does it mean that there is no way to explicitly provide some universe levels in  the corresponding Agda code
> and get it to type check?

That’s a good question, there is no formal equivalence theorem between the two presentations
but there should be one. In my universe polymorphic branch, it is incomplete because I use
heuristics to simplify the graph (mostly collapse l <= l’ constraints to l = l’ when l was
not introduced by the user), but they work most of the time. Of course with explicit instantiations
we get the same system. At the level of one definition, the heuristic does not change satisfiability
though, so the result holds there.

Thank you,
— Matthieu

> On Wed, Oct 30, 2013 at 5:46 AM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:
> 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
>

-- Matthieu