1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: usage.ml 11858 2009-01-26 13:27:23Z notin $ *)
12
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
13
Coq_config.version Coq_config.date;
14
Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version;
17
(* print the usage of coqtop (or coqc) on channel co *)
19
let print_usage_channel co command =
20
output_string co command;
21
output_string co "Coq options are:\n";
23
" -I dir -as coqdir map physical dir to logical coqdir
24
-I dir map directory dir to the empty logical path
26
-R dir -as coqdir recursively map physical dir to logical coqdir
28
-top coqdir set the toplevel name to be coqdir instead of Top
29
-notop r set the toplevel name to be the empty logical path
30
-exclude-dir f exclude subdirectories named f for option -R
32
-inputstate f read state from file f.coq
34
-nois start with an empty state
35
-outputstate f write state in file f.coq
37
-load-ml-object f load ML object file f
38
-load-ml-source f load ML file f
39
-load-vernac-source f load Coq file f.v (Load f.)
41
-load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)
43
-load-vernac-object f load Coq object file f.vo
44
-require f load Coq object file f.vo and import it (Require f.)
45
-compile f compile Coq file f.v (implies -batch)
46
-compile-verbose f verbosely compile Coq file f.v (implies -batch)
48
-opt run the native-code version of Coq
49
-byte run the bytecode version of Coq
51
-where print Coq's standard library location and exit
52
-v print Coq version and exit
54
-q skip loading of rcfile
55
-init-file f set the rcfile to f
56
-user u use the rcfile of user u
57
-batch batch mode (exits just after arguments parsing)
58
-boot boot mode (implies -q and -batch)
59
-emacs tells Coq it is executed under Emacs
60
-noglob f do not dump globalizations
61
-dump-glob f dump globalizations in file f (to be used by coqdoc)
62
-with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
63
-impredicative-set set sort Set impredicative
64
-dont-load-proofs don't load opaque proofs in memory
65
-xml export XML files either to the hierarchy rooted in
66
the directory $COQ_XML_LIBRARY_ROOT (if set) or to
68
-quality improve the legibility of the proof terms produced by
70
-h, --help print this list of options
73
(* print the usage on standard error *)
75
let print_usage = print_usage_channel stderr
77
let print_usage_coqtop () =
78
print_usage "Usage: coqtop <options>\n\n"
80
let print_usage_coqc () =
81
print_usage "Usage: coqc <options> <Coq options> file...\n
83
-verbose compile verbosely
84
-image f specify an alternative executable for Coq
85
-t keep temporary files\n\n"
87
(* Print the configuration information *)
90
if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
91
Printf.printf "COQLIB=%s/\n" Coq_config.coqlib;
92
Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc;
93
Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin;
94
Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib;
95
Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
96
Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin;
97
Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib