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.

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

Coq tools                                         28 March 1995                                           COQ(1)