The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

There is an undocumented option (-dumpgraphbox)grouping modules into 
(nested)
clusters based on the directories they live in. We used to draw boxes around
these clusters (hence the name) but I guess it might be possible to get dot
to vary the colours instead?
If it's not possible, patching the printing function to do that should be
quite easy anyways because all the information is already available (the 
modules
are listed in a rosetree where the nodes carry directory names and the 
leaves
are the files' names): 
https://github.com/coq/coq/blob/trunk/tools/coqdep.ml#L382


On 25/11/14 20:05, Jason Gross wrote:
> Neat!  However, dpdgraph is for dependencies between theorems and 
> definitions, not just files/modules.
>
> Is there any way to get -dumpgraph to color the modules by which 
> folder they live in?
> On Tue Nov 25 2014 at 5:34:37 AM gallais 
> <guillaume.allais AT strath.ac.uk <mailto:guillaume.allais AT strath.ac.uk>> 
> wrote:
>
>     Hi,
>
>     If that is a tool printing a dependency graph between the various
>     modules
>     of a project then there is no need to install anything: Pierre
>     Marie Pédrot
>     ported the patch we used to use internally in the coqtail project to
>     upstream
>     coqdep:
>
>     https://github.com/coq/coq/commit/093529c6d4f8eba7370c30b97d8d648340039374
>
>     Cheers,
>
>     On 24/11/14 09:49, Frédéric Blanqui wrote:
>     > Hi! Perhaps http://www-verimag.imag.fr/~monin/Soft/Dependot/
>     <http://www-verimag.imag.fr/%7Emonin/Soft/Dependot/> may be of
>     > interest too. Best regards, Frédéric.
>     >
>     > Le 24/11/2014 06:46, Eric Mullen a écrit :
>     >> Thanks! I'll look into dpdgraph. Much appreciated!
>     >>
>     >> Eric
>     >>
>     >> On Sun Nov 23 2014 at 9:44:02 PM Jason Gross
>     
> <jasongross9 AT gmail.com
>  
> <mailto:jasongross9 AT gmail.com>
>     >> 
> <mailto:jasongross9 AT gmail.com
>  
> <mailto:jasongross9 AT gmail.com>>>
>     wrote:
>     >>
>     >>     The links on that site also talk about Coq 6.3 being the latest
>     >>     version of Coq.  When I asked about this a while ago I was
>     >>     pointed at dpdgraph.  I don't recall where the original sources
>     >>     are (a google search might give them), there's a variant that
>     >>     works with a recent trunk at
>     >> https://github.com/HoTT/HoTT/tree/master/etc/dpdgraph-0.4alpha,
>     >>     and if you look through the history, the first version added
>     >>     might work with 8.4.
>     >>
>     >>     -Jason
>     >>
>     >>     On Nov 24, 2014 12:16 AM, "Eric Mullen"
>     >>     
> <emullen AT cs.washington.edu
>     
> <mailto:emullen AT cs.washington.edu>
>     
> <mailto:emullen AT cs.washington.edu
>     
> <mailto:emullen AT cs.washington.edu>>>
>  wrote:
>     >>
>     >>         I'm interested in building a tool to visualize
>     theorem/lemma
>     >>         dependencies and proof status (admitted or proven) in order
>     >>         to help with project management of large verification
>     >>         projects. I found the website for this tool
>     >>         (http://www-sop.inria.fr/lemme/coq-graphs/) but both of the
>     >>         download links give me back ERR_FTP_FAILED. Is there
>     another
>     >>         way I could get this tool, or is there a proper person
>     for me
>     >>         to contact about the links being bad?
>     >>
>     >>         Thanks!
>     >>         Eric Mullen
>     >>         University of Washington
>     >>
>     >