aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-12-12 12:00:25 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-12-14 18:02:41 -0500
commit29644bf0814945cbf2b4388b8f8bd19f109503a0 (patch)
treeca37a531989f7c329d78dda769f1f54dc7617ea3
parentb270ad686075e5579dc3826fafdc324ea339785c (diff)
Make [abstract] nodes show up in the Ltac profile
This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise.
-rw-r--r--plugins/ltac/g_ltac.ml412
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--test-suite/output-modulo-time/ltacprof_abstract.out14
-rw-r--r--test-suite/output-modulo-time/ltacprof_abstract.v8
-rw-r--r--test-suite/output/bug5778.out4
-rw-r--r--test-suite/output/bug5778.v7
10 files changed, 52 insertions, 15 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ebf6e450b..8dd4199e3 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -125,9 +125,9 @@ GEXTEND Gram
| IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta
| IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
(*To do: put Abstract in Refiner*)
- | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
+ | IDENT "abstract"; tc = NEXT -> TacAbstract (Loc.tag ~loc:!@loc (tc,None))
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
- TacAbstract (tc,Some s)
+ TacAbstract (Loc.tag ~loc:!@loc (tc,Some s))
| sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ]
(*End of To do*)
| "2" RIGHTA
@@ -401,12 +401,12 @@ VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
END
let is_anonymous_abstract = function
- | TacAbstract (_,None) -> true
- | TacSolve [TacAbstract (_,None)] -> true
+ | TacAbstract (_,(_,None)) -> true
+ | TacSolve [TacAbstract (_,(_,None))] -> true
| _ -> false
let rm_abstract = function
- | TacAbstract (t,_) -> t
- | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
+ | TacAbstract (_,(t,_)) -> t
+ | TacSolve [TacAbstract (_,(t,_))] -> TacSolve [t]
| x -> x
let is_explicit_terminator = function TacSolve _ -> true | _ -> false
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e5ff47356..c9676ac6f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -881,9 +881,9 @@ let pr_goal_selector ~toplevel s =
let rec pr_tac inherited tac =
let return (doc, l) = (tag tac doc, l) in
let (strm, prec) = return (match tac with
- | TacAbstract (t,None) ->
+ | TacAbstract (_,(t,None)) ->
keyword "abstract " ++ pr_tac (labstract,L) t, labstract
- | TacAbstract (t,Some s) ->
+ | TacAbstract (_,(t,Some s)) ->
hov 0 (
keyword "abstract"
++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index ccd555b61..a98752e26 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -249,7 +249,7 @@ and 'a gen_tactic_expr =
| TacProgress of 'a gen_tactic_expr
| TacShowHyps of 'a gen_tactic_expr
| TacAbstract of
- 'a gen_tactic_expr * Id.t option
+ ('a gen_tactic_expr * Id.t option) Loc.located
| TacId of 'n message_token list
| TacFail of global_flag * int or_var * 'n message_token list
| TacInfo of 'a gen_tactic_expr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebffde441..acdbc7d79 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -584,8 +584,8 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars, TacFail (g,intern_int_or_var ist n,intern_message ist l)
| TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
| TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
- | TacAbstract (tac,s) ->
- ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
+ | TacAbstract (loc,(tac,s)) ->
+ ist.ltacvars, TacAbstract (loc,(intern_pure_tactic ist tac,s))
| TacThen (t1,t2) ->
let lfun', t1 = intern_tactic_seq onlytac ist t1 in
let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ded902a8f..dccb7cb75 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1158,10 +1158,14 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
end
- | TacAbstract (tac,ido) ->
+ | TacAbstract (loc,(t,ido)) ->
+ let call = LtacMLCall tac in
+ push_trace(loc,call) ist >>= fun trace ->
+ Profile_ltac.do_profile "eval_tactic:TacAbstract" trace
+ (catch_error_tac trace begin
Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
- (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
- end
+ (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t)
+ end end)
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
| TacDispatch tl ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 79bf3685e..2b4dd2a27 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -192,7 +192,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacId _ | TacFail _ as x -> x
| TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
| TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
- | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
+ | TacAbstract (loc,(tac,s)) -> TacAbstract (loc,(subst_tactic subst tac,s))
| TacThen (t1,t2) ->
TacThen (subst_tactic subst t1, subst_tactic subst t2)
| TacDispatch tl -> TacDispatch (List.map (subst_tactic subst) tl)
diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out
new file mode 100644
index 000000000..c60c5abdd
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_abstract.out
@@ -0,0 +1,14 @@
+total time: 0.964s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0% 1 0.964s
+─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s
+─constructor --------------------------- 0.0% 0.0% 1 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s
+ ├─sleep' ------------------------------ 100.0% 100.0% 1 0.964s
+ └─constructor ------------------------- 0.0% 0.0% 1 0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v
new file mode 100644
index 000000000..10a76309e
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof_abstract.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+ idtac. idtac. abstract (sleep; constructor).
+Defined.
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
new file mode 100644
index 000000000..91ceb1b58
--- /dev/null
+++ b/test-suite/output/bug5778.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
+failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
new file mode 100644
index 000000000..0dcd76aef
--- /dev/null
+++ b/test-suite/output/bug5778.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := abstract b ().
+Ltac c _ := abs ().
+Goal True.
+ Fail c ().
+Abort.