From e7ffa1bfa25300a25c1e81583b77d2d7587bbb5d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 May 2019 14:27:36 +0200 Subject: Do not substitute opaque constants when discharging. Instead we do that on a by-need basis by reusing the section info already stored in the opaque proof. --- stm/stm.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b2bfa552b4..8efb606ddc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1732,7 +1732,6 @@ end = struct (* {{{ *) | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false | `OK (po,_) -> - let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in @@ -1744,12 +1743,11 @@ end = struct (* {{{ *) the call to [check_task_aux] above. *) let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in let uc = Univ.hcons_universe_context_set uc in + let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in (* We only manipulate monomorphic terms here. *) - let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in - let pr = discharge pr in + let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- Some pr; + p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr); Univ.ContextSet.union cst uc, false let check_task name l i = -- cgit v1.2.3 From 0f54a91eac98baf076d8be8f52bccdb1de17ea46 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jun 2019 10:19:02 +0200 Subject: Slightly tweak the representation of dischargeable opaque proofs. This will allow an easier removal of the discharge segment in a later commit. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 8efb606ddc..ad18245dec 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1747,7 +1747,7 @@ end = struct (* {{{ *) (* We only manipulate monomorphic terms here. *) let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr); + p.(bucket) <- d.(bucket), Univ.AUContext.size ctx, Some pr; Univ.ContextSet.union cst uc, false let check_task name l i = -- cgit v1.2.3 From 1cdfb1f9270e399a784b346c3f8d6abbc4477552 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jun 2019 10:35:14 +0200 Subject: Remove the discharge segment from vo files. Since the introduction of delayed section substitution, the opaque table was already containing the same information. --- stm/stm.ml | 13 ++++++++----- stm/stm.mli | 2 +- stm/vio_checking.ml | 4 ++-- 3 files changed, 11 insertions(+), 8 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index ad18245dec..1a525f8c80 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1637,7 +1637,7 @@ and Slaves : sig val info_tasks : 'a tasks -> (string * float * int) list val finish_task : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + Library.seg_univ -> Library.seg_proofs -> int tasks -> int -> Library.seg_univ val cancel_worker : WorkerPool.worker_id -> unit @@ -1722,7 +1722,7 @@ end = struct (* {{{ *) str (Printexc.to_string e))); if drop then `ERROR_ADMITTED else `ERROR - let finish_task name (cst,_) d p l i = + let finish_task name (cst,_) p l i = let { Stateid.uuid = bucket }, drop = List.nth l i in let bucket_name = if bucket < 0 then (assert drop; ", no bucket") @@ -1747,7 +1747,10 @@ end = struct (* {{{ *) (* We only manipulate monomorphic terms here. *) let () = assert (Univ.AUContext.is_empty ctx) in let pr = Constr.hcons pr in - p.(bucket) <- d.(bucket), Univ.AUContext.size ctx, Some pr; + let (ci, univs, dummy) = p.(bucket) in + let () = assert (Option.is_empty dummy) in + let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in + p.(bucket) <- ci, univs, Some pr; Univ.ContextSet.union cst uc, false let check_task name l i = @@ -2743,11 +2746,11 @@ let check_task name (tasks,rcbackup) i = with e when CErrors.noncritical e -> VCS.restore vcs; false let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u d p (t,rcbackup as tasks) = +let finish_tasks name u p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u d p t) i in + let u = State.purify (Slaves.finish_task name u p t) i in VCS.restore vcs; u in try diff --git a/stm/stm.mli b/stm/stm.mli index 5e1e9bf5ad..86e2566539 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -167,7 +167,7 @@ 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 -> + Library.seg_univ -> Library.seg_proofs -> tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 0f78e0acf6..cf0c8934b0 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -12,7 +12,7 @@ open Util let check_vio (ts,f_in) = Dumpglob.noglob (); - let _, _, _, _, tasks, _ = Library.load_library_todo f_in 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 @@ -29,7 +29,7 @@ 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 + 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 -- cgit v1.2.3