coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>>
>
- [Coq-Club] Coq-graphs, Eric Mullen, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Jason Gross, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Eric Mullen, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Frédéric Blanqui, 11/24/2014
- Re: [Coq-Club] Coq-graphs, gallais, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Jason Gross, 11/25/2014
- Re: [Coq-Club] Coq-graphs, gallais, 11/26/2014
- Re: [Coq-Club] Coq-graphs, Jean-Francois Monin, 11/26/2014
- Re: [Coq-Club] Coq-graphs, Jason Gross, 11/25/2014
- Re: [Coq-Club] Coq-graphs, gallais, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Frédéric Blanqui, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Eric Mullen, 11/24/2014
- Re: [Coq-Club] Coq-graphs, Jason Gross, 11/24/2014
Archive powered by MHonArc 2.6.18.