diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-28 00:35:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:19:11 +0200 |
| commit | 280be11cb4706e039cf4e9f68a5ae38b0aef9340 (patch) | |
| tree | e1e1a1a8465076e0fe6e95566f14d7ea0f960813 /library/states.mli | |
| parent | 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (diff) | |
[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
Diffstat (limited to 'library/states.mli')
| -rw-r--r-- | library/states.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/library/states.mli b/library/states.mli index 780a4e8dc..accd0e7ea 100644 --- a/library/states.mli +++ b/library/states.mli @@ -30,10 +30,3 @@ val replace_summary : state -> Summary.frozen -> state val with_state_protection : ('a -> 'b) -> 'a -> 'b -(** [with_state_protection_on_exception f x] applies [f] to [x] and restores the - state of the whole system as it was before applying [f] only if an - exception is raised. Unlike [with_state_protection] it also takes into - account the proof state *) - -val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b - |