From c1388ce6338742ab20aea9774e6510f43d7697ff Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 3 Oct 2013 09:09:22 +0000
Subject: STM: delegate proofs to slaves only if they are not trivial

Still too simple and not configurable

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

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index e20e75194e..8165da5d52 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -920,6 +920,8 @@ end = struct (* {{{ *)
 
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
+let delegate_policy_check l = interactive () = `Yes || List.length l > 20
+
 let collect_proof cur hd id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id); 
  let is_defined = function
@@ -934,10 +936,12 @@ let collect_proof cur hd id =
         `NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
     | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        `Optimizable (parent, Some v, accn)
+        if delegate_policy_check accn then `Optimizable (parent, Some v, accn)
+        else `NotOptimizable `TooShort
     | Some (parent, _), `Fork (_, hd', _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
-        `MaybeOptimizable (parent, accn)
+        if delegate_policy_check accn then `MaybeOptimizable (parent, accn)
+        else `NotOptimizable `TooShort
     | _, `Sideff se -> collect None (id::accn) view.next
     | _ -> `NotOptimizable `Unknown in
  match cur, (VCS.visit id).step with
-- 
cgit v1.2.3