The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  indeed that might be it. The constraints of the current proof are generated 
at Qed time
in 8.4, so you won’t see all of them. Indeed that’s “fixed" in my version, as 
the current
constraints are available, except Print Universes still shows only the global 
ones. Otherwise
I’d love to see the example, afaict your account is right Abhishek.

Cheers,
— Matthieu

On 23 janv. 2014, at 14:59, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> No, it was a serious question.
> 
> Is it possible that Qed adds multiple constraints, but you only notice one 
> of them, but there's only an inconsistency in adding both simultaneously?  
> For example, does the following example give your tool trouble?
> 
> Definition U0 := Type.
> Definition U1 := Type.
> 
> Set Printing Universes.
> 
> Inductive foo A (x : A) B (x : B) : Set := .
> 
> Goal Set.
>   refine (@foo U0 _ U1 _).
>   hnf.
>   exact U1.
>   hnf.
>   exact U0.
>   Print Universes. (* Neither Top.1 nor Top.2 shows up anywhere *)
> Qed. (* Error: Universe inconsistency (cannot enforce Top.1 < Top.2). *)
> 
> 
> I believe that the universe printing in Matthieu's polyproj branch (and in 
> 8.5) is/will be much better, and will print the relevant universe context 
> (though no pretty pictures) when it reports a universe inconsistency.
> 
> -Jason
> 
> 
> On Thu, Jan 23, 2014 at 2:39 PM, J. Ian Johnson 
> <ianj AT ccs.neu.edu>
>  wrote:
> Unless that's a rhetorical question trying to point at a flaw in the 
> approach...
> A subgraph is a connected component if all nodes in that graph have a path 
> to them from some other node in the component.
> A subgraph is /strongly/ connected if all nodes in the component have paths 
> to all other nodes in the component (there is always a way to get from A to 
> B).
> If there is a strict edge in a strongly connected component, by Jones' size 
> change principle there is an infinitely descending chain, which would be 
> inconsistent.
> If there are only non-strict edges, it is reasonable to say that every node 
> in the component should be considered at the same universe level, which is 
> consistent.
> -Ian
> ----- Original Message -----
> From: "Jason Gross" 
> <jasongross9 AT gmail.com>
> To: "Abhishek Anand" 
> <abhishek.anand.iitg AT gmail.com>
> Cc: "Coq Club" 
> <coq-club AT inria.fr>,
>  "Matthieu Sozeau" 
> <mattam AT mattam.org>
> Sent: Thursday, January 23, 2014 5:25:00 PM GMT -05:00 US/Canada Eastern
> Subject: Re: [Coq-Club] universe inconsistency: constraints visualization
> 
> 
> 
> 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
> 
> 
> 
>