diff options
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r-- | toplevel/usage.ml | 143 |
1 files changed, 74 insertions, 69 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 0282f30a..f6505e30 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: usage.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - -let version () = +let version ret = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; - exit 0 + exit ret (* print the usage of coqtop (or coqc) on channel co *) @@ -20,57 +18,61 @@ 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 - -I dir map directory dir to the empty logical path - -include dir (idem) - -R dir -as coqdir recursively map physical dir to logical coqdir - -R dir coqdir (idem) - -top coqdir set the toplevel name to be coqdir instead of Top - -notop r set the toplevel name to be the empty logical path - -exclude-dir f exclude subdirectories named f for option -R - - -inputstate f read state from file f.coq - -is f (idem) - -nois start with an empty state - -outputstate f write state in file f.coq - -compat X.Y provides compatibility support for Coq version X.Y - - -load-ml-object f load ML object file f - -load-ml-source f load ML file f - -load-vernac-source f load Coq file f.v (Load f.) - -l f (idem) - -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.) - -lv f (idem) - -load-vernac-object f load Coq object file f.vo - -require f load Coq object file f.vo and import it (Require f.) - -compile f compile Coq file f.v (implies -batch) - -compile-verbose f verbosely compile Coq file f.v (implies -batch) - - -opt run the native-code version of Coq - -byte run the bytecode version of Coq - - -where print Coq's standard library location and exit - -config print Coq's configuration information and exit - -v print Coq version and exit - - -q skip loading of rcfile - -init-file f set the rcfile to f - -user u use the rcfile of user u - -batch batch mode (exits just after arguments parsing) - -boot boot mode (implies -q and -batch) - -emacs tells Coq it is executed under Emacs - -noglob do not dump globalizations - -dump-glob f dump globalizations in file f (to be used by coqdoc) - -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) - -impredicative-set set sort Set impredicative - -dont-load-proofs don't load opaque proofs in memory - -xml export XML files either to the hierarchy rooted in - the directory $COQ_XML_LIBRARY_ROOT (if set) or to - stdout (if unset) - -quality improve the legibility of the proof terms produced by - some tactics - -h, --help print this list of options -" +" -I dir -as coqdir map physical dir to logical coqdir\ +\n -I dir map directory dir to the empty logical path\ +\n -include dir (idem)\ +\n -R dir -as coqdir recursively map physical dir to logical coqdir\ +\n -R dir coqdir (idem)\ +\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 -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\ +\n\ +\n -load-ml-object f load ML object file f\ +\n -load-ml-source f load ML file f\ +\n -load-vernac-source f load Coq file f.v (Load f.)\ +\n -l f (idem)\ +\n -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)\ +\n -lv f (idem)\ +\n -load-vernac-object f load Coq object file f.vo\ +\n -require f load Coq object file f.vo and import it (Require f.)\ +\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\ +\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 -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 -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" (* print the usage on standard error *) @@ -80,22 +82,25 @@ let print_usage_coqtop () = print_usage "Usage: coqtop <options>\n\n" let print_usage_coqc () = - print_usage "Usage: coqc <options> <Coq options> file...\n -options are: - -verbose compile verbosely - -image f specify an alternative executable for Coq - -t keep temporary files\n\n" + 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" (* 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" Coq_config.coqlib; - Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc; - Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin; - Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib; + Printf.printf "COQLIB=%s/\n" (Envars.coqlib ()); + Printf.printf "DOCDIR=%s/\n" (Envars.docdir ()); + Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep; + Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc; + Printf.printf "OCAMLOPT=%s\n" Coq_config.ocamlopt; + Printf.printf "OCAMLDOC=%s\n" Coq_config.ocamldoc; + Printf.printf "CAMLBIN=%s/\n" (Envars.camlbin ()); + Printf.printf "CAMLLIB=%s/\n" (Envars.camllib ()); Printf.printf "CAMLP4=%s\n" Coq_config.camlp4; - Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin; - Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib - - + Printf.printf "CAMLP4BIN=%s/\n" (Envars.camlp4bin ()); + Printf.printf "CAMLP4LIB=%s\n" (Envars.camlp4lib ()); + Printf.printf "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false") |