diff options
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 57 |
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") |