Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq-graphs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq-graphs


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq-graphs
  • Date: Tue, 25 Nov 2014 20:05:41 +0000

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> 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/ 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>> 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>> 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
>>
>




Archive powered by MHonArc 2.6.18.

Top of Page