diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 14 | ||||
| -rw-r--r-- | stm/stm.mli | 8 | ||||
| -rw-r--r-- | stm/stm.mllib | 2 | ||||
| -rw-r--r-- | stm/vio_checking.ml (renamed from stm/vi_checking.ml) | 18 | ||||
| -rw-r--r-- | stm/vio_checking.mli (renamed from stm/vi_checking.mli) | 8 |
5 files changed, 25 insertions, 25 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 1dff4ae94..4afdb06a1 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 715997aee..2cbd54dd5 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 2b5ff8c04..92b3a869a 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/vio_checking.ml index 925a2a89e..3922af6e1 100644 --- a/stm/vi_checking.ml +++ b/stm/vio_checking.ml @@ -8,7 +8,7 @@ open Util -let check_vi (ts,f) = +let check_vio (ts,f) = Dumpglob.noglob (); let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in Stm.set_compilation_hints long_f_dot_v; @@ -23,12 +23,12 @@ end module Pool = Map.Make(IntOT) -let schedule_vi_checking j fs = +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 ".vi" then Filename.chop_extension 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; @@ -42,7 +42,7 @@ let schedule_vi_checking j fs = 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 + | "-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 @@ -81,7 +81,7 @@ let schedule_vi_checking j fs = let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in List.flatten (List.map (fun (f, tl) -> - "-check-vi-tasks" :: + "-check-vio-tasks" :: String.concat "," (List.map string_of_int tl) :: [f]) (pack (List.sort cmp_job !what))) in let rc = ref 0 in @@ -97,12 +97,12 @@ let schedule_vi_checking j fs = done; exit !rc -let schedule_vi_compilation j fs = +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 ".vi" then Filename.chop_extension 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 = @@ -118,7 +118,7 @@ let schedule_vi_compilation j fs = let pool : Worker.process Pool.t ref = ref Pool.empty in let rec filter_argv b = function | [] -> [] - | "-schedule-vi2vo" :: rest -> filter_argv true rest + | "-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 @@ -127,7 +127,7 @@ let schedule_vi_compilation j fs = let make_job () = let f, t = List.hd !jobs in jobs := List.tl !jobs; - [ "-vi2vo"; f ] in + [ "-vio2vo"; f ] in let rc = ref 0 in while !jobs <> [] || Pool.cardinal !pool > 0 do while Pool.cardinal !pool < j && !jobs <> [] do diff --git a/stm/vi_checking.mli b/stm/vio_checking.mli index 65414eda4..fb1a0beca 100644 --- a/stm/vi_checking.mli +++ b/stm/vio_checking.mli @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* [check_vi tasks file] checks the [tasks] stored in [file] *) -val check_vi : int list * string -> bool -val schedule_vi_checking : int -> string list -> unit +(* [check_vio tasks file] checks the [tasks] stored in [file] *) +val check_vio : int list * string -> bool +val schedule_vio_checking : int -> string list -> unit -val schedule_vi_compilation : int -> string list -> unit +val schedule_vio_compilation : int -> string list -> unit |