Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
COQ(1)			    General Commands Manual			COQ(1)

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 li-
       brary 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	 warn-
       ing is printed on standard error.

       There is	no way to limit	the scope of the recursive search for directo-
       ries.

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)

NAME | SYNOPSIS | DESCRIPTION | OPTIONS | SEE ALSO | NOTES | EXAMPLES | BUGS

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=coqdep&sektion=1&manpath=FreeBSD+12.1-RELEASE+and+Ports>

home | help