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 except if -boot is given.

       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).

       -I/-Q/-R options
              Have the same effects on load path and modules names than for  other  coq  commands
              (coqtop, coqc).

       -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.

       -dumpgraph[box] file
              Dumps a dot dependency graph in file file.

       -exclude-dir dir
              Skips subdirectory dir during -R/-Q search.

       -sort  Output the given file name ordered by dependencies.

       -boot  For  coq  developpers,  prints  dependencies  over  coq  library  files (omitted by
              default).

SEE ALSO

       ocamlc(1), coqc(1), make(1).

NOTES

       Lexers (for Coq and Caml) correctly handle nested comments and strings.

       The treatment of symbolic links is primitive.

       If two files have the same name, in two different directories, a  warning  is  printed  on
       standard error.

       There is no way to limit the scope of the recursive search for directories.

EXAMPLES

       Consider the files (in the same directory):

            A.ml B.ml C.ml D.ml X.v Y.v and Z.v

       where

       +      D.ml contains the commands `open A', `open B' and `type t = C.t' ;

       +      Y.v contains the command `Require X' ;

       +      Z.v contains the commands `Require X' and `Declare ML Module "D"'.

       To get the dependencies of the Coq files:

              example% coqdep -I . *.v
              Z.vo: Z.v ./X.vo ./D.cmo
              Y.vo: Y.v ./X.vo
              X.vo: X.v

       With a warning:

              example% coqdep -w -I . *.v
              Z.vo: Z.v ./X.vo ./D.cmo
              Y.vo: Y.v ./X.vo
              X.vo: X.v
              ### Warning : In file Z.v, the ML modules declaration should be
              ### Declare ML Module "A" "B" "C" "D".

       To get only the Caml dependencies:

              example% coqdep -c -I . *.ml
              D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
              D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
              C.cmo: C.ml
              C.cmx: C.ml
              B.cmo: B.ml
              B.cmx: B.ml
              A.cmo: A.ml
              A.cmx: A.ml

BUGS

       Please report any bug to coq-bugs@pauillac.inria.fr