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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
let fatal_error exn =
Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
exit exit_code
let set_worker_id opt s =
assert (s <> "master");
Flags.async_proofs_worker_id := s
let get_host_port opt s =
match String.split_on_char ':' s with
| [host; portr; portw] ->
Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
| ["stdfds"] -> Some Spawned.AnonPipe
| _ ->
Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
let get_error_resilience opt = function
| "on" | "all" | "yes" -> Stm.AsyncOpts.FAll
| "off" | "no" -> Stm.AsyncOpts.FNone
| s -> Stm.AsyncOpts.FOnly (String.split_on_char ',' s)
let get_priority opt s =
try CoqworkmgrApi.priority_of_string s
with Invalid_argument _ ->
Coqargs.error_wrong_arg ("Error: low/high expected after "^opt)
let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
| "no" | "off" -> APoff
| "yes" | "on" -> APon
| "lazy" -> APonLazy
| _ ->
Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt)
let get_cache opt = function
| "force" -> Some Stm.AsyncOpts.Force
| _ ->
Coqargs.error_wrong_arg ("Error: force expected after "^opt)
let spawn_args (opts:Coqargs.t) =
let output_dir = match opts.config.output_directory with
| None -> []
| Some dir -> ["-output-directory";dir]
in
let test_mode = if opts.config.test_mode then ["-test-mode"] else [] in
let native_output = ["-native-output-dir"; opts.config.native_output_dir] in
let native_include ni = ["-nI";ni] in
let native_includes = CList.concat_map native_include opts.config.native_include_dirs in
let ml_include i = ["-I"; i] in
let ml_includes = CList.concat_map ml_include opts.pre.ml_includes in
let boot = if opts.pre.boot then ["-boot"] else [] in
List.concat [
output_dir;
test_mode;
native_output;
native_includes;
ml_includes;
boot;
["-q"; "-noinit"]
]
let parse_args opts arglist : Stm.AsyncOpts.stm_opt * string list =
let init = Stm.AsyncOpts.default_opts ~spawn_args:(spawn_args opts) in
let args = ref arglist in
let = ref [] in
let rec parse oval = match !args with
| [] ->
(oval, List.rev !extras)
| opt :: rem ->
args := rem;
let next () = match !args with
| x::rem -> args := rem; x
| [] -> Coqargs.error_missing_arg opt
in
let noval = begin match opt with
|"-async-proofs" ->
{ oval with
Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
}
|"-async-proofs-j" ->
{ oval with
Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ()))
}
|"-async-proofs-cache" ->
{ oval with
Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
}
|"-async-proofs-tac-j" ->
let j = Coqargs.get_int ~opt (next ()) in
if j < 0 then begin
Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 0")
end;
{ oval with
Stm.AsyncOpts.async_proofs_n_tacworkers = j
}
|"-async-proofs-worker-priority" ->
{ oval with
Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
}
|"-async-proofs-private-flags" ->
{ oval with
Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
}
|"-async-proofs-tactic-error-resilience" ->
{ oval with
Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
}
|"-async-proofs-command-error-resilience" ->
{ oval with
Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ())
}
|"-async-proofs-delegation-threshold" ->
{ oval with
Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ())
}
|"-worker-id" -> set_worker_id opt (next ()); oval
|"-main-channel" ->
let ch = next () in
Spawned.main_channel := get_host_port opt ch;
{ oval with spawn_args = opt :: ch :: oval.spawn_args }
|"-control-channel" ->
let ch = next () in
Spawned.control_channel := get_host_port opt ch;
{ oval with spawn_args = opt :: ch :: oval.spawn_args }
|"-async-queries-always-delegate"
|"-async-proofs-always-delegate"
|"-async-proofs-never-reopen-branch" ->
{ oval with
Stm.AsyncOpts.async_proofs_never_reopen_branch = true;
spawn_args = opt :: oval.spawn_args;
}
|"-stm-debug" -> Stm.stm_debug := true; { oval with spawn_args = opt :: oval.spawn_args }
| s ->
extras := s :: !extras;
oval
end in
parse noval
in
try
parse init
with any -> fatal_error any
let usage = "\
\n -stm-debug STM debug mode (will trace every transaction)\
"