diff options
| author | gareuselesinge | 2013-08-30 12:20:07 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-30 12:20:07 +0000 |
| commit | de9798346c7df0593d4d7b83a8f316991f6fb230 (patch) | |
| tree | 3541e5bfc7127f14a3a789c0076776c3d0917e9b /lib/future.ml | |
| parent | e458f2e2beb65e49c4bb45c54ab07ce3b0b8a9bb (diff) | |
Stm: if slave process dies badly go back to local lazy evaluation
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
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/future.ml b/lib/future.ml index 292fd6648a..3cbaa95dc5 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -59,9 +59,15 @@ let proj = function let create f = ref (Closure f) +type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] let create_delegate () = let c = ref Delegated in - c, (function `Val v -> c := Val (v, None) | `Exn e -> c := Exn e) + c, (fun v -> + assert (!c = Delegated); + match v with + | `Val v -> c := Val (v, None) + | `Exn e -> c := Exn e + | `Comp f -> c := !f) (* TODO: get rid of try/catch *) let compute ~pure c : 'a value = match !c with |