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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
let check_vi (ts,f) =
Dumpglob.noglob ();
let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
module Worker = Spawn.Sync(struct
let add_timeout ~sec f =
ignore(Thread.create (fun () ->
while true do
Unix.sleep sec;
if not (f ()) then Thread.exit ()
done)
())
end)
module IntOT = struct
type t = int
let compare = compare
end
module Pool = Map.Make(IntOT)
let schedule_vi_checking j fs =
if j < 1 then Errors.error "The number of workers must be bigger than 0";
let jobs = ref [] in
List.iter (fun f ->
let f =
if Filename.check_suffix f ".vi" then Filename.chop_extension f
else f in
let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
if infos <> [] then jobs := (f, eta, infos) :: !jobs)
fs;
let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
jobs := List.sort cmp_job !jobs;
let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in
let pool : Worker.process Pool.t ref = ref Pool.empty in
let rec filter_argv b = function
| [] -> []
| "-schedule-vi-checking" :: rest -> filter_argv true rest
| s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
| _ :: rest when b -> filter_argv b rest
| s :: rest -> s :: filter_argv b rest in
let pack = function
| [] -> []
| ((f,_),_,_) :: _ as l ->
let rec aux last acc = function
| [] -> [last,acc]
| ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
| ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
aux f [] l in
let prog = Sys.argv.(0) in
let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
let make_job () =
let cur = ref 0.0 in
let what = ref [] in
let j_left = j - Pool.cardinal !pool in
let take_next_file () =
let f, t, tasks = List.hd !jobs in
jobs := List.tl !jobs;
cur := !cur +. t;
what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in
if List.length !jobs >= j_left then take_next_file ()
else while !jobs <> [] &&
!cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do
let f, t, tasks = List.hd !jobs in
jobs := List.tl !jobs;
let n, tt, id = List.hd tasks in
if List.length tasks > 1 then
jobs := (f, t -. tt, List.tl tasks) :: !jobs;
cur := !cur +. tt;
what := ((f,id),n,tt) :: !what;
done;
if !what = [] then take_next_file ();
eta := !eta -. !cur;
let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
List.flatten
(List.map (fun (f, tl) ->
"-check-vi-tasks" ::
String.concat "," (List.map string_of_int tl) :: [f])
(pack (List.sort cmp_job !what))) in
let rc = ref 0 in
while !jobs <> [] || Pool.cardinal !pool > 0 do
while Pool.cardinal !pool < j && !jobs <> [] do
let args = Array.of_list (stdargs @ make_job ()) in
let proc, _, _ = Worker.spawn prog args in
pool := Pool.add (Worker.unixpid proc) proc !pool;
done;
let pid, ret = Unix.wait () in
if ret <> Unix.WEXITED 0 then rc := 1;
pool := Pool.remove pid !pool;
done;
exit !rc
|
