summaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml57
1 files changed, 34 insertions, 23 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 52bd2d33..d4d44569 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -14,23 +14,25 @@ let version ret =
(* print the usage of coqtop (or coqc) on channel co *)
+let extra_usage = ref []
+let add_to_usage name text = extra_usage := (name,text) :: !extra_usage
+
let print_usage_channel co command =
output_string co command;
output_string co "Coq options are:\n";
output_string co
-" -I dir -as coqdir map physical dir to logical coqdir\
-\n -I dir map directory dir to the empty logical path\
+" -I dir look for ML files in dir\
\n -include dir (idem)\
+\n -I dir -as coqdir implicitly map physical dir to logical coqdir\
\n -R dir -as coqdir recursively map physical dir to logical coqdir\
\n -R dir coqdir (idem)\
+\n -Q dir coqdir map physical dir to logical coqdir\
\n -top coqdir set the toplevel name to be coqdir instead of Top\
\n -notop set the toplevel name to be the empty logical path\
\n -exclude-dir f exclude subdirectories named f for option -R\
\n\
-\n -inputstate f read state from file f.coq\
-\n -is f (idem)\
-\n -nois start with an empty state\
-\n -outputstate f write state in file f.coq\
+\n -noinit start without loading the Init library\
+\n -nois (idem)\
\n -compat X.Y provides compatibility support for Coq version X.Y\
\n -verbose-compat-notations be warned when using compatibility notations\
\n -no-compat-notations get an error when using compatibility notations\
@@ -46,47 +48,54 @@ let print_usage_channel co command =
\n -compile f compile Coq file f.v (implies -batch)\
\n -compile-verbose f verbosely compile Coq file f.v (implies -batch)\
\n\
-\n -opt run the native-code version of Coq\
-\n -byte run the bytecode version of Coq\
-\n\
\n -where print Coq's standard library location and exit\
\n -config print Coq's configuration information and exit\
\n -v print Coq version and exit\
+\n -list-tags print highlight color tags known by Coq and exit\
\n\
\n -q skip loading of rcfile\
\n -init-file f set the rcfile to f\
\n -batch batch mode (exits just after arguments parsing)\
\n -boot boot mode (implies -q and -batch)\
+\n -bt print backtraces (requires configure debug flag)\
+\n -debug debug mode (implies -bt)\
\n -emacs tells Coq it is executed under Emacs\
+\n -color (on|off|auto) configure color output (only active through coqtop)\
\n -noglob do not dump globalizations\
\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
\n -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
\n -impredicative-set set sort Set impredicative\
-\n -force-load-proofs load opaque proofs in memory initially\
-
-\n -lazy-load-proofs load opaque proofs in memory by necessity (default)\
-\n -dont-load-proofs see opaque proofs as axioms instead of loading them\
-\n -xml export XML files either to the hierarchy rooted in\
-\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
-\n stdout (if unset)\
-\n -quality improve the legibility of the proof terms produced by\
-\n some tactics\
-\n -h, --help print this list of options\
-\n"
+\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
+\n -time display the time taken by each command\
+\n -no-native-compiler disable the native_compute reduction machinery\
+\n -h, -help print this list of options\
+\n";
+ List.iter (fun (name, text) ->
+ output_string co
+ ("\nWith the flag '-toploop "^name^
+ "' these extra option are also available:\n"^
+ text^"\n"))
+ !extra_usage
(* print the usage on standard error *)
let print_usage = print_usage_channel stderr
let print_usage_coqtop () =
- print_usage "Usage: coqtop <options>\n\n"
+ print_usage "Usage: coqtop <options>\n\n";
+ flush stderr ;
+ exit 1
let print_usage_coqc () =
print_usage "Usage: coqc <options> <Coq options> file...\n\
\noptions are:\
\n -verbose compile verbosely\
\n -image f specify an alternative executable for Coq\
-\n -t keep temporary files\n\n"
+\n -opt run the native-code version of Coq\
+\n -byte run the bytecode version of Coq\
+\n -t keep temporary files\n\n";
+ flush stderr ;
+ exit 1
(* Print the configuration information *)
@@ -101,6 +110,8 @@ let print_config () =
Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ());
Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ());
Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
+ Printf.printf "CAMLP4O=%s\n" Coq_config.camlp4o;
Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ());
Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ());
+ Printf.printf "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")