From fd47b2d2638518fe62ce9c63557d2dab219d9558 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 30 Jun 2016 19:41:53 +0200 Subject: Goal selectors now use the keyword [only]. This fixes some parsing problems when doing things like [let n := 2 in idtac n]. See bug #4877. --- ltac/g_ltac.ml4 | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'ltac') diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index b5494a7cbb..fbeb89a634 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -45,7 +45,6 @@ let new_entry name = let e = Gram.entry_create name in e -let selector = new_entry "vernac:selector" let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" @@ -79,7 +78,7 @@ let warn_deprecated_appcontext = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - tactic_mode constr_may_eval constr_eval selector toplevel_selector; + tactic_mode constr_may_eval constr_eval toplevel_selector; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -316,13 +315,16 @@ GEXTEND Gram l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; + selector_body: + [ [ l = range_selector_or_nth -> l + | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ] + ; selector: - [ [ l = range_selector_or_nth; ":" -> l - | IDENT "all" ; ":" -> SelectAll ] ] + [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] ; toplevel_selector: - [ [ s = selector -> s - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ] + [ [ sel = selector_body; ":" -> sel + | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] -- cgit v1.2.3 From e1df1b77f8c72636b6e347f41f6f38976c86e909 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Sep 2016 16:32:42 +0200 Subject: -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100) With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files. --- ltac/profile_ltac.ml | 4 ++-- ltac/profile_ltac_tactics.ml4 | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'ltac') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 102918e5e5..a91ff98fb9 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -401,11 +401,11 @@ let print_results ~cutoff = print_results_filter ~cutoff ~filter:(fun _ -> true) let print_results_tactic tactic = - print_results_filter ~cutoff:0.0 ~filter:(fun s -> + print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s -> String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = - if get_profiling () then print_results ~cutoff:0.0 + if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 9083bda60a..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END -- cgit v1.2.3 From cf87e73ff4dd0b9c70436d66d326ae839868ba78 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Sep 2016 17:26:14 +0200 Subject: Fix bug #5036 autorewrite, sections and universes Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately). --- ltac/extratactics.ml4 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ltac') diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index e50b0520bc..d6ba670d83 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,7 +263,8 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Global.push_context_set false ctx; Univ.ContextSet.empty) + else (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in -- cgit v1.2.3 From c4c7aa6d7b14a6d76c287b97d487abe055406577 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 18:28:24 -0400 Subject: LtacProf cutoff is for total percent, not time --- ltac/profile_ltac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ltac') diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index a91ff98fb9..2514ededb0 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -128,7 +128,7 @@ let to_ltacprof_results xml = | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") let feedback_results results = - Feedback.(feedback + Feedback.(feedback (Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results))) (* ************** pretty printing ************************************* *) @@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node = !global in warn_encountered_multi_success_backtracking (); - let filter s n = filter s && n >= cutoff in + let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ -- cgit v1.2.3