coqdep - Online in the Cloud

PROGRAM:

NAME

coqdep - Compute inter-module dependencies for Coq and Caml programs

SYNOPSIS

coqdep [ -w ] [ -I directory ] [ -coqlib directory ] [ -c ] [ -i ] [ -D ] [ -slash ]
filename ... directory ...

DESCRIPTION

coqdep compute inter-module dependencies for Coq and Caml programs, and prints the
dependencies on the standard output in a format readable by make. When a directory is
given as argument, it is recursively looked at.

Dependencies of Coq modules are computed by looking at Require commands (Require, Require
Export, Require Import), Declare ML Module commands and Load commands. Dependencies
relative to modules from the Coq library are not printed.

Dependencies of Caml modules are computed by looking at open directives and the dot
notation module.value.

OPTIONS

-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is
exactly the same as ocamldep).

-w Prints a warning if a Coq command Declare ML Module is incorrect. (For instance,
you wrote `Declare ML Module "A".', but the module A contains #open "B"). The
correct command is printed (see option -D). The warning is printed on standard
error.

-D This commands looks for every command Declare ML Module of each Coq file given as
argument and complete (if needed) the list of Caml modules. The new command is
printed on the standard output. No dependency is computed with this option.

-slash Prints paths using a slash instead of the OS specific separator. This option is
useful when developping under Cygwin.

-I directory
The files .v .ml .mli of the directory directory are taken into account during the
calculus of dependencies, but their own dependencies are not printed.

-coqlib directory
Indicates where is the Coq library. The default value has been determined at
installation time, and therefore this option should not be used under normal
circumstances.

Use coqdep online using onworks.net services