commande Timeout + compaction des traces de debug_tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11959 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 66 insertions, 38 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e8ca54c9c..6f1e95d60 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -792,37 +792,44 @@ let explain_reduction_tactic_error = function
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' e
 
-let explain_ltac_call_trace (last,trace,loc) =
-  let calls = last :: List.rev (List.map snd trace) in
-  let pr_call = function
-  | Proof_type.LtacNotationCall s -> quote (str s)
-  | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
-  | Proof_type.LtacVarCall (id,t) ->
-      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ 
-      Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-  | Proof_type.LtacAtomCall (te,otac) -> quote
-      (Pptactic.pr_glob_tactic (Global.env())
-	(Tacexpr.TacAtom (dummy_loc,te)))
-      ++ (match !otac with
-      | Some te' when (Obj.magic te' <> te) ->
-	  strbrk " (expanded to " ++ quote
-	  (Pptactic.pr_tactic (Global.env())
-	    (Tacexpr.TacAtom (dummy_loc,te')))
-	++ str ")"
-      | _ -> mt ())
-  | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
-      let filter =
-	function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
-      let unboundvars = list_map_filter filter unboundvars in
-      quote (pr_rawconstr_env (Global.env()) c) ++
-      (if unboundvars <> [] or vars <> [] then
-	strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> 
-	pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
-	  (List.rev vars @ unboundvars)
-       else mt()) ++ str ")" in
-  if calls <> [] then
-    let kind_of_last_call = match list_last calls with
-    | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
+let explain_ltac_call_trace (nrep,last,trace,loc) =
+  let calls =
+    (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in
+  let pr_call (n,ck) =
+    (match ck with
+       | Proof_type.LtacNotationCall s -> quote (str s)
+       | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+       | Proof_type.LtacVarCall (id,t) ->
+	   quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ 
+	     Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+       | Proof_type.LtacAtomCall (te,otac) -> quote
+	   (Pptactic.pr_glob_tactic (Global.env())
+	      (Tacexpr.TacAtom (dummy_loc,te)))
+	   ++ (match !otac with
+		 | Some te' when (Obj.magic te' <> te) ->
+		     strbrk " (expanded to " ++ quote
+		       (Pptactic.pr_tactic (Global.env())
+			  (Tacexpr.TacAtom (dummy_loc,te')))
+		     ++ str ")"
+		 | _ -> mt ())
+       | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
+	   let filter =
+	     function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
+	   let unboundvars = list_map_filter filter unboundvars in
+	   quote (pr_rawconstr_env (Global.env()) c) ++
+	     (if unboundvars <> [] or vars <> [] then
+		strbrk " (with " ++
+		  prlist_with_sep pr_coma
+		  (fun (id,c) -> 
+		     pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
+		  (List.rev vars @ unboundvars)
+	      else mt()) ++ str ")") ++
+      (if n=2 then str " (repeated twice)"
+       else if n>2 then str " (repeated "++int n++str" times)"
+       else mt()) in
+    if calls <> [] then
+      let kind_of_last_call = match list_last calls with
+    | (_,Proof_type.LtacConstrInterp _) -> ", last term evaluation failed."
     | _ -> ", last call failed." in
     hov 0 (str "In nested Ltac calls to " ++ 
            pr_enum pr_call calls ++ strbrk kind_of_last_call)
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 053bf16a3..8cc179e81 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -42,4 +42,5 @@ val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
 val explain_ltac_call_trace : 
-  Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> std_ppcmds
+  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc ->
+  std_ppcmds
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index aa519cd8c..fad6d8e98 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -51,6 +51,8 @@ let real_error = function
   | Error_in_file (_, _, e) -> e
   | e -> e
 
+let timeout_handler _ = error "Timeout!"
+
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
@@ -159,11 +161,27 @@ let rec vernac_com interpfun (loc,com) =
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
     | VernacTime v ->
-	let tstart = System.get_time() in
-        if not !just_parsing then interp v;
-	let tend = System.get_time() in
-        msgnl (str"Finished transaction in " ++
-                 System.fmt_time_difference tstart tend)
+	if not !just_parsing then begin
+	  let tstart = System.get_time() in
+          interp v;
+	  let tend = System.get_time() in
+          msgnl (str"Finished transaction in " ++
+                   System.fmt_time_difference tstart tend)
+	end
+
+    | VernacTimeout(n,v) ->
+	if not !just_parsing then begin
+	  let psh =
+	    Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
+	  ignore (Unix.alarm n);
+	  let stop() =
+	    (* stop alarm *)
+	    ignore(Unix.alarm 0);
+	    (* restore handler *)
+	    Sys.set_signal Sys.sigalrm psh in
+	  try interp v; stop()
+	  with e -> stop(); raise e
+	end
 
     | v -> if not !just_parsing then interpfun v
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5796d79ee..4e9edd90a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1291,7 +1291,8 @@ let vernac_check_guard () =
 
 let interp c = match c with
   (* Control (done in vernac) *)
-  | (VernacTime _ | VernacList _ | VernacLoad _) -> assert false
+  | (VernacTime _ | VernacList _ | VernacLoad _| VernacTimeout _) ->
+      assert false
 
   (* Syntax *)
   | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b94526a6e..7a9e2b5a6 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -188,6 +188,7 @@ type vernac_expr =
   | VernacList of located_vernac_expr list
   | VernacLoad of verbose_flag * lstring
   | VernacTime of vernac_expr
+  | VernacTimeout of int * vernac_expr
 
   (* Syntax *) 
   | VernacTacticNotation of int * grammar_production list * raw_tactic_expr