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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 outputstate opts =
Option.iter (fun ostate_file ->
let fname = CUnix.make_suffix ostate_file ".coq" in
Vernacstate.System.dump fname) opts.Coqcargs.outputstate
let coqc_init _copts ~opts =
Flags.quiet := true;
System.trust_file_cache := true;
Coqtop.init_color opts.Coqargs.config
let coqc_specific_usage = Usage.{
executable_name = "coqc";
extra_args = "file...";
extra_options = "\n\
coqc specific options:\
\n -o f.vo use f.vo as the output file name\
\n -verbose compile and output the input file\
\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 -vos process statements but ignore opaque proofs, and produce a .vos file\
\n -vok process the file by loading .vos instead of .vo files for\
\n dependencies, and produce an empty .vok file on success\
\n -vio process statements and suspend opaque proofs, and produce a .vio file\
\n\
\nUndocumented:\
\n -quick (deprecated) alias for -vio\
\n -vio2vo [see manual]\
\n -check-vio-tasks [see manual]\
\n"
}
let coqc_main (copts,stm_opts) ~opts =
Topfmt.(in_phase ~phase:CompilationPhase)
Ccompile.compile_files (opts,stm_opts) copts;
(* Careful this will modify the load-path and state so after this
point some stuff may not be safe anymore. *)
Topfmt.(in_phase ~phase:CompilationPhase)
Ccompile.do_vio opts copts;
(* Allow the user to output an arbitrary state *)
outputstate copts;
flush_all();
if opts.Coqargs.post.Coqargs.output_context then begin
let sigma, env = let e = Global.env () in Evd.from_env e, e in
Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
end;
CProfile.print_profile ()
let coqc_run copts ~opts () =
let _feeder = Feedback.add_feeder Coqloop.coqloop_feed in
try
coqc_main ~opts copts;
exit 0
with exn ->
flush_all();
Topfmt.print_err_exn exn;
flush_all();
let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
exit exit_code
let custom_coqc : (Coqcargs.t * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel
= Coqtop.{
parse_extra = (fun ~opts extras ->
let stm_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
(Coqcargs.parse extras, stm_opts), []);
help = coqc_specific_usage;
init = coqc_init;
run = coqc_run;
opts = Coqargs.default;
}
let main () =
Coqtop.start_coq custom_coqc
|
