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 --- plugins/ltac/tacentries.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index bcd5b388a..0bf6e3d15 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -468,7 +468,9 @@ let register_ltac local tacl = let () = List.iter iter_rec recvars in List.map map rfun in - let defs = Future.transactify defs () in + (* STATE XXX: Review what is going on here. Why does this needs + protection? Why is not the STM level protection enough? Fishy *) + let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; -- cgit v1.2.3