aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/ppvernac.ml1
-rw-r--r--proofs/proof_type.ml4
-rw-r--r--proofs/proof_type.mli4
-rw-r--r--tactics/tacinterp.ml21
-rw-r--r--toplevel/himsg.ml69
-rw-r--r--toplevel/himsg.mli3
-rw-r--r--toplevel/vernac.ml28
-rw-r--r--toplevel/vernacentries.ml3
-rw-r--r--toplevel/vernacexpr.ml1
10 files changed, 86 insertions, 52 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7f4a99542..dfe79a254 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -65,8 +65,8 @@ let no_hook _ _ = ()
GEXTEND Gram
GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
vernac: FIRST
- [ [ IDENT "Time"; locality; v = vernac_aux ->
- check_locality (); VernacTime v
+ [ [ IDENT "Time"; v = vernac -> VernacTime v
+ | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v)
| locality; v = vernac_aux ->
check_locality (); v ] ]
;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 7b3491de2..b86f5ce66 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -489,6 +489,7 @@ let rec pr_vernac = function
| VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
++ spc()) else spc() ++ qs s
| VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
+ | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v
(* Syntax *)
| VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index dabc84ca3..5bd8060ae 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -102,8 +102,8 @@ type ltac_call_kind =
| LtacConstrInterp of rawconstr *
((identifier * constr) list * (identifier * identifier option) list)
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
let abstract_tactic_box = ref (ref None)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 1529a07f3..0bd0eaa11 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -137,8 +137,8 @@ type ltac_call_kind =
| LtacConstrInterp of rawconstr *
((identifier * constr) list * (identifier * identifier option) list)
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
val abstract_tactic_box : atomic_tactic_expr option ref ref
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0129c06c8..ac65d3a52 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -93,13 +93,13 @@ let catch_error call_trace tac g =
| LtacLocated _ as e -> raise e
| Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
| e ->
- let (loc',c),tail = list_sep_last call_trace in
+ let (nrep,loc',c),tail = list_sep_last call_trace in
let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
if tail = [] then
let loc = if loc = dloc then loc' else loc in
raise (Stdpp.Exc_located(loc,e'))
else
- raise (Stdpp.Exc_located(loc',LtacLocated((c,tail,loc),e')))
+ raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign =
@@ -295,10 +295,14 @@ let lookup_genarg_glob id = let (f,_,_) = lookup_genarg id in f
let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f
let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f
+let push_trace (loc,ck) = function
+ | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl
+ | trl -> (1,loc,ck)::trl
+
let propagate_trace ist loc id = function
| VFun (_,lfun,it,b) ->
let t = if it=[] then b else TacFun (it,b) in
- VFun ((loc,LtacVarCall (id,t))::ist.trace,lfun,it,b)
+ VFun (push_trace(loc,LtacVarCall (id,t)) ist.trace,lfun,it,b)
| x -> x
(* Dynamically check that an argument is a tactic *)
@@ -1453,7 +1457,7 @@ let interp_gen kind ist sigma env (c,ce) =
| Some c ->
let ltacdata = (List.map fst ltacvars,unbndltacvars) in
intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
- let trace = (dloc,LtacConstrInterp (c,vars))::ist.trace in
+ let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c
(* Interprets a constr and solve remaining evars with default tactic *)
@@ -1756,9 +1760,10 @@ and eval_tactic ist = function
let box = ref None in abstract_tactic_box := box;
let call = LtacAtomCall (t,box) in
let tac = (* catch error in the interpretation *)
- catch_error ((dloc,call)::ist.trace) (interp_atomic ist gl) t in
+ catch_error (push_trace(dloc,call)ist.trace)
+ (interp_atomic ist gl) t in
(* catch error in the evaluation *)
- catch_error ((loc,call)::ist.trace) tac gl
+ catch_error (push_trace(loc,call)ist.trace) tac gl
| TacFun _ | TacLetIn _ -> assert false
| TacMatchGoal _ | TacMatch _ -> assert false
| TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
@@ -1804,7 +1809,7 @@ and interp_ltac_reference loc' mustbetac ist gl = function
let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in
let ist =
{ lfun=[]; debug=ist.debug; avoid_ids=ids;
- trace = loc_info::ist.trace } in
+ trace = push_trace loc_info ist.trace } in
val_interp ist gl (lookup r)
and interp_tacarg ist gl = function
@@ -2392,7 +2397,7 @@ and interp_atomic ist gl = function
in
let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
- let trace = (loc,LtacNotationCall s)::ist.trace in
+ let trace = push_trace (loc,LtacNotationCall s) ist.trace in
interp_tactic { ist with lfun=lfun; trace=trace } body gl
let make_empty_glob_sign () =
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 03:42:48 +0000