| Age | Commit message (Collapse) | Author |
|---|
|
A computation that is an exception morally holds no value
hence can be replaced by an type-equivalent computation.
This mechanism is used to edit broken proofs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16808 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The Stm commit switched from an home made handling of failures to
a with_state_protection. This was wrong, since in case of success
the global state has to be left altered.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Processing the proof in a slave process may fail for an implementation
error, e.g. the state could not be marshalled, or an anomaly is raised
by the slave.
In this case we fall back to local, lazy, evaluation in the master
process.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures.
Futures can represent local (lazy) computations or remote ones
(delegated). Delegating a future lets a third party assign its
value at some poit in the future; in the meanwhile accessing the
future value raises an exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
|
