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
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util let check_vio (ts,f_in) = let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts module Worker = Spawn.Sync () module IntOT = struct type t = int let compare = compare end module Pool = Map.Make(IntOT) let schedule_vio_checking j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun long_f_dot_vio -> let _,_,_, tasks, _ = Library.load_library_todo long_f_dot_vio in Stm.set_compilation_hints long_f_dot_vio; 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 := (long_f_dot_vio, 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-vio-checking" :: rest -> filter_argv true rest | s :: rest when String.length s > 0 && 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-vio-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; Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc let schedule_vio_compilation j fs = if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); let jobs = ref [] in List.iter (fun long_f_dot_vio -> let aux = Aux_file.load_aux_file_for long_f_dot_vio in let eta = try float_of_string (Aux_file.get aux "vo_compile_time") with Not_found -> 0.0 in jobs := (long_f_dot_vio, eta) :: !jobs) fs; let cmp_job (_,t1) (_,t2) = compare t2 t1 in jobs := List.sort cmp_job !jobs; let pool : Worker.process Pool.t ref = ref Pool.empty in let rec filter_argv b = function | [] -> [] | "-schedule-vio2vo" :: rest -> filter_argv true rest | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) | _ :: rest when b -> filter_argv b rest | s :: rest -> s :: filter_argv b rest in let prog = Sys.argv.(0) in let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in let all_jobs = !jobs in let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; [ "-vio2vo"; f ] 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; Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; if !rc = 0 then begin (* set the access and last modification time of all files to the same t * not to confuse make into thinking that some of them are outdated *) let t = Unix.gettimeofday () in List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc