diff options
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 36 |
1 files changed, 12 insertions, 24 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 38ceacf5..504ffa52 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) let version ret = @@ -30,7 +32,7 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \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 -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ @@ -56,7 +58,8 @@ let print_usage_channel co command = \n\ \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ -\n -v print Coq version and exit\ +\n -v, --version print Coq version and exit\ +\n -print-version print Coq version in easy to parse format and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ \n -quiet unset display of extra information (implies -w \"-all\")\ @@ -69,22 +72,20 @@ let print_usage_channel co command = \n -boot boot mode (implies -q and -batch)\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ +\n -stm-debug STM debug mode (will trace every transaction) \ \n -emacs tells Coq it is executed under Emacs\ \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 -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\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 -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -\n for full Gc stats dump) +\n for full Gc stats dump)\ \n -native-compiler precompile files for the native_compute machinery\ \n -h, -help, --help print this list of options\ \n"; @@ -115,16 +116,3 @@ let print_usage_coqc () = flush stderr ; exit 1 -(* Print the configuration information *) - -let print_config () = - if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n"; - Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); - Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); - Printf.printf "OCAMLFIND=%s\n" (Envars.ocamlfind ()); - 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") |