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
open Coqargs
open Coqcargs
open Common_compile
let create_empty_file filename =
let f = open_out filename in
close_out f
let source ldir file = Loc.InFile {
dirpath=Some (Names.DirPath.to_string ldir);
file = file;
}
let compile opts stm_options injections copts ~echo ~f_in ~f_out =
let open Vernac.State in
let output_native_objects = match opts.config.native_compiler with
| NativeOff -> false | NativeOn {ondemand} -> not ondemand
in
let mode = copts.compilation_mode in
let ext_in, ext_out =
match mode with
| BuildVo -> ".v", ".vo"
| BuildVos -> ".v", ".vos"
| BuildVok -> ".v", ".vok"
in
let long_f_dot_in, long_f_dot_out =
ensure_exists_with_prefix ~src:f_in ~tgt:f_out ~src_ext:ext_in ~tgt_ext:ext_out in
let dump_empty_vos () =
let long_f_dot_vos = (safe_chop_extension long_f_dot_out) ^ ".vos" in
create_empty_file long_f_dot_vos in
let dump_empty_vok () =
let long_f_dot_vok = (safe_chop_extension long_f_dot_out) ^ ".vok" in
create_empty_file long_f_dot_vok in
match mode with
| BuildVo | BuildVok ->
let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
Stm.new_doc
Stm.{ doc_type = VoDoc long_f_dot_out; injections; } in
let state = { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } in
let state = Load.load_init_vernaculars opts ~state in
let ldir = Stm.get_ldir ~doc:state.doc in
Aux_file.(start_aux_file
~aux_file:(aux_file_name_for long_f_dot_out)
~v_file:long_f_dot_in);
Dumpglob.push_output copts.glob_out;
Dumpglob.start_dump_glob ~vfile:long_f_dot_in ~vofile:long_f_dot_out;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
let wall_clock1 = Unix.gettimeofday () in
let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in
let source = source ldir long_f_dot_in in
let state = Vernac.load_vernac ~echo ~check ~state ~source long_f_dot_in in
let fullstate = Stm.finish ~doc:state.doc in
ensure_no_pending_proofs ~filename:long_f_dot_in fullstate;
let () = Stm.join ~doc:state.doc in
let wall_clock2 = Unix.gettimeofday () in
if mode = BuildVo
then Library.save_library_to ~output_native_objects Library.ProofsTodoNone ldir long_f_dot_out;
Aux_file.record_in_aux_at "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
if mode = BuildVo then
dump_empty_vos();
dump_empty_vok();
Dumpglob.end_dump_glob ()
| BuildVos ->
let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
Stm.new_doc
Stm.{ doc_type = VosDoc long_f_dot_out; injections;
} in
let state = { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } in
let state = Load.load_init_vernaculars opts ~state in
let ldir = Stm.get_ldir ~doc:state.doc in
let source = source ldir long_f_dot_in in
let state = Vernac.load_vernac ~echo ~check:false ~source ~state long_f_dot_in in
let state = Stm.finish ~doc:state.doc in
ensure_no_pending_proofs state ~filename:long_f_dot_in;
let () = Stm.snapshot_vos ~doc ~output_native_objects ldir long_f_dot_out in
Stm.reset_task_queue ();
()
let compile opts stm_opts copts injections ~echo ~f_in ~f_out =
ignore(CoqworkmgrApi.get 1);
compile opts stm_opts injections copts ~echo ~f_in ~f_out;
CoqworkmgrApi.giveback 1
let compile_file opts stm_opts copts injections (f_in, echo) =
let f_out = copts.compilation_output_name in
if !Flags.beautify then
Flags.with_option Flags.beautify_file
(fun f_in -> compile opts stm_opts copts injections ~echo ~f_in ~f_out) f_in
else
compile opts stm_opts copts injections ~echo ~f_in ~f_out
let compile_file opts stm_opts copts injections =
Option.iter (compile_file opts stm_opts copts injections) copts.compile_file