aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/future.ml1
-rw-r--r--lib/future.mli1
-rw-r--r--lib/remoteCounter.ml3
-rw-r--r--lib/remoteCounter.mli3
-rw-r--r--lib/stateid.ml9
-rw-r--r--lib/stateid.mli10
-rw-r--r--library/library.ml46
-rw-r--r--library/library.mli3
-rw-r--r--stm/asyncTaskQueue.ml12
-rw-r--r--stm/asyncTaskQueue.mli7
-rw-r--r--stm/stm.ml92
-rw-r--r--stm/stm.mli19
-rw-r--r--stm/tQueue.ml9
-rw-r--r--stm/tQueue.mli3
-rw-r--r--toplevel/vernac.ml4
15 files changed, 137 insertions, 85 deletions
diff --git a/lib/future.ml b/lib/future.ml
index 6ebbd4b1d..4437cec84 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -41,6 +41,7 @@ module UUID = struct
end
module UUIDMap = Map.Make(UUID)
+module UUIDSet = Set.Make(UUID)
type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
diff --git a/lib/future.mli b/lib/future.mli
index 18b014132..a03823af8 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -61,6 +61,7 @@ module UUID : sig
end
module UUIDMap : Map.S with type key = UUID.t
+module UUIDSet : Set.S with type elt = UUID.t
exception NotReady
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 72887b21a..c0217b22e 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -37,6 +37,9 @@ let new_counter ~name a ~incr ~build =
let backup () = !counters
+let snapshot () =
+ List.map (fun (n,v) -> n, Obj.repr (ref (ref !!(Obj.obj v)))) !counters
+
let restore l =
List.iter (fun (name, data) ->
assert(List.mem_assoc name !counters);
diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli
index 5a47ba663..18e6b6b59 100644
--- a/lib/remoteCounter.mli
+++ b/lib/remoteCounter.mli
@@ -20,4 +20,7 @@ val new_counter : name:string ->
type remote_counters_status
val backup : unit -> remote_counters_status
+(* like backup but makes a copy so that further increment does not alter
+ * the snapshot *)
+val snapshot : unit -> remote_counters_status
val restore : remote_counters_status -> unit
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 09cc2b7e8..59cf206e2 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -39,3 +39,12 @@ let compare = Int.compare
module Set = Set.Make(struct type t = int let compare = compare end)
+type ('a,'b) request = {
+ exn_info : t * t;
+ stop : t;
+ document : 'b;
+ loc : Loc.t;
+ uuid : 'a;
+ name : string
+}
+
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 11fac7a92..341544a67 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -33,3 +33,13 @@ val of_xml : xml -> t
* The initial_state_id is assumed to be safe. *)
val add : exn -> ?valid:t -> t -> exn
val get : exn -> (t * t) option
+
+type ('a,'b) request = {
+ exn_info : t * t;
+ stop : t;
+ document : 'b;
+ loc : Loc.t;
+ uuid : 'a;
+ name : string
+}
+
diff --git a/library/library.ml b/library/library.ml
index 7f5ca5af6..ceadb3ace 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -670,19 +670,35 @@ let error_recursively_dependent_library dir =
writing the content and computing the checksum... *)
let save_library_to ?todo dir f otab =
- let f, todo, utab, dtab =
- match todo with
+ let f, except = match todo with
| None ->
assert(!Flags.compilation_mode = Flags.BuildVo);
- f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None)
- | Some d ->
- assert(!Flags.compilation_mode = Flags.BuildVi);
- f ^ "i", (fun x -> Some (d x)),
- (fun x -> Some (x,Univ.ContextSet.empty,false)), (fun x -> Some x) in
- let cenv, seg, ast = Declaremods.end_library dir in
+ f ^ "o", Future.UUIDSet.empty
+ | Some (l,_) ->
+ f ^ "i",
+ List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e)
+ Future.UUIDSet.empty l in
+ let cenv, seg, ast = Declaremods.end_library ~except dir in
let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
- assert(!Flags.compilation_mode = Flags.BuildVi ||
- Array.for_all Future.is_val opaque_table);
+ let tasks, utab, dtab =
+ match todo with
+ | None -> None, None, None
+ | Some (tasks, rcbackup) ->
+ let tasks =
+ List.map Stateid.(fun r ->
+ { r with uuid = Future.UUIDMap.find r.uuid f2t_map }) tasks in
+ Some (tasks,rcbackup),
+ Some (univ_table,Univ.ContextSet.empty,false),
+ Some disch_table in
+ let except =
+ Future.UUIDSet.fold (fun uuid acc ->
+ Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc)
+ except Int.Set.empty in
+ let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
+ Array.iteri (fun i x ->
+ if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
+ Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
+ opaque_table;
let md = {
md_name = dir;
md_compiled = cenv;
@@ -695,11 +711,11 @@ let save_library_to ?todo dir f otab =
let (f',ch) = raw_extern_library f in
try
(* Writing vo payload *)
- System.marshal_out_segment f' ch (md : seg_lib);
- System.marshal_out_segment f' ch (utab univ_table : seg_univ option);
- System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option);
- System.marshal_out_segment f' ch (todo f2t_map : 'tasks option);
- System.marshal_out_segment f' ch (opaque_table : seg_proofs);
+ System.marshal_out_segment f' ch (md : seg_lib);
+ System.marshal_out_segment f' ch (utab : seg_univ option);
+ System.marshal_out_segment f' ch (dtab : seg_discharge option);
+ System.marshal_out_segment f' ch (tasks : 'tasks option);
+ System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
if not !Flags.no_native_compiler then
diff --git a/library/library.mli b/library/library.mli
index c92b9d623..9e914d9bb 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -43,7 +43,8 @@ val import_module : bool -> qualid located -> unit
val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:(int Future.UUIDMap.t -> 'tasks) ->
+val save_library_to :
+ ?todo:((Future.UUID.t,'document) Stateid.request list * 'counters) ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 74e83a39f..22e7c0243 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -304,13 +304,19 @@ module Make(T : Task) = struct
flush_all (); exit 1
done
- let dump () =
- assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *)
- List.map fst (TQueue.dump queue)
+ let clear () =
+ assert(WorkersPool.is_empty ()); (* We allow that only if no slaves *)
+ TQueue.clear queue
+
+ let snapshot () =
+ List.map fst
+ (TQueue.wait_until_n_are_waiting_then_snapshot
+ (WorkersPool.n_workers ()) queue)
let init n =
WorkersPool.init n manage_slave
(fun n -> Printf.sprintf "%s:%d" T.name n)
+
let destroy () =
WorkersPool.destroy ();
TQueue.destroy queue
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index ddbb28457..cd91ba129 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -61,6 +61,11 @@ module Make(T : Task) : sig
val set_order : (T.task -> T.task -> int) -> unit
- val dump : unit -> T.task list
+ (* Take a snapshot (non destructive but waits until all workers are
+ * enqueued) *)
+ val snapshot : unit -> T.task list
+
+ (* Clears the queue, only if the worker prool is empty *)
+ val clear : unit -> unit
end
diff --git a/stm/stm.ml b/stm/stm.ml
index 5349b85a8..026866616 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -701,14 +701,6 @@ let record_pb_time proof_name loc time =
hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
end
-type 'a a_request = {
- r_exn_info : Stateid.t * Stateid.t;
- r_stop : Stateid.t;
- r_document : VCS.vcs;
- r_loc : Loc.t;
- r_uuid : 'a;
- r_name : string }
-
exception RemoteException of std_ppcmds
let _ = Errors.register_handler (function
| RemoteException ppcmd -> ppcmd
@@ -730,7 +722,7 @@ module Task = struct
t_uuid : Future.UUID.t;
t_name : string }
- type request = Future.UUID.t a_request
+ type request = (Future.UUID.t,VCS.vcs) Stateid.request
type error = {
e_error_at : Stateid.t;
@@ -746,17 +738,17 @@ module Task = struct
let extra_env () = !async_proofs_workers_extra_env
let name_of_task t = t.t_name
- let name_of_request r = r.r_name
+ let name_of_request r = r.Stateid.name
let request_of_task age { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name } =
assert(age = `Fresh);
try Some {
- r_exn_info = t_exn_info;
- r_stop = t_stop;
- r_document = VCS.slice ~start:t_stop ~stop:t_start;
- r_loc = t_loc;
- r_uuid = t_uuid;
- r_name = t_name }
+ Stateid.exn_info = t_exn_info;
+ stop = t_stop;
+ document = VCS.slice ~start:t_stop ~stop:t_start;
+ loc = t_loc;
+ uuid = t_uuid;
+ name = t_name }
with VCS.Expired -> None
let use_response { t_assign; t_loc; t_name } = function
@@ -795,13 +787,13 @@ module Task = struct
Proof_global.return_proof ()
let build_proof_here (id,valid) loc eop =
Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop)
- let perform { r_exn_info; r_stop = eop; r_document = vcs; r_loc } =
+ let perform { Stateid.exn_info; stop = eop; document = vcs; loc } =
try
VCS.restore vcs;
VCS.print ();
let rc, time =
let wall_clock = Unix.gettimeofday () in
- let l = Future.force (build_proof_here r_exn_info r_loc eop) in
+ let l = Future.force (build_proof_here exn_info loc eop) in
l, Unix.gettimeofday () -. wall_clock in
VCS.print ();
RespBuiltProof(rc,time)
@@ -877,18 +869,19 @@ module Slaves : sig
val slave_main_loop : (unit -> unit) -> unit
val slave_init_stdout : unit -> unit
- type tasks
- val dump_final : int Future.UUIDMap.t -> tasks
- val dump_snapshot : int Future.UUIDMap.t -> tasks
- val check_task : string -> tasks -> int -> bool
- val info_tasks : tasks -> (string * float * int) list
+ type 'a tasks = ('a,VCS.vcs) Stateid.request list
+ val dump_snapshot : unit -> Future.UUID.t tasks
+ val check_task : string -> int tasks -> int -> bool
+ val info_tasks : 'a tasks -> (string * float * int) list
val finish_task :
string ->
Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
- tasks -> int -> Library.seg_univ
+ int tasks -> int -> Library.seg_univ
val cancel_worker : string -> unit
+ val reset_task_queue : unit -> unit
+
val set_perspective : Stateid.t list -> unit
end = struct
@@ -896,19 +889,19 @@ end = struct
module TaskQueue = AsyncTaskQueue.Make(Task)
let check_task_aux extra name l i =
- let { r_stop; r_document; r_loc; r_name } = List.nth l i in
+ let { Stateid.stop; document; loc; name = r_name } = List.nth l i in
Pp.msg_info(
str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
- VCS.restore r_document;
+ VCS.restore document;
try
- !Task.reach_known_state ~cache:`No r_stop;
+ !Task.reach_known_state ~cache:`No stop;
(* The original terminator, a hook, has not been saved in the .vi*)
Proof_global.set_terminator
(Lemmas.standard_proof_terminator []
(Lemmas.mk_hook (fun _ _ -> ())));
let proof = Proof_global.close_proof (fun x -> x) in
- vernac_interp r_stop ~proof
- { verbose = false; loc = r_loc;
+ vernac_interp stop ~proof
+ { verbose = false; loc;
expr = (VernacEndProof (Proved (true,None))) };
Some proof
with e ->
@@ -938,7 +931,7 @@ end = struct
str (Printexc.to_string e))); None
let finish_task name (u,cst,_) d p l i =
- let bucket = (List.nth l i).r_uuid in
+ let bucket = (List.nth l i).Stateid.uuid in
match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
| None -> exit 1
| Some (po,pt) ->
@@ -972,14 +965,14 @@ end = struct
| None -> false
let info_tasks l =
- CList.map_i (fun i { r_loc; r_name } ->
+ CList.map_i (fun i { Stateid.loc; name } ->
let time1 =
- try float_of_string (Aux_file.get !hints r_loc "proof_build_time")
+ try float_of_string (Aux_file.get !hints loc "proof_build_time")
with Not_found -> 0.0 in
let time2 =
- try float_of_string (Aux_file.get !hints r_loc "proof_check_time")
+ try float_of_string (Aux_file.get !hints loc "proof_check_time")
with Not_found -> 0.0 in
- r_name, max (time1 +. time2) 0.0001,i) 0 l
+ name, max (time1 +. time2) 0.0001,i) 0 l
let set_perspective idl =
let open Stateid in
@@ -1024,17 +1017,13 @@ end = struct
let cancel_worker = TaskQueue.cancel_worker
(* For external users this name is nicer than request *)
- type tasks = int a_request list
- let dump f2t_map =
- let tasks = TaskQueue.dump () in
- prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
- List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
- (CList.map_filter (Task.request_of_task `Fresh) tasks)
- let dump_snapshot f2t_map =
+ type 'a tasks = ('a,VCS.vcs) Stateid.request list
+ let dump_snapshot () =
let tasks = TaskQueue.snapshot () in
prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
- List.map (function r -> { r with r_uuid = Future.UUIDMap.find r.r_uuid f2t_map })
- (CList.map_filter (Task.request_of_task `Fresh) tasks)
+ CList.map_filter (Task.request_of_task `Fresh) tasks
+
+ let reset_task_queue () = TaskQueue.clear ()
end
@@ -1236,7 +1225,8 @@ let collect_proof keep cur hd brkind id =
else `Sync (name,proof_using_ast last,`Policy)
| `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.BuildVi ||
+ !Flags.async_proofs_always_delegate) ->
(try
let name = name ids in
let hint, time = get_hint_ctx loc, get_hint_bp_time name in
@@ -1602,8 +1592,9 @@ let join () =
VCS.print ();
VCS.print ()
-type tasks = Slaves.tasks * RemoteCounter.remote_counters_status
-let dump x = Slaves.dump x, RemoteCounter.backup ()
+let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
+type document = VCS.vcs
+type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
let check_task name (tasks,rcbackup) i =
RemoteCounter.restore rcbackup;
let vcs = VCS.backup () in
@@ -1683,6 +1674,15 @@ let handle_failure e vcs tty =
VCS.print ();
raise e
+let snapshot_vi ldir long_f_dot_v =
+ finish ();
+ if List.length (VCS.branches ()) > 1 then
+ Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs");
+ Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+ (Global.opaque_tables ())
+
+let reset_task_queue = Slaves.reset_task_queue
+
let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
let warn_if_pos a b =
if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
diff --git a/stm/stm.mli b/stm/stm.mli
index d77c19cfb..c4664a67c 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -46,16 +46,25 @@ val stop_worker : string -> unit
(* Joins the entire document. Implies finish, but also checks proofs *)
val join : unit -> unit
-(* To save to disk an incomplete document *)
-type tasks
-val dump_final : int Future.UUIDMap.t -> tasks
-val dump_snapshot : int Future.UUIDMap.t -> tasks
+(* Saves on the dist a .vi 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
+
+(* Empties the task queue, can be used only if the worker pool is empty (E.g.
+ * after having built a .vi in batch mode *)
+val reset_task_queue : unit -> unit
+
+(* A .vi contains tasks to be completed *)
+type tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
val finish_tasks : string ->
Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
- tasks -> Library.seg_univ * Library.seg_proofs
+ tasks -> Library.seg_univ * Library.seg_proofs
(* Id of the tip of the current branch *)
val get_current_state : unit -> Stateid.t
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index fe9cf015a..04e4e81f9 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -103,15 +103,6 @@ let wait_until_n_are_waiting_and_queue_empty j tq =
done;
Mutex.unlock tq.lock
-let dump { queue; lock } =
- let l = ref [] in
- Mutex.lock lock;
- while not (PriorityQueue.is_empty queue) do
- l := PriorityQueue.pop queue :: !l
- done;
- Mutex.unlock lock;
- List.rev !l
-
let wait_until_n_are_waiting_then_snapshot j tq =
let l = ref [] in
Mutex.lock tq.lock;
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index abb14f969..230ce032a 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -15,9 +15,6 @@ val push : 'a t -> 'a -> unit
val set_order : 'a t -> ('a -> 'a -> int) -> unit
val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
-(* also empties the queue *)
-val dump : 'a t -> 'a list
-
(* Non destructive *)
val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index dcce58199..b56b515dc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -333,8 +333,8 @@ let compile verbosely f =
let _ = load_vernac verbosely long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
- Library.save_library_to ~todo:Stm.dump_final ldir long_f_dot_v
- (Global.opaque_tables ())
+ Stm.snapshot_vi ldir long_f_dot_v;
+ Stm.reset_task_queue ()
| Vi2Vo ->
let open Filename in
let open Library in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 02:23:09 +0000