A dependency graph displayed with dotty.
This page describes software that was distributed in the years 1998-2000. The maintenance of this software has been discontinued, so that most of the links available in other paragraphs are actually dead. At the time of writing these lines (October 2015), the most up-to-date version of similar software that we are working on is the software available at the following address:
In an effort to provide tools to help maintaining large proof scripts for the Coq system, we have developed a collection of Coq packages that construct graphs representing various aspects of the structure of Coq scripts.
To use these tools, you only need to load our developments in the Coq system, using the Require command and type a command. This command will produce a file containg a description of the graph to display in a simple format. This graph can then be displayed with an off-the-shelf graph displayer. We provide converters from the simple graph format to the format accepted by a few well-known graph displayers, e.g. dotty or daVinci.
How to install Our tools
the package is available from ftp://ftp-sop/lemme/coq-graphs/coq-graphs-6.3.1.tgz. A smaller source package is also available from ftp://ftp-sop.inria.fr/lemme/coq-graphs/coq-graphs-6.3.1-src.tgz.
The package consists in a collection of compiled ML files and vernacular files. These files can only be used with the distributed version of Coq corresponding to the version the files have been compiled with. For example, if your version of Coq is 6.3.1, you should have downloaded a file called: coq-graphs-6.3.1.tgz. Let us suppose that you have placed this file in the directory referred to by the variable $TMP and that you want to place the package in $COQGRAPHDIR. You only need to perform the following operation.
cd $COQGRAPHDIR gunzip -c $TMP/coq-graphs-6.3.1.tgz | tar xf -
Loading the package in Coq
To enable the commands provided by our package in Coq you only need to type the following command at the coqtop prompt.
AddPath "$COQGRAPHDIR/graphs". Add ML Path "$COQGRAPHDIR/graphs". Require Graph_com.
this command should proceed silently. If there is an error message, you may need to perform a source installation, see below.
To re-construct an executable package, it requires that you have also installed Coq from the sources. You simply need to download the source distribution of the graph package: coq-graph-6.3.1-src.tgz and recompile it.
The commands to issue has the following form:
cd $COQGRAPHDIR gunzip -c $TMP/coq-graphs-6.3.1-src.tgz | tar xf - cd graphs make COQTOP=$COQTOP
Here, we assume that the variable $COQTOP designates the location where you have installed Coq.
The package provides the following commands.
WarningsCommands starting with "Dotty" will behave normally only if dotty is installed on your machine and available as a regular command (through the PATH variable).