From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 28 May 2017 00:35:57 +0200 Subject: [stm] Remove state-handling from Futures. We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s --- proofs/pfedit.ml | 2 +- proofs/proof_global.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'proofs') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 23f96b5a3..469e1a011 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,7 +156,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with - const_entry_body = Future.chain ~pure:true ce.const_entry_body + const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cd4d1dcf6..621178982 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -373,11 +373,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in - fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) + fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> Future.from_val (univctx, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> + Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, -- cgit v1.2.3