The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

In that case let me second Frederic's advice about
http://www-verimag.imag.fr/~monin/Soft/Dependot/ ;)
(unlesss I missed your point).

We used this lightweight tool for years in projects
ranging from small to large size.

Cheers,
Jean-Francois

On Tue, Nov 25, 2014 at 08:05:41PM +0000, 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
>    
> <[1]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:
> 
>      
> [2]https://github.com/coq/coq/commit/093529c6d4f8eba7370c30b97d8d648340039374
> 
>      Cheers,
> 
>      On 24/11/14 09:49, Frédéric Blanqui wrote:
>      > Hi! Perhaps [3]http://www-verimag.imag.fr/~monin/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
>      
> <[4]jasongross9 AT gmail.com
>      >> 
> <mailto:[5]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
>      >>   
>       [6]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"
>      >>     
> <[7]emullen AT cs.washington.edu
>      
> <mailto:[8]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
>      >>         ([9]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
>      >>
>      >
> 

-- 
Jean-Francois Monin