blob: a0eb96e59486871da9d3534084376a633c2bdff6 (
plain)
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
|
(* $Id$ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
Coq_config.version Coq_config.date;
Printf.printf "compiled on %s\n" Coq_config.compile_date;
exit 0
(* print the usage of coqtop (or coqc) on channel co *)
let print_usage_channel co command =
output_string co command;
output_string co "Options are:\n";
output_string co
" -I dir add directory dir in the include path
-include dir (idem)
-R dir coqdir recursively map physical dir to logical coqdir
-src add source directories in the include path
-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
-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.)
-load-vernac-object f load Coq object file f.vo
-require f load Coq object file f.vo and import it (Require f.)
-opt run the native-code version of Coq or Coq_SearchIsos
-image f specify an alternative binary image f
-bindir dir specify an alternative directory for the binaries
-libdir dir specify an alternative directory for the library
-where print Coq's standard library location 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)
-emacs tells Coq it is executed under Emacs
"
(* print the usage on standard error *)
let print_usage = print_usage_channel stderr
let print_usage_coqtop () =
print_usage "Usage: coqtop <options>\n";
output_string stderr
" -searchisos run Coq_SearchIsos\n"
let print_usage_coqc () =
print_usage "Usage: coqc [-i] [-t] <options> file...\n
-i compile specification only (in file.vi)
-t keep temporary files\n\n"
|