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. --- lib/flags.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index 13525165a..d29064c97 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -226,6 +226,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 0.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode -- cgit v1.2.3 From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 17:15:10 +0200 Subject: Fix bug #4798: compat notations should not modify the parser. This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. --- ide/texmacspp.ml | 3 +- intf/vernacexpr.mli | 3 +- lib/flags.ml | 27 +++++++++------- lib/flags.mli | 1 + parsing/g_vernac.ml4 | 5 ++- printing/ppvernac.ml | 8 ++--- test-suite/bugs/closed/4798.v | 3 ++ toplevel/metasyntax.ml | 75 ++++++++++++++++++++++++++++--------------- 8 files changed, 80 insertions(+), 45 deletions(-) create mode 100644 test-suite/bugs/closed/4798.v (limited to 'lib/flags.ml') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008a..9de1df9f1 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -189,7 +189,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 6df85f076..1063a74d9 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -211,8 +211,9 @@ type syntax_modifier = | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing of Flags.compat_version + | SetOnlyParsing | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version | SetFormat of string * string located type proof_end = diff --git a/lib/flags.ml b/lib/flags.ml index d29064c97..af55e9e2b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current -let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false -| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false -| V8_4, (V8_4 | V8_5 | Current) -> false -| V8_5, (V8_5 | Current) -> false -| Current, Current -> false -| V8_3, V8_2 -> true -| V8_4, (V8_2 | V8_3) -> true -| V8_5, (V8_2 | V8_3 | V8_4) -> true -| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true - +let version_compare v1 v2 = match v1, v2 with +| V8_2, V8_2 -> 0 +| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1 +| V8_3, V8_2 -> 1 +| V8_3, V8_3 -> 0 +| V8_3, (V8_4 | V8_5 | Current) -> -1 +| V8_4, (V8_2 | V8_3) -> 1 +| V8_4, V8_4 -> 0 +| V8_4, (V8_5 | Current) -> -1 +| V8_5, (V8_2 | V8_3 | V8_4) -> 1 +| V8_5, V8_5 -> 0 +| V8_5, Current -> -1 +| Current, Current -> 0 +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1 + +let version_strictly_greater v = version_compare !compat_version v > 0 let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function diff --git a/lib/flags.mli b/lib/flags.mli index 839c252cb..9dc0c9c04 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -64,6 +64,7 @@ val univ_print : bool ref type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref +val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b0b656acf..1a4012891 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1115,10 +1115,9 @@ GEXTEND Gram | IDENT "right"; IDENT "associativity" -> SetAssoc RightA | IDENT "no"; IDENT "associativity" -> SetAssoc NonA | IDENT "only"; IDENT "printing" -> SetOnlyPrinting - | IDENT "only"; IDENT "parsing" -> - SetOnlyParsing Flags.Current + | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> - SetOnlyParsing (Coqinit.get_compat_version s) + SetCompatVersion (Coqinit.get_compat_version s) | IDENT "format"; s1 = [s = STRING -> (!@loc,s)]; s2 = OPT [s = STRING -> (!@loc,s)] -> begin match s1, s2 with diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1d8dcabcc..503b29aaf 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -367,8 +367,8 @@ module Make | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing Flags.Current -> keyword "only parsing" - | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s @@ -1002,13 +1002,13 @@ module Make ) | VernacHints (_, dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),_,compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + (match compat with None -> [] | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 000000000..dbc3d46fc --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a1edb7139..ce8798c71 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -673,8 +673,13 @@ type syntax_extension = { synext_notgram : notation_grammar; synext_unparsing : unparsing list; synext_extra : (string * string) list; + synext_compat : Flags.compat_version option; } +let is_active_compat = function +| None -> true +| Some v -> 0 <= Flags.version_compare v !Flags.compat_version + type syntax_extension_obj = locality_flag * syntax_extension list let cache_one_syntax_extension se = @@ -685,13 +690,15 @@ let cache_one_syntax_extension se = let oldprec = Notation.level_of_notation ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec with Not_found -> - (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; - (* Declare the parsing rule *) - if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; - (* Declare the notation rule *) - Notation.declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + if is_active_compat se.synext_compat then begin + (* Reserve the notation level *) + Notation.declare_notation_level ntn prec; + (* Declare the parsing rule *) + if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram; + (* Declare the notation rule *) + Notation.declare_notation_rule ntn + ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram + end let cache_syntax_extension (_, (_, sy)) = List.iter cache_one_syntax_extension sy @@ -725,9 +732,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj = let interp_modifiers modl = let onlyparsing = ref false in let onlyprinting = ref false in + let compat = ref None in let rec interp assoc level etyps format extra = function | [] -> - (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra) + (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra) | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then @@ -749,12 +757,15 @@ let interp_modifiers modl = | SetAssoc a :: l -> if not (Option.is_empty assoc) then error"An associativity is given more than once."; interp (Some a) level etyps format extra l - | SetOnlyParsing _ :: l -> + | SetOnlyParsing :: l -> onlyparsing := true; interp assoc level etyps format extra l | SetOnlyPrinting :: l -> onlyprinting := true; interp assoc level etyps format extra l + | SetCompatVersion v :: l -> + compat := Some v; + interp assoc level etyps format extra l | SetFormat ("text",s) :: l -> if not (Option.is_empty format) then error "A format is given more than once."; interp assoc level etyps (Some s) extra l @@ -763,7 +774,7 @@ let interp_modifiers modl = in interp None None [] None [] modl let check_infix_modifiers modifiers = - let (_, _, t, _, _, _, _) = interp_modifiers modifiers in + let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in if not (List.is_empty t) then error "Explicit entry level or type unexpected in infix notation." @@ -775,20 +786,25 @@ let check_useless_entry_types recvars mainvars etyps = | _ -> () let not_a_syntax_modifier = function -| SetOnlyParsing _ -> true +| SetOnlyParsing -> true | SetOnlyPrinting -> true +| SetCompatVersion _ -> true | _ -> false let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods let is_only_parsing mods = - let test = function SetOnlyParsing _ -> true | _ -> false in + let test = function SetOnlyParsing -> true | _ -> false in List.exists test mods let is_only_printing mods = let test = function SetOnlyPrinting -> true | _ -> false in List.exists test mods +let get_compat_version mods = + let test = function SetCompatVersion v -> Some v | _ -> None in + try Some (List.find_map test mods) with Not_found -> None + (* Compute precedences from modifiers (or find default ones) *) let set_entry_type etyps (x,typ) = @@ -966,7 +982,7 @@ let remove_curly_brackets l = in aux true l let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in + let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in let (recvars,mainvars,symbols) = analyze_notation_tokens toks in @@ -992,12 +1008,12 @@ let compute_syntax_data df modifiers = let sy_data = (n,sy_typs,symbols',fmt) in let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in + let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in (* Return relevant data for interpretation and for parsing/printing *) (msgs,i_data,i_typs,sy_fulldata,extra) let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in + let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then (Feedback.msg_warning ?loc:None, @@ -1014,6 +1030,7 @@ type notation_obj = { notobj_interp : interpretation; notobj_onlyparse : bool; notobj_onlyprint : bool; + notobj_compat : Flags.compat_version option; notobj_notation : notation * notation_location; } @@ -1024,7 +1041,9 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin + let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in + let active = is_active_compat nobj.notobj_compat in + if Int.equal i 1 && fresh && active then begin (* Declare the interpretation *) let onlyprint = nobj.notobj_onlyprint in let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in @@ -1094,7 +1113,9 @@ let recover_syntax ntn = synext_notation = ntn; synext_notgram = pa_rule; synext_unparsing = pp_rule; - synext_extra = pp_extra_rules } + synext_extra = pp_extra_rules; + synext_compat = None; + } with Not_found -> raise NoSyntaxRule @@ -1128,7 +1149,7 @@ let make_pp_rule (n,typs,symbols,fmt) = | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) -let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = +let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat = let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in let pp_rule = make_pp_rule sy_data in let sy = { @@ -1137,6 +1158,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint = synext_notgram = pa_rule; synext_unparsing = pp_rule; synext_extra = extra; + synext_compat = compat; } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open @@ -1153,9 +1175,9 @@ let to_map l = let add_notation_in_scope local df c mods scope = let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in (* Prepare the interpretation *) - let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in + let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint compat in let i_vars = make_internalization_vars recvars mainvars i_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1173,6 +1195,7 @@ let add_notation_in_scope local df c mods scope = (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in (* Ready to change the global state *) @@ -1181,7 +1204,7 @@ let add_notation_in_scope local df c mods scope = Lib.add_anonymous_leaf (inNotation notation); df' -let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint = +let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) @@ -1212,6 +1235,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (** Order is important here! *) notobj_onlyparse = onlyparse; notobj_onlyprint = onlyprint; + notobj_compat = compat; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1221,19 +1245,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) let add_syntax_extension local ((loc,df),mods) = let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra onlyprint in + let sy_rules = make_syntax_rules sy_data extra onlyprint None in Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) let add_notation_interpretation ((loc,df),c,sc) = - let df' = add_notation_interpretation_core false df c sc false false in + let df' = add_notation_interpretation_core false df c sc false false None in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ()); + (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> error "Parsing rule for this notation has to be previously declared."); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc @@ -1246,7 +1270,8 @@ let add_notation local c ((loc,df),modifiers) sc = (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in - try add_notation_interpretation_core local df c sc onlyparse onlyprint + let compat = get_compat_version modifiers in + try add_notation_interpretation_core local df c sc onlyparse onlyprint compat with NoSyntaxRule -> (* Try to determine a default syntax rule *) add_notation_in_scope local df c modifiers sc -- cgit v1.2.3 From 46daf37ed46397b03a30fa2d89b62ffcc2c8d166 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Sep 2016 14:32:50 -0400 Subject: Set the default LtacProf cutoff to 2% This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time. --- lib/flags.ml | 2 +- test-suite/Makefile | 2 +- test-suite/output-modulo-time/ltacprof.v | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/flags.ml') diff --git a/lib/flags.ml b/lib/flags.ml index af55e9e2b..65873e521 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -231,7 +231,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false -let profile_ltac_cutoff = ref 0.0 +let profile_ltac_cutoff = ref 2.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/test-suite/Makefile b/test-suite/Makefile index a40ea80ae..d2899034b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -51,7 +51,7 @@ SINGLE_QUOTE=" get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1))))) # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) -has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) +has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index d79451f0f..6611db70e 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. -- cgit v1.2.3