From 341909bbc5c1c59e81dfad2f2532602e2561ec36 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Jan 2015 18:09:26 +0100 Subject: rename: vi -> vio --- stm/stm.ml | 14 ++--- stm/stm.mli | 8 +-- stm/stm.mllib | 2 +- stm/vi_checking.ml | 144 --------------------------------------------------- stm/vi_checking.mli | 13 ----- stm/vio_checking.ml | 144 +++++++++++++++++++++++++++++++++++++++++++++++++++ stm/vio_checking.mli | 13 +++++ 7 files changed, 169 insertions(+), 169 deletions(-) delete mode 100644 stm/vi_checking.ml delete mode 100644 stm/vi_checking.mli create mode 100644 stm/vio_checking.ml create mode 100644 stm/vio_checking.mli (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 1dff4ae948..4afdb06a18 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1145,7 +1145,7 @@ end = struct (* {{{ *) VCS.restore document; try Reach.known_state ~cache:`No stop; - (* The original terminator, a hook, has not been saved in the .vi*) + (* The original terminator, a hook, has not been saved in the .vio*) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] (Lemmas.mk_hook (fun _ _ -> ()))); @@ -1245,7 +1245,7 @@ end = struct (* {{{ *) let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then - if !Flags.compilation_mode = Flags.BuildVi then begin + if !Flags.compilation_mode = Flags.BuildVio then begin let f,assign = Future.create_delegate ~blocking:true (State.exn_on id ~valid) in let t_uuid = Future.uuid f in @@ -1536,11 +1536,11 @@ let async_policy () = if interactive () = `Yes then (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy) else - (!compilation_mode = Flags.BuildVi || !async_proofs_mode <> Flags.APoff) + (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff) let delegate name = let time = get_hint_bp_time name in - time >= 1.0 || !Flags.compilation_mode = Flags.BuildVi + time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio let collect_proof keep cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); @@ -1579,7 +1579,7 @@ let collect_proof keep cur hd brkind id = `ASync (parent last,proof_using_ast last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached (parent last)) && - !Flags.compilation_mode = Flags.BuildVi -> + !Flags.compilation_mode = Flags.BuildVio -> assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); (try let name, hint = name ids, get_hint_ctx loc in @@ -1903,10 +1903,10 @@ let handle_failure (e, info) vcs tty = VCS.print (); iraise (e, info) -let snapshot_vi ldir long_f_dot_v = +let snapshot_vio ldir long_f_dot_v = finish (); if List.length (VCS.branches ()) > 1 then - Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs"); + Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v (Global.opaque_tables ()) diff --git a/stm/stm.mli b/stm/stm.mli index 715997aee0..2cbd54dd5a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -49,18 +49,18 @@ val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) val join : unit -> unit -(* Saves on the dist a .vi corresponding to the current status: +(* Saves on the dist a .vio corresponding to the current status: - if the worker prool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failuere) *) -val snapshot_vi : DirPath.t -> string -> unit +val snapshot_vio : DirPath.t -> string -> unit (* Empties the task queue, can be used only if the worker pool is empty (E.g. - * after having built a .vi in batch mode *) + * after having built a .vio in batch mode *) val reset_task_queue : unit -> unit -(* A .vi contains tasks to be completed *) +(* A .vio contains tasks to be completed *) type tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list diff --git a/stm/stm.mllib b/stm/stm.mllib index 2b5ff8c04a..92b3a869a9 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -9,4 +9,4 @@ CoqworkmgrApi AsyncTaskQueue Texmacspp Stm -Vi_checking +Vio_checking diff --git a/stm/vi_checking.ml b/stm/vi_checking.ml deleted file mode 100644 index 925a2a89e3..0000000000 --- a/stm/vi_checking.ml +++ /dev/null @@ -1,144 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Stm.check_task f tasks ids && acc) true ts - -module Worker = Spawn.Sync(struct 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 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 - -let schedule_vi_compilation 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 paths = Loadpath.get_paths () in - let _, long_f_dot_v = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in - let aux = Aux_file.load_aux_file_for long_f_dot_v in - let eta = - try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") - with Not_found -> 0.0 in - jobs := (f, 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-vi2vo" :: 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 prog = Sys.argv.(0) in - let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in - let make_job () = - let f, t = List.hd !jobs in - jobs := List.tl !jobs; - [ "-vi2vo"; 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; - pool := Pool.remove pid !pool; - done; - exit !rc - - diff --git a/stm/vi_checking.mli b/stm/vi_checking.mli deleted file mode 100644 index 65414eda41..0000000000 --- a/stm/vi_checking.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool -val schedule_vi_checking : int -> string list -> unit - -val schedule_vi_compilation : int -> string list -> unit diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml new file mode 100644 index 0000000000..3922af6e1c --- /dev/null +++ b/stm/vio_checking.ml @@ -0,0 +1,144 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Stm.check_task f tasks ids && acc) true ts + +module Worker = Spawn.Sync(struct end) + +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 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 ".vio" then Filename.chop_extension f + else f in + let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in + Stm.set_compilation_hints 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-vio-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-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; + pool := Pool.remove pid !pool; + done; + exit !rc + +let schedule_vio_compilation 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 ".vio" then Filename.chop_extension f + else f in + let paths = Loadpath.get_paths () in + let _, long_f_dot_v = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let aux = Aux_file.load_aux_file_for long_f_dot_v in + let eta = + try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") + with Not_found -> 0.0 in + jobs := (f, 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 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 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; + pool := Pool.remove pid !pool; + done; + exit !rc + + diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli new file mode 100644 index 0000000000..fb1a0beca4 --- /dev/null +++ b/stm/vio_checking.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool +val schedule_vio_checking : int -> string list -> unit + +val schedule_vio_compilation : int -> string list -> unit -- cgit v1.2.3