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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <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 *)
(************************************************************************)
(** Coq compiler : coqc *)
(** For improving portability, coqc is now an OCaml program instead
of a shell script. We use as much as possible the Sys and Filename
module for better portability, but the Unix module is still used
here and there (with explicitly qualified function names Unix.foo).
We process here the commmand line to extract names of files to compile,
then we compile them one by one while passing by the rest of the command
line to a process running "coqtop -batch -compile <file>".
*)
let binary = ref "coqtop"
let image = ref ""
let verbose = ref false
let rec make_compilation_args = function
| [] -> []
| file :: fl ->
let file_noext =
if Filename.check_suffix file ".v" then
Filename.chop_suffix file ".v"
else file
in
(if !verbose then "-compile-verbose" else "-compile")
:: file_noext :: (make_compilation_args fl)
(* compilation of files [files] with command [command] and args [args] *)
let compile command args files =
let args' = command :: args @ (make_compilation_args files) in
Unix.execvp command (Array.of_list args')
let usage () =
Usage.print_usage_coqc () ;
flush stderr ;
exit 1
(* parsing of the command line *)
let extra_arg_needed = ref true
let parse_args () =
let rec parse (cfiles,args) = function
| [] ->
List.rev cfiles, List.rev args
| ("-verbose" | "--verbose") :: rem ->
verbose := true ; parse (cfiles,args) rem
| "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
| "-image" :: [] -> usage ()
| "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
| "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
(* Obsolete options *)
| "-libdir" :: _ :: rem ->
print_string "Warning: option -libdir deprecated and ignored\n";
flush stdout;
parse (cfiles,args) rem
| ("-db"|"-debugger") :: rem ->
print_string "Warning: option -db/-debugger deprecated and ignored\n";
flush stdout;
parse (cfiles,args) rem
(* Informative options *)
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
| ("-v"|"--version") :: _ -> Usage.version 0
| ("-where") :: _ ->
Envars.set_coqlib (fun x -> x);
print_endline (Envars.coqlib ());
exit 0
| ("-config" | "--config") :: _ ->
Envars.set_coqlib (fun x -> x);
Usage.print_config ();
exit 0
(* Options for coqtop : a) options with 0 argument *)
| ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
|"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
|"-impredicative-set"|"-vm"|"-no-native-compiler"
|"-verbose-compat-notations"|"-no-compat-notations"
|"-indices-matter"|"-quick"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
as o) :: rem ->
parse (cfiles,o::args) rem
(* Options for coqtop : b) options with 1 argument *)
| ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
|"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
|"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
| [] -> usage ()
end
(* Options for coqtop : c) options with 1 argument and possibly more *)
| ("-I"|"-include" as o) :: rem ->
begin
match rem with
| s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem'
| s :: "-as" :: [] -> usage ()
| s :: rem' -> parse (cfiles,s::o::args) rem'
| [] -> usage ()
end
| "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem
| "-R" :: s :: "-as" :: [] -> usage ()
| "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
| "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
| ("-schedule-vi-checking"
|"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem ->
let nodash, rem =
CList.split_when (fun x -> String.length x > 1 && x.[0] = '-') rem in
extra_arg_needed := false;
parse (cfiles, List.rev nodash @ s :: o :: args) rem
| f :: rem ->
if Sys.file_exists f then
parse (f::cfiles,args) rem
else
let fv = f ^ ".v" in
if Sys.file_exists fv then
parse (fv::cfiles,args) rem
else begin
prerr_endline ("coqc: "^f^": no such file or directory") ;
exit 1
end
in
parse ([],[]) (List.tl (Array.to_list Sys.argv))
(* main: we parse the command line, define the command to compile files
* and then call the compilation on each file *)
let main () =
let cfiles, args = parse_args () in
if cfiles = [] && !extra_arg_needed then begin
prerr_endline "coqc: too few arguments" ;
usage ()
end;
let coqtopname =
if !image <> "" then !image
else Filename.concat Envars.coqbin (!binary ^ Coq_config.exec_extension)
in
(* List.iter (compile coqtopname args) cfiles*)
Unix.handle_unix_error (compile coqtopname args) cfiles
let _ = Printexc.print main ()
|
