A dependency graph displayed with dotty.
Disclaimer
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:
https://github.com/Karmaki/coq-dpdgraph
introduction
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.
- Coercions, Coercions are used to ease data input and output when some type can be viewed as a subtype of another. The natural injection from one type to the other can be declared as a coercion. The collection of all declared coercions can be represented as a directed graph that often helps understand the structure of mathematical theories.
- Dependencies between theorems and definitions, an easy analysis of proof terms makes it possible to know whether some theorem is used when proving another one or when defining a new concept. Visualizing the complete graph of dependence is useful to detect those development that are not used and to foresee the impact of modifying a theorem or definition.
- Dependencies between proof commands, when performing goal-directed proof, the usual proof mode in coq, you issue a sequence of commands, where each command does not necessarily depend on all the commands that precede them. Visualizing the dependency tree makes it easier to localize important commands.
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
Downloading
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.
Binary installation
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.
Source installation
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.
User guide
The package provides the following commands.
- FileCoerceGraph <file name>.
- Dumps a representation of the current Coercion graph into the file file name (a string).
- FileDepAfter <start definition> <start package> <file name>.
- Dumps a representation of the dependency graph into the file file name (a string), showing dependencies only for theorems and definitions given after <start definition> (a string) and present in packages loaded after <start package> (a string).
- FileProofTree <file name>.
- Dumps a representation of the current proof tree into the file file name (a string).
- DottyCoerceGraph.
- Calls the dotty graph editor to display to display the current Coercion graph. Please read this warning.
- DottyDepAfter <start definition> <start package>.
- Calls dotty to display the dependency graph, showing dependencies only for theorems and definitions given after <start definition> (a string) and present in packages loaded after <start package> (a string). Please read this warning.
- FileProofTree <file name>.
- Calls dotty to display the current proof tree into the file file name (a string).
Warnings
Commands starting with "Dotty" will behave normally only if dotty is installed on your machine and available as a regular command (through the PATH variable).Authors
Package designed by Olivier Pons, this page maintained by Yves Bertot.