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: gallais <guillaume.allais AT strath.ac.uk>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq-graphs
  • Date: Mon, 24 Nov 2014 10:26:40 +0000

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