1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
(************************************************************************)
(* * 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 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
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 ret
let machine_readable_version ret =
Printf.printf "%s %s\n"
Coq_config.version Coq_config.caml_version;
exit 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_common co command =
output_string co command;
output_string co "Coq options are:\n";
output_string co
" -I dir look for ML files in dir\
\n -include dir (idem)\
\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 -topfile f set the toplevel name as though compiling f\
\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\
\n -nois (idem)\
\n -compat X.Y provides compatibility support for Coq version X.Y\
\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 lib, -r lib\
\n load Coq library lib (Require lib)\
\n -rfrom root lib load Coq library lib (From root Require lib.)\
\n -require-import lib, -ri lib\
\n load and import Coq library lib\
\n (equivalent to Require Import lib.)\
\n -require-export lib, -re lib\
\n load and transitively import Coq library lib\
\n (equivalent to Require Export lib.)\
\n -require-import-from root lib, -rifrom lib\
\n load and import Coq library lib\
\n (equivalent to From root Require Import lib.)\
\n -require-export-from root lib, -refrom lib\
\n load and transitively import Coq library lib\
\n (equivalent to From root Require Export lib.)\
\n\
\n -where print Coq's standard library location and exit\
\n -config, --config print Coq's configuration information 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\")\
\n -w (w1,..,wn) configure display of warnings\
\n -color (yes|no|auto) configure color output\
\n -emacs tells Coq it is executed under Emacs\
\n\
\n -q skip loading of rcfile\
\n -init-file f set the rcfile to f\
\n -bt print backtraces (requires configure debug flag)\
\n -debug debug mode (implies -bt)\
\n -diffs (on|off|removed) highlight differences between proof steps\
\n -stm-debug STM debug mode (will trace every transaction)\
\n -noglob do not dump globalizations\
\n -dump-glob f dump globalizations in file f (to be used by coqdoc)\
\n -impredicative-set set sort Set impredicative\
\n -allow-sprop allow using the proof irrelevant SProp sort\
\n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -type-in-type disable universe consistency checking\
\n -mangle-names x mangle auto-generated names using prefix x\
\n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\
\n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\
\n -unset \"Foo Bar\" disable Foo Bar (as Unset Foo Bar. in a file)\
\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 -bytecode-compiler (yes|no) enable the vm_compute reduction machine\
\n -native-compiler (yes|no|ondemand) enable the native_compute reduction machine\
\n -h, -help, --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_coqtop () =
print_usage_common stderr "Usage: coqtop <options>\n\n";
output_string stderr "\n\
coqtop specific options:\
\n\
\n -batch batch mode (exits just after argument parsing)\
\n";
flush stderr ;
exit 1
let print_usage_coqc () =
print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
output_string stderr "\n\
coqc specific options:\
\n\
\n -o f.vo use f.vo as the output file name\
\n -verbose compile and output the input file\
\n -quick quickly compile .v files to .vio files (skip proofs)\
\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\
\n into fi.vo\
\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\
\n proofs in each fi.vio\
\n\
\nUndocumented:\
\n -vio2vo [see manual]\
\n -check-vio-tasks [see manual]\
\n";
flush stderr ;
exit 1
|
