From 81cddc53da47e26bb43771e46e9a1ce03de60d60 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 10 Oct 2013 11:22:51 +0000
Subject: STM: a proof with nested proofs cannot be delegated

The reason is that the state gets altered by side effects
by the Qed of inner proofs.  This kind of side effects cannot
be reproduced in the slaves easily.  And there is no point
in working hard for this corner case.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 1eae14a3a5..3457afff16 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -971,7 +971,8 @@ let collect_proof cur hd id =
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         if delegate_policy_check accn then `MaybeOptimizable (parent, accn)
         else `NotOptimizable `TooShort
-    | _, `Sideff se -> collect None (id::accn) view.next
+    | _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
+    | _, `Sideff (`Id _) -> `NotOptimizable `NestedProof
     | _ -> `NotOptimizable `Unknown in
  match cur, (VCS.visit id).step with
  | (parent, (_,_,VernacExactProof _)), `Fork _ ->
@@ -981,6 +982,14 @@ let collect_proof cur hd id =
      else if is_defined cur then `NotOptimizable `Transparent
      else collect (Some cur) [] id
 
+let string_of_reason = function
+  | `Transparent -> "Transparent"
+  | `AlreadyEvaluated -> "AlreadyEvaluated"
+  | `TooShort -> "TooShort"
+  | `NestedProof -> "NestedProof"
+  | `Immediate -> "Immediate"
+  | _ -> "Unknown Reason"
+
 let known_state ?(redefine_qed=false) ~cache id =
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -1052,11 +1061,7 @@ let known_state ?(redefine_qed=false) ~cache id =
               ), `Yes
           | `NotOptimizable reason -> (fun () ->
                 prerr_endline ("NotOptimizable " ^ Stateid.to_string id ^ " " ^
-                  match reason with
-                  | `Transparent -> "Transparent"
-                  | `AlreadyEvaluated -> "AlreadyEvaluated"
-                  | `TooShort -> "TooShort"
-                  | _ -> "WTF");
+                  string_of_reason reason);
                 reach eop;
                 begin match keep with
                 | VtKeep ->
-- 
cgit v1.2.3