aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/coqworkmgrApi.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-10 04:27:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-11 12:43:25 +0100
commit50159f9c1748ccf1d66341d171081a998d116d2f (patch)
treeef58c58b10abcb45142b56d261bc15f034b2731e /stm/coqworkmgrApi.ml
parenta758aac39aa330911f5f589ab3cae1bebed1e9ce (diff)
[flags] [stm] Reorganize flags.
We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
Diffstat (limited to 'stm/coqworkmgrApi.ml')
-rw-r--r--stm/coqworkmgrApi.ml25
1 files changed, 14 insertions, 11 deletions
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index 6d6a198c5..14fd97a6d 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -8,8 +8,15 @@
let debug = false
+type priority = Low | High
+let string_of_priority = function Low -> "low" | High -> "high"
+let priority_of_string = function
+ | "low" -> Low
+ | "high" -> High
+ | _ -> raise (Invalid_argument "priority_of_string")
+
type request =
- | Hello of Flags.priority
+ | Hello of priority
| Get of int
| TryGet of int
| GiveBack of int
@@ -36,8 +43,8 @@ let positive_int_of_string n =
let parse_request s =
if debug then Printf.eprintf "parsing '%s'\n" s;
match Str.split (Str.regexp " ") (strip_r s) with
- | [ "HELLO"; "LOW" ] -> Hello Flags.Low
- | [ "HELLO"; "HIGH" ] -> Hello Flags.High
+ | [ "HELLO"; "LOW" ] -> Hello Low
+ | [ "HELLO"; "HIGH" ] -> Hello High
| [ "GET"; n ] -> Get (positive_int_of_string n)
| [ "TRYGET"; n ] -> TryGet (positive_int_of_string n)
| [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n)
@@ -57,8 +64,8 @@ let parse_response s =
| _ -> raise ParseError
let print_request = function
- | Hello Flags.Low -> "HELLO LOW\n"
- | Hello Flags.High -> "HELLO HIGH\n"
+ | Hello Low -> "HELLO LOW\n"
+ | Hello High -> "HELLO HIGH\n"
| Get n -> Printf.sprintf "GET %d\n" n
| TryGet n -> Printf.sprintf "TRYGET %d\n" n
| GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n
@@ -106,8 +113,7 @@ let with_manager f g =
let get n =
with_manager
- (fun () ->
- min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))
+ (fun () -> n)
(fun cin cout ->
output_string cout (print_request (Get n));
flush cout;
@@ -118,10 +124,7 @@ let get n =
let tryget n =
with_manager
- (fun () ->
- Some
- (min n
- (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)))
+ (fun () -> Some n)
(fun cin cout ->
output_string cout (print_request (TryGet n));
flush cout;