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