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
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"
| BuildVio -> ".v", ".vio"
| Vio2Vo -> ".vio", ".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 ()
| BuildVio | BuildVos ->
let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
Stm.new_doc
Stm.{ doc_type = VioDoc 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 create_vos = (mode = BuildVos) in
let () = Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out in
Stm.reset_task_queue ();
if mode = BuildVio then dump_empty_vos();
()
| Vio2Vo ->
Flags.async_proofs_worker_id := "Vio2Vo";
let sum, lib, univs, tasks, proofs =
Library.load_library_todo long_f_dot_in in
let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in
Library.save_library_raw long_f_dot_out sum lib univs proofs;
dump_empty_vos();
create_empty_file (long_f_dot_out ^ "k")
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