diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 20 | ||||
| -rw-r--r-- | toplevel/stm.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 14 insertions, 10 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 8c1c6b02b..9cb5e9511 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -641,7 +641,7 @@ module Slaves : sig val finish_task : string -> Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> - tasks -> int -> unit + tasks -> int -> Library.seg_univ val cancel_worker : int -> unit @@ -878,7 +878,7 @@ end = struct (* {{{ *) Pp.msg_error (str"unable to print error message: " ++ str (Printexc.to_string e))); None - let finish_task name u d p l i = + let finish_task name (u,cst,_) d p l i = let bucket = match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with @@ -898,9 +898,10 @@ end = struct (* {{{ *) let pr = Future.chain ~greedy:true ~pure:true pr discharge in let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in Future.sink pr; - Future.sink uc; + let extra = Future.join uc in u.(bucket) <- uc; - p.(bucket) <- pr + p.(bucket) <- pr; + u, Univ.union_constraints cst extra, false | _ -> assert false let check_task name l i = @@ -1611,12 +1612,15 @@ let check_task name (tasks,_) i = let info_tasks (tasks,_) = Slaves.info_tasks tasks let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; - let finish_task (_,_,i) = + let finish_task u (_,_,i) = let vcs = VCS.backup () in - Future.purify (Slaves.finish_task name u d p t) i; + let u = Future.purify (Slaves.finish_task name u d p t) i in Pp.pperr_flush (); - VCS.restore vcs in - try List.iter finish_task (info_tasks tasks) + VCS.restore vcs; + u in + try + let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in + (u,a,true), p with e -> Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e); exit 1 diff --git a/toplevel/stm.mli b/toplevel/stm.mli index c47bacf65..1eba274ab 100644 --- a/toplevel/stm.mli +++ b/toplevel/stm.mli @@ -50,7 +50,7 @@ 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 -> unit + 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/toplevel/vernac.ml b/toplevel/vernac.ml index 4ea9c2236..11cb726c7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -348,6 +348,6 @@ let compile verbosely f = let f = if check_suffix f ".vi" then chop_extension f else f in let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv); - Stm.finish_tasks lfdv univs disch proofs tasks; + let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv lib univs proofs |