From d6d81d63591e37fd74c841165afd9e3baf6e0d8d Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 13 Nov 2015 15:56:47 +0100 Subject: Fix #4408. Removed documentation for broken -D -w (but the option are still there). Fixed documentation of others. --- man/coqdep.1 | 65 ++++++++++++++++++++++++++++++++++++--------------------- tools/coqdep.ml | 13 +++++++----- 2 files changed, 49 insertions(+), 29 deletions(-) diff --git a/man/coqdep.1 b/man/coqdep.1 index 5a6cd609e..81f7e1e0d 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -46,7 +46,9 @@ commands (Require, Require Export, Require Import), commands and .IR Load \& commands. Dependencies relative to modules from the Coq library are not -printed. +printed except if +.BR \-boot \& +is given. Dependencies of Caml modules are computed by looking at .IR open \& @@ -59,35 +61,50 @@ directives and the dot notation .BI \-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is exactly the same as ocamldep). -.TP -.BI \-w -Prints a warning if a Coq command -.IR Declare \& -.IR ML \& -.IR 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. -.TP -.BI \-D -This commands looks for every command -.IR Declare \& -.IR ML \& -.IR 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. +\" THESE OPTIONS ARE BROKEN CURRENTLY +\" .TP +\" .BI \-w +\" Prints a warning if a Coq command +\" .IR Declare \& +\" .IR ML \& +\" .IR 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. +\" .TP +\" .BI \-D +\" This commands looks for every command +\" .IR Declare \& +\" .IR ML \& +\" .IR 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. .TP -.BI \-I \ directory -The files .v .ml .mli of the directory -.IR directory \& -are taken into account during the calculus of dependencies, -but their own dependencies are not printed. +.BI \-I/\-Q/\-R \ options +Have the same effects on load path and modules names than for other +coq commands (coqtop, coqc). .TP .BI \-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. +.TP +.BI \-dumpgraph[box] \ file +Dumps a dot dependency graph in file +.IR file \&. +.TP +.BI \-exclude-dir \ dir +Skips subdirectory +.IR dir \ during +.BR -R/-Q \ search. +.TP +.B \-sort +Output the given file name ordered by dependencies. +.TP +.B \-boot +For coq developpers, prints dependencies over coq library files +(omitted by default). .SH SEE ALSO diff --git a/tools/coqdep.ml b/tools/coqdep.ml index e51572fc3..011293a90 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -428,10 +428,13 @@ end let usage () = eprintf " usage: coqdep [options] +\n"; eprintf " options:\n"; - eprintf " -c : \n"; - eprintf " -D : \n"; - eprintf " -w : \n"; - eprintf " -boot : \n"; + eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; + (* Does not work anymore *) + (* eprintf " -w : Print informations on missing or wrong \"Declare + ML Module\" commands in coq files.\n"; *) + (* Does not work anymore: *) + (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) + eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; eprintf " -I dir -as logname : adds (non recursively) dir to coq load path under logical name logname\n"; @@ -441,7 +444,7 @@ let usage () = eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; - eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R search\n"; + eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; -- cgit v1.2.3