A dependency graph displayed with dotty. |
## DisclaimerThis 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 ## introductionIn 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 ## How to install Our tools## Downloadingthe 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: 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
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: 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 ## User guideThe 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).
## WarningsCommands starting with "Dotty" will behave normally only if dotty is installed on your machine and available as a regular command (through thePATH variable).
## AuthorsPackage designed by Olivier Pons, this page maintained by Yves Bertot. |

Last modified: Tue Oct 27 09:49:50 MET 2015

Previously modified: Mon Apr 17 16:04:51 MEST 2000