From 45748e4efae8630cc13b0199dfcc9803341e8cd8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Jun 2015 10:08:58 +0200 Subject: Strip some trailing spaces --- Makefile.build | 22 +++++++++++----------- Makefile.common | 14 +++++++------- lib/pp.ml | 2 +- ltac/tacinterp.ml | 18 +++++++++--------- 4 files changed, 28 insertions(+), 28 deletions(-) diff --git a/Makefile.build b/Makefile.build index fc92507e6..44eb42f9a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -78,8 +78,8 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile -# The SHOW and HIDE variables control whether make will echo complete commands -# or only abbreviated versions. +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make SHOW := $(if $(VERBOSE),@true "",@echo "") @@ -231,7 +231,7 @@ grammar/grammar.cma : $(GRAMCMO) $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml $(HIDE)$(GRAMC) test.ml -o test-grammar @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ ## Support of Camlp5 and Camlp5 @@ -283,7 +283,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -293,7 +293,7 @@ $(COQTOPEXE): $(COQTOPBYTE) endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) @@ -896,7 +896,7 @@ install-emacs: install-latex: $(MKDIR) $(FULLCOQDOCDIR) - $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) + $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) ########################################################################### @@ -968,7 +968,7 @@ dev/printers.cma: dev/printers.mllib $(SHOW)'Testing $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer @rm -f test-printer - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here @@ -1107,7 +1107,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob + $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' @@ -1187,7 +1187,7 @@ otags: Makefile Makefile.build Makefile.common config/Makefile : ; -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/Makefile.common b/Makefile.common index 86a7ea847..f592cd6ec 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQC:=bin/coqc$(EXE) @@ -35,7 +35,7 @@ else endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -119,7 +119,7 @@ HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): COQTEXOPTS:=-boot -n 72 -sl -small -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex RefMan-ext.v.tex \ @@ -149,7 +149,7 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ########################################################################### -# Object and Source files +# Object and Source files ########################################################################### COQRUN := coqrun @@ -393,7 +393,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/lib/pp.ml b/lib/pp.ml index d07f01b90..99c774e8d 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -44,7 +44,7 @@ end module Tag : sig - type t + type t type 'a key val create : string -> 'a key val inj : 'a -> 'a key -> t diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5ee9b0fc4..2c1f59634 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -988,7 +988,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_map (interp_binding ist env) sigma l in @@ -1164,7 +1164,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1309,7 +1309,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in - let extra = TacStore.set ist.extra f_avoid_ids ids in + let extra = TacStore.set ist.extra f_avoid_ids ids in let extra = TacStore.set extra f_trace (push_trace loc_info ist) in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in @@ -1633,7 +1633,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the @@ -1648,7 +1648,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in - (k,(loc,f))) cb + (k,(loc,f))) cb in let sigma,tac = match cl with | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l @@ -1661,7 +1661,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacElim (ev,(keep,cb),cbo) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = project gl in + let sigma = project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1715,7 +1715,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = + let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in @@ -1825,7 +1825,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let sigma = Sigma.to_evar_map sigma in @@ -1851,7 +1851,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in -- cgit v1.2.3 From 9ff2c9d8d042c9989b6a8138c308398c49ae116f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Jun 2015 10:12:41 +0200 Subject: LtacProf for Coq trunk This add LtacProfiling. Much of the code was written by Tobias Tebbi (@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq v8.5 and Coq trunk. --- .gitignore | 1 + Makefile.build | 2 +- Makefile.common | 5 +- lib/pp.ml | 32 +++++ lib/pp.mli | 3 + library/declaremods.ml | 6 + library/declaremods.mli | 3 + ltac/ltac.mllib | 1 + ltac/profile_ltac_tactics.ml4 | 40 ++++++ ltac/tacinterp.ml | 41 +++--- ltacprof/ltacprof.mllib | 1 + ltacprof/profile_ltac.ml | 286 ++++++++++++++++++++++++++++++++++++++++++ ltacprof/profile_ltac.mli | 15 +++ test-suite/success/ltacprof.v | 8 ++ tools/coq_makefile.ml | 5 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 1 + toplevel/usage.ml | 1 + 18 files changed, 432 insertions(+), 21 deletions(-) create mode 100644 ltac/profile_ltac_tactics.ml4 create mode 100644 ltacprof/ltacprof.mllib create mode 100644 ltacprof/profile_ltac.ml create mode 100644 ltacprof/profile_ltac.mli create mode 100644 test-suite/success/ltacprof.v diff --git a/.gitignore b/.gitignore index 116f88dd7..bc1a05684 100644 --- a/.gitignore +++ b/.gitignore @@ -128,6 +128,7 @@ parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml ltac/extraargs.ml +ltac/profile_ltac_tactics.ml ide/coqide_main.ml # other auto-generated files diff --git a/Makefile.build b/Makefile.build index 44eb42f9a..c6fef10b6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -570,7 +570,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac +.PHONY: engine highparsing stm toplevel ltac ltacprof lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma diff --git a/Makefile.common b/Makefile.common index f592cd6ec..37db66be3 100644 --- a/Makefile.common +++ b/Makefile.common @@ -62,7 +62,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp stm \ + proofs tactics pretyping interp stm ltacprof\ toplevel parsing printing intf engine ltac PLUGINS:=\ @@ -167,7 +167,8 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma + stm/stm.cma ltacprof/ltacprof.cma toplevel/toplevel.cma \ + parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/lib/pp.ml b/lib/pp.ml index 99c774e8d..5d7c71635 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -168,6 +168,38 @@ let utf8_length s = done ; !cnt +(* Variant of String.sub for UTF8 character positions *) +let utf8_sub s start_u len_u = + let len_b = String.length s + and end_u = start_u + len_u + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + let start_b = ref len_b in + while !p < len_b && !cnt < end_u do + if !cnt <= start_u then start_b := !p ; + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len_b && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + let end_b = !p in + String.sub s !start_b (end_b - !start_b) + (* formatting commands *) let str s = Glue.atom(Ppcmd_print (Str_def s)) let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i))) diff --git a/lib/pp.mli b/lib/pp.mli index a18744c37..56b82e448 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -100,6 +100,9 @@ val close_tag : unit -> std_ppcmds val string_of_ppcmds : std_ppcmds -> string +val utf8_length : string -> int +val utf8_sub : string -> int -> int -> string + (** {6 Printing combinators} *) val pr_comma : unit -> std_ppcmds diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa0..dcd63c769 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087..3917fe8d6 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -90,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index e0c6f3ac0..d8854e6e7 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -10,6 +10,7 @@ Extraargs G_obligations Coretactics Extratactics +Profile_ltac_tactics G_auto G_class Rewrite diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 new file mode 100644 index 000000000..0c4e0b075 --- /dev/null +++ b/ltac/profile_ltac_tactics.ml4 @@ -0,0 +1,40 @@ +(*i camlp4deps: "grammar/grammar.cma" i*) + +open Profile_ltac +open Stdarg + +DECLARE PLUGIN "profile_ltac_plugin" + +let tclSET_PROFILING b = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + set_profiling b)) + +TACTIC EXTEND start_profiling + | [ "start" "profiling" ] -> [ tclSET_PROFILING true ] +END + +TACTIC EXTEND stop_profiling + | [ "stop" "profiling" ] -> [ tclSET_PROFILING false ] +END;; + + +VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF + [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ] +END + +VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF + [ "Stop" "Profiling" ] -> [ set_profiling false ] + END + +VERNAC COMMAND EXTEND ResetProfiling CLASSIFIED AS SIDEFF + [ "Reset" "Profile" ] -> [ reset_profile() ] +END + +VERNAC COMMAND EXTEND ShowProfile CLASSIFIED AS QUERY + [ "Show" "Profile" ] -> [ print_results() ] +END + + +VERNAC COMMAND EXTEND ShowProfileTactic CLASSIFIED AS QUERY + [ "Show" "Profile" string(s) ] -> [ print_results_tactic s ] +END diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 2c1f59634..4f7c02968 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -286,9 +286,10 @@ let constr_of_id env id = (** Generic arguments : table of interpretation functions *) +(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *) let push_trace call ist = match TacStore.get ist.extra f_trace with -| None -> [call] -| Some trace -> call :: trace +| None -> Proofview.tclUNIT [call] +| Some trace -> Proofview.tclLIFT (Proofview.NonLogical.make Profile_ltac.entered_call) <*> Proofview.tclUNIT (call :: trace) let propagate_trace ist loc id v = let v = Value.normalize v in @@ -297,10 +298,11 @@ let propagate_trace ist loc id v = match tacv with | VFun (appl,_,lfun,it,b) -> let t = if List.is_empty it then b else TacFun (it,b) in - let ans = VFun (appl,push_trace(loc,LtacVarCall (id,t)) ist,lfun,it,b) in - of_tacvalue ans - | _ -> v - else v + push_trace(loc,LtacVarCall (id,t)) ist >>= fun trace -> + let ans = VFun (appl,trace,lfun,it,b) in + Proofview.tclUNIT (of_tacvalue ans) + | _ -> Proofview.tclUNIT v + else Proofview.tclUNIT v let append_trace trace v = let v = Value.normalize v in @@ -622,8 +624,13 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in intern_gen kind_for_intern ~allow_patvar ~ltacvars env c in - let trace = - push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in + (* Jason Gross: To avoid unnecessary modifications to tacinterp, as + suggested by Arnaud Spiwack, we run push_trace immediately. We do + this with the kludge of an empty proofview, and rely on the + invariant that running the tactic returned by push_trace does + not modify sigma. *) + let (_, dummy_proofview) = Proofview.init sigma [] in + let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) c in @@ -1169,7 +1176,9 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> let call = LtacAtomCall t in - catch_error_tac (push_trace(loc,call) ist) (interp_atomic ist t) + push_trace(loc,call) ist >>= fun trace -> + Profile_ltac.do_profile "eval_tactic:2" trace + (catch_error_tac trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ -> assert false | TacMatchGoal _ | TacMatch _ -> assert false | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) @@ -1251,7 +1260,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let tac l = let addvar x v accu = Id.Map.add x v accu in let lfun = List.fold_right2 addvar ids l ist.lfun in - let trace = push_trace (loc,LtacNotationCall s) ist in + Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in @@ -1276,7 +1285,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> - let trace = push_trace (loc,LtacMLCall tac) ist in + push_trace (loc,LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in @@ -1302,15 +1311,17 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id in - Ftactic.bind (force_vrec ist v) begin fun v -> - let v = propagate_trace ist loc id v in + let open Ftactic in + force_vrec ist v >>= begin fun v -> + Ftactic.lift (propagate_trace ist loc id v) >>= fun v -> if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in let loc_info = ((if Loc.is_ghost loc' then loc else loc'),LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in - let extra = TacStore.set extra f_trace (push_trace loc_info ist) in + push_trace loc_info ist >>= fun trace -> + let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; extra = extra; } in let appl = GlbAppl[r,[]] in val_interp ~appl ist (Tacenv.interp_ltac r) @@ -1408,7 +1419,7 @@ and tactic_of_value ist vle = lfun = lfun; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in - catch_error_tac trace tac + Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/ltacprof/ltacprof.mllib b/ltacprof/ltacprof.mllib new file mode 100644 index 000000000..383e5d285 --- /dev/null +++ b/ltacprof/ltacprof.mllib @@ -0,0 +1 @@ +Profile_ltac diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml new file mode 100644 index 000000000..889ae77b8 --- /dev/null +++ b/ltacprof/profile_ltac.ml @@ -0,0 +1,286 @@ +open Pp +open Printer +open Util + + +let is_profiling = ref false +let set_profiling b = is_profiling := b + +let should_display_profile_at_close = ref false +let set_display_profile_at_close b = should_display_profile_at_close := b + + +let new_call = ref false +let entered_call() = new_call := true +let is_new_call() = let b = !new_call in new_call := false; b + +(** Local versions of the old Pp.msgnl *) +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + +(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) +let encountered_multi_success_backtracking = ref false +let warn_encountered_multi_success_backtracking() = + if !encountered_multi_success_backtracking + then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") +let encounter_multi_success_backtracking() = + if not !encountered_multi_success_backtracking + then begin + encountered_multi_success_backtracking := true; + warn_encountered_multi_success_backtracking() + end + + +type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} +let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} +let add_entry e add_total {total; local; ncalls; max_total} = + if add_total then e.total <- e.total +. total; + e.local <- e.local +. local; + e.ncalls <- e.ncalls + ncalls; + if add_total then e.max_total <- max e.max_total max_total + +type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} +let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}] + +let on_stack = Hashtbl.create 5 + +let get_node c table = + try Hashtbl.find table c + with Not_found -> + let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in + Hashtbl.add table c new_node; + new_node + +let rec add_node node node' = + add_entry node.entry true node'.entry; + Hashtbl.iter + (fun s node' -> add_node (get_node s node.children) node') + node'.children + +let time() = + let times = Unix.times() in + times.Unix.tms_utime +. times.Unix.tms_stime + +let rec print_treenode indent (tn : treenode) = + msgnl(str(indent^"{ entry = {")); + Feedback.msg_notice(str(indent^"total = ")); + msgnl(str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice(str(indent^"local = ")); + msgnl(str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice(str(indent^"ncalls = ")); + msgnl(str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice(str(indent^"max_total = ")); + msgnl(str (indent^(string_of_float tn.entry.max_total))); + msgnl(str(indent^"}")); + msgnl(str(indent^"children = {")); + Hashtbl.iter + (fun s node -> + msgnl(str(indent^" "^s^" |-> ")); + print_treenode (indent^" ") node + ) + tn.children; + msgnl(str(indent^"} }")) + +let rec print_stack (st : treenode list) = + (match st with + | [] -> msgnl(str "[]") + | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) + + +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + (Tacexpr.TacAtom (Loc.ghost,te))) + | Tacexpr.LtacConstrInterp (c,_) -> + pr_glob_constr_env (Global.env()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s + +let exit_tactic option_start_time_add_total c = + (match option_start_time_add_total with + | Some (start_time, add_total) -> begin + try + let node :: stack' = !stack in + let parent = List.hd stack' in + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time() -. start_time in + parent.entry.local <- parent.entry.local -. diff; + add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; + with Failure("hd") -> (* oops, our stack is invalid *) + encounter_multi_success_backtracking() + end + | None -> () + ) + +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling && is_new_call() then + match call_trace with + | (_, c) :: _ -> + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time() in + Some (start_time, add_total) + ) + | [] -> None + else None)) >>= fun option_start_time_add_total -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic option_start_time_add_total c + | [] -> ())))) + + + +let format_sec x = (Printf.sprintf "%.3fs" x) +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s +let padr n s = str s ++ ws (max 0 (n - utf8_length s)) +let padr_with c n s = + let ulength = utf8_length s in + str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) + +let rec list_iter_is_last f = function + | [] -> () + | [x] -> f true x + | x :: xs -> f false x; list_iter_is_last f xs + +let header() = + msgnl(str" tactic self total calls max"); + msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") + +let rec print_node all_total indent prefix (s,n) = + let e = n.entry in + msgnl( + h 0( + padr_with '-' 40 (prefix ^ s ^ " ") + ++padl 7 (format_ratio (e.local /. all_total)) + ++padl 7 (format_ratio (e.total /. all_total)) + ++padl 8 (string_of_int e.ncalls) + ++padl 10 (format_sec(e.max_total)) + ) + ); + print_table all_total indent false n.children + +and print_table all_total indent first_level table = + let ls = Hashtbl.fold + (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) + table [] in + match ls with + | [(s,n)] when (not first_level) -> + print_node all_total indent (indent^"└") (s,n) + | _ -> + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + list_iter_is_last + (fun is_last -> + print_node + all_total + (indent^if first_level then "" else if is_last then " " else " │") + (indent^if first_level then "─" else if is_last then " └─" else " ├─") + ) + ls + +let print_results() = + let tree = (List.hd !stack).children in + let all_total = -. (List.hd !stack).entry.local in + let global = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + ) + table + in + cumulate tree; + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(str""); + header(); + print_table all_total "" true global; + msgnl(str""); + header(); + print_table all_total "" true tree + (* FOR DEBUGGING *) + (* ; + msgnl(str""); + print_stack(!stack) + *) + +let print_results_tactic tactic = + let tree = (List.hd !stack).children in + let table_tactic = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + ) + table + in + cumulate tree; + let all_total = -. (List.hd !stack).entry.local in + let tactic_total = + Hashtbl.fold + (fun _ node all_total -> node.entry.total +. all_total) + table_tactic 0. in + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(h 0( + str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) + ) + ); + msgnl(str""); + header(); + print_table tactic_total "" true table_tactic + +let reset_profile() = + stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; + encountered_multi_success_backtracking := false + +let do_print_results_at_close () = + if !should_display_profile_at_close + then print_results () + else () + +let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltacprof/profile_ltac.mli b/ltacprof/profile_ltac.mli new file mode 100644 index 000000000..dd750517e --- /dev/null +++ b/ltacprof/profile_ltac.mli @@ -0,0 +1,15 @@ +val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic + +val set_profiling : bool -> unit + +val set_display_profile_at_close : bool -> unit + +val entered_call : unit -> unit + +val print_results : unit -> unit + +val print_results_tactic : string -> unit + +val reset_profile : unit -> unit + +val do_print_results_at_close : unit -> unit diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v new file mode 100644 index 000000000..6b73443d6 --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Start Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Profile. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 7b76514e4..91bb88753 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -49,8 +49,9 @@ let section s = let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; "toplevel"; - "stm"; "grammar"; "config"; "ltac"; "engine"] + "proofs"; "tactics"; "tools"; "ltacprof"; + "toplevel"; "stm"; "grammar"; "config"; + "ltac"; "engine"] let usage () = diff --git a/tools/coqc.ml b/tools/coqc.ml index f957200ab..7210efc4f 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -88,7 +88,7 @@ let parse_args () = (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profileltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 869f6bb93..c2a1bac73 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,6 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true + |"-profileltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f855c096e..fa57d9d21 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,6 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ +\n -profileltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -- cgit v1.2.3 From b9b8e5d4305b7a37b1cae364756834fd60d58fb6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 5 May 2016 14:29:21 -0400 Subject: Add LtacProf documentation --- doc/refman/RefMan-ltac.tex | 98 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 89 insertions(+), 9 deletions(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 12dea9a30..59015742e 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -78,7 +78,7 @@ For instance {\tt try repeat \tac$_1$ || \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.} \end{quote} -is understood as +is understood as \begin{quote} {\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\ {\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).} @@ -174,7 +174,7 @@ is understood as \\ {\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ \\ -\tacarg & ::= & +\tacarg & ::= & {\qualid}\\ & $|$ & {\tt ()} \\ & $|$ & {\tt ltac :} {\atom}\\ @@ -344,7 +344,7 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. expects multiple goals, such as {\tt swap}, would act as if a single goal is focused. - \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} + \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} This variant of local tactic application is paired with a sequence. In this variant, $n$ must be the number of goals @@ -782,7 +782,7 @@ setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}). \begin{coq_example} Ltac f x := match x with - context f [S ?X] => + context f [S ?X] => idtac X; (* To display the evaluation order *) assert (p := eq_refl 1 : X=1); (* To filter the case X=1 *) let x:= context f[O] in assert (x=O) (* To observe the context *) @@ -1026,7 +1026,7 @@ Reset Initial. \index{Tacticals!abstract@{\tt abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as -{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called +{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the current goal and \textit{n} is chosen so that this is a fresh name. Such auxiliary lemma is inlined in the final proof term @@ -1196,6 +1196,86 @@ s: & continue current evaluation without stopping\\ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} + +\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\comindex{Start Profiling}\comindex{Stop Profiling}\comindex{Show Profile}\comindex{Reset Profile}} + +It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug. + +\begin{quote} +{\tt Start Profiling}. +\end{quote} +Enables the profiler and resets the profile + +\begin{quote} +{\tt Stop Profiling}. +\end{quote} +Disables the profiler + +\begin{quote} +{\tt Show Profile}. +\end{quote} +Prints the profile + +\begin{quote} +{\tt Show Profile} {\qstring}. +\end{quote} +Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. + +\begin{quote} +{\tt Reset Profile}. +\end{quote} +Resets the profile, that is, deletes all accumulated information + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Require Import Coq.omega.Omega. + +Ltac mytauto := tauto. +Ltac tac := intros; repeat split; omega || mytauto. + +Notation max x y := (x + (y - x)) (only parsing). +\end{coq_example*} +\begin{coq_example*} +Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, + max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z + /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z + -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A). +Proof. +\end{coq_example*} +\begin{coq_example} + Start Profiling. + tac. +\end{coq_example} +{\let\textit\texttt% use tt mode for the output of ltacprof +\begin{coq_example} + Show Profile. +\end{coq_example} +\begin{coq_example} + Show Profile "omega". +\end{coq_example} +} +\begin{coq_example*} +Abort. +Stop Profiling. +\end{coq_example*} + +\tacindex{start profiling}\tacindex{stop profiling} +The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling. + +\begin{quote} +{\tt start profiling}. +\end{quote} + +\begin{quote} +{\tt stop profiling}. +\end{quote} + +You can also pass the {\tt -profileltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. + +Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. + \endinput \subsection{Permutation on closed lists} @@ -1229,7 +1309,7 @@ Another more complex example is the problem of permutation on closed lists. The aim is to show that a closed list is a permutation of another one. First, we define the permutation predicate as shown on Figure~\ref{permutpred}. - + \begin{figure}[p] \begin{center} \fbox{\begin{minipage}{0.95\textwidth} @@ -1555,7 +1635,7 @@ Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}. \begin{center} \fbox{\begin{minipage}{0.95\textwidth} \begin{coq_example*} -Lemma isos_ex1 : +Lemma isos_ex1 : forall A B:Set, A * unit * B = B * (unit * A). Proof. intros; IsoProve. @@ -1575,7 +1655,7 @@ Qed. \label{isoslem} \end{figure} -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" -%%% End: +%%% End: -- cgit v1.2.3 From 51b32595081d279624c8ec162f9ed686ed660d9b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 11 May 2016 12:30:15 -0400 Subject: Remove a spurious tclFINALLY when not profiling Implement the suggestion of @mattam82 to check whether or not we're profiling before inserting the tclFINALLY. Timing stats: Using: ```bash make clean && git clean -xfd && ./configure -local -with-doc no -coqide no && /usr/bin/time -f "all coq (real: %e, user: %U, sys: %S, mem: %M ko)" make STDTIME='/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 -j4 2>&1 ``` Without LtacProf (4c078b0362542908eb2fe1d63f0d867b339953fd), two runs: ``` real: 147.96, user: 467.93, sys: 30.80, mem: 820468 ko real: 148.04, user: 467.92, sys: 30.49, mem: 820680 ko ``` With LtacProf, two runs: ``` real: 148.32, user: 469.09, sys: 30.57, mem: 818588 ko real: 148.38, user: 469.71, sys: 30.56, mem: 816720 ko ``` Overall overhead on building Coq: about 0.24% Differences in the slowest files: ``` After | File Name | Before || Change --------------------------------------------------------------------------- 7m07.32s | Total | 7m05.16s || +0m02.15s --------------------------------------------------------------------------- 0m44.90s | Numbers/Rational/BigQ/QMake | 0m44.11s || +0m00.78s 0m15.94s | plugins/setoid_ring/Ncring_polynom | 0m15.72s || +0m00.21s 0m14.04s | Numbers/Cyclic/DoubleCyclic/DoubleCyclic | 0m14.05s || -0m00.01s 0m10.65s | Numbers/Cyclic/DoubleCyclic/DoubleSqrt | 0m10.45s || +0m00.20s 0m09.57s | FSets/FMapAVL | 0m09.53s || +0m00.04s 0m09.51s | MSets/MSetRBT | 0m09.45s || +0m00.06s 0m07.00s | Numbers/Cyclic/DoubleCyclic/DoubleDiv | 0m07.05s || -0m00.04s 0m06.88s | Numbers/Cyclic/Int31/Cyclic31 | 0m06.94s || -0m00.06s 0m05.82s | plugins/setoid_ring/Field_theory | 0m05.87s || -0m00.04s 0m05.74s | FSets/FMapFullAVL | 0m05.71s || +0m00.03s 0m05.37s | Reals/Ratan | 0m05.42s || -0m00.04s 0m05.36s | plugins/setoid_ring/Ring_polynom | 0m05.37s || -0m00.00s 0m05.09s | plugins/micromega/EnvRing | 0m04.96s || +0m00.12s ``` --- ltacprof/profile_ltac.ml | 45 +++++++++++++++++++++------------------------ 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml index 889ae77b8..71b96614c 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltacprof/profile_ltac.ml @@ -107,22 +107,17 @@ let string_of_call ck = let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in CString.strip s -let exit_tactic option_start_time_add_total c = - (match option_start_time_add_total with - | Some (start_time, add_total) -> begin - try - let node :: stack' = !stack in - let parent = List.hd stack' in - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time() -. start_time in - parent.entry.local <- parent.entry.local -. diff; - add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; - with Failure("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking() - end - | None -> () - ) +let exit_tactic start_time add_total c = + try + let node :: stack' = !stack in + let parent = List.hd stack' in + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time() -. start_time in + parent.entry.local <- parent.entry.local -. diff; + add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; + with Failure("hd") -> (* oops, our stack is invalid *) + encounter_multi_success_backtracking() let tclFINALLY tac (finally : unit Proofview.tactic) = let open Proofview.Notations in @@ -151,14 +146,16 @@ let do_profile s call_trace tac = Some (start_time, add_total) ) | [] -> None - else None)) >>= fun option_start_time_add_total -> - tclFINALLY - tac - (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> - exit_tactic option_start_time_add_total c - | [] -> ())))) + else None)) >>= function + | Some (start_time, add_total) -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic start_time add_total c + | [] -> ())))) + | None -> tac -- cgit v1.2.3 From 739ead8b2d70f978e31f793234d7a633636742a1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 13 May 2016 17:57:06 -0400 Subject: -profileltac -> -profile-ltac, as per @herbelin https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ``` --- doc/refman/RefMan-ltac.tex | 2 +- tools/coqc.ml | 2 +- toplevel/coqtop.ml | 2 +- toplevel/usage.ml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 59015742e..24f4b2a77 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1272,7 +1272,7 @@ The following two tactics behave like {\tt idtac} but enable and disable the pro {\tt stop profiling}. \end{quote} -You can also pass the {\tt -profileltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. +You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. diff --git a/tools/coqc.ml b/tools/coqc.ml index 7210efc4f..18b2a24fa 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -88,7 +88,7 @@ let parse_args () = (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profileltac" + | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c2a1bac73..de0f73ff4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,7 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true - |"-profileltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio diff --git a/toplevel/usage.ml b/toplevel/usage.ml index fa57d9d21..5359a288a 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -77,7 +77,7 @@ let print_usage_channel co command = \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ \n -time display the time taken by each command\ -\n -profileltac display the time taken by each (sub)tactic\ +\n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -- cgit v1.2.3 From 13e11b6aec1444071dc3787da15e89a6bc0eb0dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 14 May 2016 23:09:20 -0400 Subject: Synchronize the profiler state with the document This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected. --- doc/refman/RefMan-ltac.tex | 2 +- ltac/profile_ltac_tactics.ml4 | 2 +- ltacprof/profile_ltac.ml | 19 +++++++++++++++++-- 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 24f4b2a77..608793d04 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1204,7 +1204,7 @@ It is possible to measure the time spent in invocations of primitive tactics as \begin{quote} {\tt Start Profiling}. \end{quote} -Enables the profiler and resets the profile +Enables the profiler \begin{quote} {\tt Stop Profiling}. diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 0c4e0b075..ce00c2920 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -19,7 +19,7 @@ END;; VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF - [ "Start" "Profiling" ] -> [ reset_profile(); set_profiling true ] + [ "Start" "Profiling" ] -> [ set_profiling true ] END VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml index 71b96614c..6ae07689d 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltacprof/profile_ltac.ml @@ -3,7 +3,8 @@ open Printer open Util -let is_profiling = ref false +(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. *) +let is_profiling = Summary.ref false ~name:"is-profiling-ltac" let set_profiling b = is_profiling := b let should_display_profile_at_close = ref false @@ -40,7 +41,21 @@ let add_entry e add_total {total; local; ncalls; max_total} = if add_total then e.max_total <- max e.max_total max_total type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} -let stack = ref [{entry=empty_entry(); children=Hashtbl.create 20}] + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) +let deepcopy_entry {total; local; ncalls; max_total} = + {total; local; ncalls; max_total} + +let rec deepcopy_treenode {entry; children} = + {entry = deepcopy_entry entry; + children = + (let children' = Hashtbl.create (Hashtbl.length children) in + Hashtbl.iter + (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) + children; + children')} + +let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" let on_stack = Hashtbl.create 5 -- cgit v1.2.3 From 9b0376731de3b71a7461747d12763becca1e5399 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 15 May 2016 16:05:11 -0400 Subject: Make Ltac Profiling an setting --- doc/refman/RefMan-ltac.tex | 26 +++++++++++++------------- ltac/profile_ltac_tactics.ml4 | 36 ++++++++++++++++++------------------ ltacprof/profile_ltac.ml | 6 ++++-- ltacprof/profile_ltac.mli | 2 ++ test-suite/success/ltacprof.v | 4 ++-- 5 files changed, 39 insertions(+), 35 deletions(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 608793d04..ffcb37134 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1197,27 +1197,27 @@ r $n$: & advance $n$ steps further\\ r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\ \end{tabular} -\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\comindex{Start Profiling}\comindex{Stop Profiling}\comindex{Show Profile}\comindex{Reset Profile}} +\subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}} It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug. \begin{quote} -{\tt Start Profiling}. +{\tt Set Ltac Profiling}. \end{quote} Enables the profiler \begin{quote} -{\tt Stop Profiling}. +{\tt Unset Ltac Profiling}. \end{quote} Disables the profiler \begin{quote} -{\tt Show Profile}. +{\tt Show Ltac Profile}. \end{quote} Prints the profile \begin{quote} -{\tt Show Profile} {\qstring}. +{\tt Show Ltac Profile} {\qstring}. \end{quote} Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. @@ -1245,34 +1245,34 @@ Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, Proof. \end{coq_example*} \begin{coq_example} - Start Profiling. + Set Ltac Profiling. tac. \end{coq_example} {\let\textit\texttt% use tt mode for the output of ltacprof \begin{coq_example} - Show Profile. + Show Ltac Profile. \end{coq_example} \begin{coq_example} - Show Profile "omega". + Show Ltac Profile "omega". \end{coq_example} } \begin{coq_example*} Abort. -Stop Profiling. +Unset Ltac Profiling. \end{coq_example*} -\tacindex{start profiling}\tacindex{stop profiling} +\tacindex{start ltac profiling}\tacindex{stop ltac profiling} The following two tactics behave like {\tt idtac} but enable and disable the profiling. They allow you to exclude parts of a proof script from profiling. \begin{quote} -{\tt start profiling}. +{\tt start ltac profiling}. \end{quote} \begin{quote} -{\tt stop profiling}. +{\tt stop ltac profiling}. \end{quote} -You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Start Profiling} at the beginning of each document, and a {\tt Show Profile} at the end. +You can also pass the {\tt -profile-ltac} command line option to {\tt coqc}, which performs a {\tt Set Ltac Profiling} at the beginning of each document, and a {\tt Show Ltac Profile} at the end. Note that the profiler currently does not handle backtracking into multi-success tactics, and issues a warning to this effect in many cases when such backtracking occurs. diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index ce00c2920..b83ab8c52 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -9,32 +9,32 @@ let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) -TACTIC EXTEND start_profiling - | [ "start" "profiling" ] -> [ tclSET_PROFILING true ] +TACTIC EXTEND start_ltac_profiling + | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END TACTIC EXTEND stop_profiling - | [ "stop" "profiling" ] -> [ tclSET_PROFILING false ] + | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END;; - -VERNAC COMMAND EXTEND StartProfiling CLASSIFIED AS SIDEFF - [ "Start" "Profiling" ] -> [ set_profiling true ] -END - -VERNAC COMMAND EXTEND StopProfiling CLASSIFIED AS SIDEFF - [ "Stop" "Profiling" ] -> [ set_profiling false ] - END - -VERNAC COMMAND EXTEND ResetProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Profile" ] -> [ reset_profile() ] +let _ = + Goptions.declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } + +VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] END -VERNAC COMMAND EXTEND ShowProfile CLASSIFIED AS QUERY - [ "Show" "Profile" ] -> [ print_results() ] +VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY + [ "Show" "Ltac" "Profile" ] -> [ print_results() ] END -VERNAC COMMAND EXTEND ShowProfileTactic CLASSIFIED AS QUERY - [ "Show" "Profile" string(s) ] -> [ print_results_tactic s ] +VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY + [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] END diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml index 6ae07689d..97d74ad80 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltacprof/profile_ltac.ml @@ -3,9 +3,11 @@ open Printer open Util -(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. *) -let is_profiling = Summary.ref false ~name:"is-profiling-ltac" +(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) +let is_profiling = ref false + let set_profiling b = is_profiling := b +let get_profiling () = !is_profiling let should_display_profile_at_close = ref false let set_display_profile_at_close b = should_display_profile_at_close := b diff --git a/ltacprof/profile_ltac.mli b/ltacprof/profile_ltac.mli index dd750517e..65c067e86 100644 --- a/ltacprof/profile_ltac.mli +++ b/ltacprof/profile_ltac.mli @@ -2,6 +2,8 @@ val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.ta val set_profiling : bool -> unit +val get_profiling : unit -> bool + val set_display_profile_at_close : bool -> unit val entered_call : unit -> unit diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index 6b73443d6..ae11358ed 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -1,8 +1,8 @@ (** Some LtacProf tests *) -Start Profiling. +Set Ltac Profiling. Ltac multi := (idtac + idtac). Goal True. try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. -Show Profile. +Show Ltac Profile. -- cgit v1.2.3 From 6b78930640a03260f98fa90411070c6dbad8d266 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 20 May 2016 13:45:08 -0400 Subject: Improve a comment in the test suite --- test-suite/success/ltacprof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index ae11358ed..d5552695c 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -3,6 +3,6 @@ Set Ltac Profiling. Ltac multi := (idtac + idtac). Goal True. - try (multi; fail). (* Anomaly: Uncaught exception Failure("hd"). Please report. *) + try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. Show Ltac Profile. -- cgit v1.2.3 From 45de05d0ea9740f14c58dfd67436ddbea03c6a49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 13 Jun 2016 23:50:04 +0200 Subject: Revert "Strip some trailing spaces" This reverts commit 45748e4efae8630cc13b0199dfcc9803341e8cd8. --- Makefile.build | 22 +++++++++++----------- Makefile.common | 14 +++++++------- lib/pp.ml | 2 +- ltac/tacinterp.ml | 16 ++++++++-------- 4 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Makefile.build b/Makefile.build index c6fef10b6..4f3077e5d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -78,8 +78,8 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile -# The SHOW and HIDE variables control whether make will echo complete commands -# or only abbreviated versions. +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make SHOW := $(if $(VERBOSE),@true "",@echo "") @@ -231,7 +231,7 @@ grammar/grammar.cma : $(GRAMCMO) $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl test.mlp -o test.ml $(HIDE)$(GRAMC) test.ml -o test-grammar @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ ## Support of Camlp5 and Camlp5 @@ -283,7 +283,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -thread -o $@ $(STRIP) $@ $(CODESIGN) $@ @@ -293,7 +293,7 @@ $(COQTOPEXE): $(COQTOPBYTE) endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) - $(SHOW)'COQMKTOP -o $@' + $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) @@ -896,7 +896,7 @@ install-emacs: install-latex: $(MKDIR) $(FULLCOQDOCDIR) - $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) + $(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) # -$(UPDATETEX) ########################################################################### @@ -968,7 +968,7 @@ dev/printers.cma: dev/printers.mllib $(SHOW)'Testing $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -o test-printer @rm -f test-printer - $(SHOW)'OCAMLC -a $@' + $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -thread $(SYSCMA) $(P4CMA) $(filter-out %.mllib, $^) -linkall -a -o $@ ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here @@ -1107,7 +1107,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) $(SHOW)'COQC $<' - $(HIDE)rm -f $*.glob + $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' @@ -1187,7 +1187,7 @@ otags: Makefile Makefile.build Makefile.common config/Makefile : ; -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/Makefile.common b/Makefile.common index 37db66be3..e2f67226b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,7 +12,7 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) +COQMKTOP:=bin/coqmktop$(EXE) COQC:=bin/coqc$(EXE) @@ -35,7 +35,7 @@ else endif INSTALLBIN:=install -INSTALLLIB:=install -m 644 +INSTALLLIB:=install -m 644 INSTALLSH:=./install.sh MKDIR:=install -d @@ -119,7 +119,7 @@ HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): COQTEXOPTS:=-boot -n 72 -sl -small -DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex +DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex RefMan-ext.v.tex \ @@ -149,7 +149,7 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) ########################################################################### -# Object and Source files +# Object and Source files ########################################################################### COQRUN := coqrun @@ -394,7 +394,7 @@ GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) -# For emacs: -# Local Variables: -# mode: makefile +# For emacs: +# Local Variables: +# mode: makefile # End: diff --git a/lib/pp.ml b/lib/pp.ml index 5d7c71635..868787864 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -44,7 +44,7 @@ end module Tag : sig - type t + type t type 'a key val create : string -> 'a key val inj : 'a -> 'a key -> t diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4f7c02968..ab61c8abb 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -995,7 +995,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_map (interp_binding ist env) sigma l in @@ -1171,7 +1171,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1644,7 +1644,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacIntroPattern l) (* spiwack: print uninterpreted, not sure if it is the @@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let l = List.map (fun (k,c) -> let loc, f = interp_open_constr_with_bindings_loc ist c in - (k,(loc,f))) cb + (k,(loc,f))) cb in let sigma,tac = match cl with | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l @@ -1672,7 +1672,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | TacElim (ev,(keep,cb),cbo) -> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = project gl in + let sigma = project gl in let sigma, cb = interp_constr_with_bindings ist env sigma cb in let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in let named_tac = @@ -1726,7 +1726,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = + let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in @@ -1836,7 +1836,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let sigma = Sigma.to_evar_map sigma in @@ -1862,7 +1862,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> - Id.Map.add id (Value.of_constr c) lfun) + Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in -- cgit v1.2.3 From 236627cdf081e51fce3bc54fdee4e40d4f6ca85e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 00:08:14 +0200 Subject: Moving UTF-8 related functions to Unicode module. --- lib/pp.ml | 32 ---------------------- lib/pp.mli | 3 --- lib/unicode.ml | 70 ++++++++++++++++++++++++++++++++++++++++++++++++ lib/unicode.mli | 6 +++++ ltacprof/profile_ltac.ml | 1 + 5 files changed, 77 insertions(+), 35 deletions(-) diff --git a/lib/pp.ml b/lib/pp.ml index 868787864..d07f01b90 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -168,38 +168,6 @@ let utf8_length s = done ; !cnt -(* Variant of String.sub for UTF8 character positions *) -let utf8_sub s start_u len_u = - let len_b = String.length s - and end_u = start_u + len_u - and cnt = ref 0 - and nc = ref 0 - and p = ref 0 in - let start_b = ref len_b in - while !p < len_b && !cnt < end_u do - if !cnt <= start_u then start_b := !p ; - begin - match s.[!p] with - | '\000'..'\127' -> nc := 0 (* ascii char *) - | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) - | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) - | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) - | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) - end ; - incr p ; - while !p < len_b && !nc > 0 do - match s.[!p] with - | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc - | _ (* not a continuation byte *) -> nc := 0 - done ; - incr cnt - done ; - let end_b = !p in - String.sub s !start_b (end_b - !start_b) - (* formatting commands *) let str s = Glue.atom(Ppcmd_print (Str_def s)) let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i))) diff --git a/lib/pp.mli b/lib/pp.mli index 56b82e448..a18744c37 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -100,9 +100,6 @@ val close_tag : unit -> std_ppcmds val string_of_ppcmds : std_ppcmds -> string -val utf8_length : string -> int -val utf8_sub : string -> int -> int -> string - (** {6 Printing combinators} *) val pr_comma : unit -> std_ppcmds diff --git a/lib/unicode.ml b/lib/unicode.ml index 7aa8d9d51..dc852d981 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -261,3 +261,73 @@ let ascii_of_ident s = (Buffer.add_char out s.[!i]; incr i) done; Buffer.contents out + +(* Compute length of an UTF-8 encoded string + Rem 1 : utf8_length <= String.length (equal if pure ascii) + Rem 2 : if used for an iso8859_1 encoded string, the result is + wrong in very rare cases. Such a wrong case corresponds to any + sequence of a character in range 192..253 immediately followed by a + character in range 128..191 (typical case in french is "déçu" which + is counted 3 instead of 4); then no real harm to use always + utf8_length even if using an iso8859_1 encoding *) + +(** FIXME: duplicate code with Pp *) + +let utf8_length s = + let len = String.length s + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + while !p < len do + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + !cnt + +(* Variant of String.sub for UTF8 character positions *) +let utf8_sub s start_u len_u = + let len_b = String.length s + and end_u = start_u + len_u + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + let start_b = ref len_b in + while !p < len_b && !cnt < end_u do + if !cnt <= start_u then start_b := !p ; + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len_b && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + let end_b = !p in + String.sub s !start_b (end_b - !start_b) diff --git a/lib/unicode.mli b/lib/unicode.mli index aaf455dec..1f8bd44ee 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -40,3 +40,9 @@ val ascii_of_ident : string -> string (** Validate an UTF-8 string *) val is_utf8 : string -> bool + +(** Return the length of a valid UTF-8 string. *) +val utf8_length : string -> int + +(** Variant of {!String.sub} for UTF-8 strings. *) +val utf8_sub : string -> int -> int -> string diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml index 97d74ad80..41bde12b1 100644 --- a/ltacprof/profile_ltac.ml +++ b/ltacprof/profile_ltac.ml @@ -1,3 +1,4 @@ +open Unicode open Pp open Printer open Util -- cgit v1.2.3 From e4d5bbeecb4c5a4eca82700ba3946d9fd174e215 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 00:12:44 +0200 Subject: Moving back Ltac profiling to the Ltac folder. --- Makefile.build | 2 +- Makefile.common | 5 +- lib/flags.ml | 1 + lib/flags.mli | 2 + ltac/ltac.mllib | 1 + ltac/profile_ltac.ml | 304 ++++++++++++++++++++++++++++++++++++++++++ ltac/profile_ltac.mli | 15 +++ ltac/profile_ltac_tactics.ml4 | 9 -- ltacprof/ltacprof.mllib | 1 - ltacprof/profile_ltac.ml | 301 ----------------------------------------- ltacprof/profile_ltac.mli | 17 --- toplevel/coqtop.ml | 2 +- 12 files changed, 327 insertions(+), 333 deletions(-) create mode 100644 ltac/profile_ltac.ml create mode 100644 ltac/profile_ltac.mli delete mode 100644 ltacprof/ltacprof.mllib delete mode 100644 ltacprof/profile_ltac.ml delete mode 100644 ltacprof/profile_ltac.mli diff --git a/Makefile.build b/Makefile.build index 4f3077e5d..fc92507e6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -570,7 +570,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac ltacprof +.PHONY: engine highparsing stm toplevel ltac lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma diff --git a/Makefile.common b/Makefile.common index e2f67226b..86a7ea847 100644 --- a/Makefile.common +++ b/Makefile.common @@ -62,7 +62,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp stm ltacprof\ + proofs tactics pretyping interp stm \ toplevel parsing printing intf engine ltac PLUGINS:=\ @@ -167,8 +167,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma ltacprof/ltacprof.cma toplevel/toplevel.cma \ - parsing/highparsing.cma ltac/ltac.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738c..4983e4082 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -220,6 +220,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dc..e13655e4a 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -143,6 +143,8 @@ val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) +val profile_ltac : bool ref + (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index d8854e6e7..65ed114cf 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -3,6 +3,7 @@ Tacenv Tactic_debug Tacintern Tacentries +Profile_ltac Tacinterp Evar_tactics Tactic_option diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml new file mode 100644 index 000000000..4f982f1eb --- /dev/null +++ b/ltac/profile_ltac.ml @@ -0,0 +1,304 @@ +open Unicode +open Pp +open Printer +open Util + + +(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) +let is_profiling = Flags.profile_ltac + +let set_profiling b = is_profiling := b +let get_profiling () = !is_profiling + +let new_call = ref false +let entered_call() = new_call := true +let is_new_call() = let b = !new_call in new_call := false; b + +(** Local versions of the old Pp.msgnl *) +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + +(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) +let encountered_multi_success_backtracking = ref false +let warn_encountered_multi_success_backtracking() = + if !encountered_multi_success_backtracking + then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") +let encounter_multi_success_backtracking() = + if not !encountered_multi_success_backtracking + then begin + encountered_multi_success_backtracking := true; + warn_encountered_multi_success_backtracking() + end + + +type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} +let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} +let add_entry e add_total {total; local; ncalls; max_total} = + if add_total then e.total <- e.total +. total; + e.local <- e.local +. local; + e.ncalls <- e.ncalls + ncalls; + if add_total then e.max_total <- max e.max_total max_total + +type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} + +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) +let deepcopy_entry {total; local; ncalls; max_total} = + {total; local; ncalls; max_total} + +let rec deepcopy_treenode {entry; children} = + {entry = deepcopy_entry entry; + children = + (let children' = Hashtbl.create (Hashtbl.length children) in + Hashtbl.iter + (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) + children; + children')} + +let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" + +let on_stack = Hashtbl.create 5 + +let get_node c table = + try Hashtbl.find table c + with Not_found -> + let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in + Hashtbl.add table c new_node; + new_node + +let rec add_node node node' = + add_entry node.entry true node'.entry; + Hashtbl.iter + (fun s node' -> add_node (get_node s node.children) node') + node'.children + +let time() = + let times = Unix.times() in + times.Unix.tms_utime +. times.Unix.tms_stime + +let rec print_treenode indent (tn : treenode) = + msgnl(str(indent^"{ entry = {")); + Feedback.msg_notice(str(indent^"total = ")); + msgnl(str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice(str(indent^"local = ")); + msgnl(str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice(str(indent^"ncalls = ")); + msgnl(str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice(str(indent^"max_total = ")); + msgnl(str (indent^(string_of_float tn.entry.max_total))); + msgnl(str(indent^"}")); + msgnl(str(indent^"children = {")); + Hashtbl.iter + (fun s node -> + msgnl(str(indent^" "^s^" |-> ")); + print_treenode (indent^" ") node + ) + tn.children; + msgnl(str(indent^"} }")) + +let rec print_stack (st : treenode list) = + (match st with + | [] -> msgnl(str "[]") + | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) + + +let string_of_call ck = + let s = + string_of_ppcmds + (match ck with + | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst + | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id + | Tacexpr.LtacAtomCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + (Tacexpr.TacAtom (Loc.ghost,te))) + | Tacexpr.LtacConstrInterp (c,_) -> + pr_glob_constr_env (Global.env()) c + | Tacexpr.LtacMLCall te -> + (Pptactic.pr_glob_tactic (Global.env()) + te) + ) in + for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; + let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in + CString.strip s + +let exit_tactic start_time add_total c = + try + let node :: stack' = !stack in + let parent = List.hd stack' in + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time() -. start_time in + parent.entry.local <- parent.entry.local -. diff; + add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; + with Failure("hd") -> (* oops, our stack is invalid *) + encounter_multi_success_backtracking() + +let tclFINALLY tac (finally : unit Proofview.tactic) = + let open Proofview.Notations in + Proofview.tclIFCATCH + tac + (fun v -> finally <*> Proofview.tclUNIT v) + (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) + +let do_profile s call_trace tac = + let open Proofview.Notations in + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + if !is_profiling && is_new_call() then + match call_trace with + | (_, c) :: _ -> + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time() in + Some (start_time, add_total) + ) + | [] -> None + else None)) >>= function + | Some (start_time, add_total) -> + tclFINALLY + tac + (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> + (match call_trace with + | (_, c) :: _ -> + exit_tactic start_time add_total c + | [] -> ())))) + | None -> tac + + + +let format_sec x = (Printf.sprintf "%.3fs" x) +let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) +let padl n s = ws (max 0 (n - utf8_length s)) ++ str s +let padr n s = str s ++ ws (max 0 (n - utf8_length s)) +let padr_with c n s = + let ulength = utf8_length s in + str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) + +let rec list_iter_is_last f = function + | [] -> () + | [x] -> f true x + | x :: xs -> f false x; list_iter_is_last f xs + +let header() = + msgnl(str" tactic self total calls max"); + msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") + +let rec print_node all_total indent prefix (s,n) = + let e = n.entry in + msgnl( + h 0( + padr_with '-' 40 (prefix ^ s ^ " ") + ++padl 7 (format_ratio (e.local /. all_total)) + ++padl 7 (format_ratio (e.total /. all_total)) + ++padl 8 (string_of_int e.ncalls) + ++padl 10 (format_sec(e.max_total)) + ) + ); + print_table all_total indent false n.children + +and print_table all_total indent first_level table = + let ls = Hashtbl.fold + (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) + table [] in + match ls with + | [(s,n)] when (not first_level) -> + print_node all_total indent (indent^"└") (s,n) + | _ -> + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + list_iter_is_last + (fun is_last -> + print_node + all_total + (indent^if first_level then "" else if is_last then " " else " │") + (indent^if first_level then "─" else if is_last then " └─" else " ├─") + ) + ls + +let print_results() = + let tree = (List.hd !stack).children in + let all_total = -. (List.hd !stack).entry.local in + let global = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + ) + table + in + cumulate tree; + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(str""); + header(); + print_table all_total "" true global; + msgnl(str""); + header(); + print_table all_total "" true tree + (* FOR DEBUGGING *) + (* ; + msgnl(str""); + print_stack(!stack) + *) + +let print_results_tactic tactic = + let tree = (List.hd !stack).children in + let table_tactic = Hashtbl.create 20 in + let rec cumulate table = + Hashtbl.iter + (fun s node -> + if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + ) + table + in + cumulate tree; + let all_total = -. (List.hd !stack).entry.local in + let tactic_total = + Hashtbl.fold + (fun _ node all_total -> node.entry.total +. all_total) + table_tactic 0. in + warn_encountered_multi_success_backtracking(); + msgnl(str""); + msgnl(h 0( + str"total time: "++padl 11 (format_sec(all_total)) + ) + ); + msgnl(h 0( + str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) + ) + ); + msgnl(str""); + header(); + print_table tactic_total "" true table_tactic + +let reset_profile() = + stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; + encountered_multi_success_backtracking := false + +let do_print_results_at_close () = if get_profiling () then print_results () + +let _ = Declaremods.append_end_library_hook do_print_results_at_close + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Ltac Profiling"; + optkey = ["Ltac"; "Profiling"]; + optread = get_profiling; + optwrite = set_profiling } diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli new file mode 100644 index 000000000..0029b8b55 --- /dev/null +++ b/ltac/profile_ltac.mli @@ -0,0 +1,15 @@ +val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic + +val set_profiling : bool -> unit + +val get_profiling : unit -> bool + +val entered_call : unit -> unit + +val print_results : unit -> unit + +val print_results_tactic : string -> unit + +val reset_profile : unit -> unit + +val do_print_results_at_close : unit -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index b83ab8c52..8889bd13c 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -17,15 +17,6 @@ TACTIC EXTEND stop_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END;; -let _ = - Goptions.declare_bool_option - { optsync = true; - optdepr = false; - optname = "Ltac Profiling"; - optkey = ["Ltac"; "Profiling"]; - optread = get_profiling; - optwrite = set_profiling } - VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] END diff --git a/ltacprof/ltacprof.mllib b/ltacprof/ltacprof.mllib deleted file mode 100644 index 383e5d285..000000000 --- a/ltacprof/ltacprof.mllib +++ /dev/null @@ -1 +0,0 @@ -Profile_ltac diff --git a/ltacprof/profile_ltac.ml b/ltacprof/profile_ltac.ml deleted file mode 100644 index 41bde12b1..000000000 --- a/ltacprof/profile_ltac.ml +++ /dev/null @@ -1,301 +0,0 @@ -open Unicode -open Pp -open Printer -open Util - - -(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) -let is_profiling = ref false - -let set_profiling b = is_profiling := b -let get_profiling () = !is_profiling - -let should_display_profile_at_close = ref false -let set_display_profile_at_close b = should_display_profile_at_close := b - - -let new_call = ref false -let entered_call() = new_call := true -let is_new_call() = let b = !new_call in new_call := false; b - -(** Local versions of the old Pp.msgnl *) -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !Pp_control.std_ft strm - -(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) -let encountered_multi_success_backtracking = ref false -let warn_encountered_multi_success_backtracking() = - if !encountered_multi_success_backtracking - then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") -let encounter_multi_success_backtracking() = - if not !encountered_multi_success_backtracking - then begin - encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking() - end - - -type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} -let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} -let add_entry e add_total {total; local; ncalls; max_total} = - if add_total then e.total <- e.total +. total; - e.local <- e.local +. local; - e.ncalls <- e.ncalls + ncalls; - if add_total then e.max_total <- max e.max_total max_total - -type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} - -(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) -let deepcopy_entry {total; local; ncalls; max_total} = - {total; local; ncalls; max_total} - -let rec deepcopy_treenode {entry; children} = - {entry = deepcopy_entry entry; - children = - (let children' = Hashtbl.create (Hashtbl.length children) in - Hashtbl.iter - (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) - children; - children')} - -let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" - -let on_stack = Hashtbl.create 5 - -let get_node c table = - try Hashtbl.find table c - with Not_found -> - let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in - Hashtbl.add table c new_node; - new_node - -let rec add_node node node' = - add_entry node.entry true node'.entry; - Hashtbl.iter - (fun s node' -> add_node (get_node s node.children) node') - node'.children - -let time() = - let times = Unix.times() in - times.Unix.tms_utime +. times.Unix.tms_stime - -let rec print_treenode indent (tn : treenode) = - msgnl(str(indent^"{ entry = {")); - Feedback.msg_notice(str(indent^"total = ")); - msgnl(str (indent^(string_of_float (tn.entry.total)))); - Feedback.msg_notice(str(indent^"local = ")); - msgnl(str (indent^(string_of_float tn.entry.local))); - Feedback.msg_notice(str(indent^"ncalls = ")); - msgnl(str (indent^(string_of_int tn.entry.ncalls))); - Feedback.msg_notice(str(indent^"max_total = ")); - msgnl(str (indent^(string_of_float tn.entry.max_total))); - msgnl(str(indent^"}")); - msgnl(str(indent^"children = {")); - Hashtbl.iter - (fun s node -> - msgnl(str(indent^" "^s^" |-> ")); - print_treenode (indent^" ") node - ) - tn.children; - msgnl(str(indent^"} }")) - -let rec print_stack (st : treenode list) = - (match st with - | [] -> msgnl(str "[]") - | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) - - -let string_of_call ck = - let s = - string_of_ppcmds - (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s - | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id - | Tacexpr.LtacAtomCall te -> - (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) - | Tacexpr.LtacConstrInterp (c,_) -> - pr_glob_constr_env (Global.env()) c - | Tacexpr.LtacMLCall te -> - (Pptactic.pr_glob_tactic (Global.env()) - te) - ) in - for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; - let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in - CString.strip s - -let exit_tactic start_time add_total c = - try - let node :: stack' = !stack in - let parent = List.hd stack' in - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time() -. start_time in - parent.entry.local <- parent.entry.local -. diff; - add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; - with Failure("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking() - -let tclFINALLY tac (finally : unit Proofview.tactic) = - let open Proofview.Notations in - Proofview.tclIFCATCH - tac - (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) - -let do_profile s call_trace tac = - let open Proofview.Notations in - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling && is_new_call() then - match call_trace with - | (_, c) :: _ -> - let s = string_of_call c in - let parent = List.hd !stack in - let node, add_total = try Hashtbl.find on_stack s, false - with Not_found -> - let node = get_node s parent.children in - Hashtbl.add on_stack s node; - node, true - in - if not add_total && node = List.hd !stack then None else ( - stack := node :: !stack; - let start_time = time() in - Some (start_time, add_total) - ) - | [] -> None - else None)) >>= function - | Some (start_time, add_total) -> - tclFINALLY - tac - (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> - exit_tactic start_time add_total c - | [] -> ())))) - | None -> tac - - - -let format_sec x = (Printf.sprintf "%.3fs" x) -let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x)) -let padl n s = ws (max 0 (n - utf8_length s)) ++ str s -let padr n s = str s ++ ws (max 0 (n - utf8_length s)) -let padr_with c n s = - let ulength = utf8_length s in - str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) - -let rec list_iter_is_last f = function - | [] -> () - | [x] -> f true x - | x :: xs -> f false x; list_iter_is_last f xs - -let header() = - msgnl(str" tactic self total calls max"); - msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") - -let rec print_node all_total indent prefix (s,n) = - let e = n.entry in - msgnl( - h 0( - padr_with '-' 40 (prefix ^ s ^ " ") - ++padl 7 (format_ratio (e.local /. all_total)) - ++padl 7 (format_ratio (e.total /. all_total)) - ++padl 8 (string_of_int e.ncalls) - ++padl 10 (format_sec(e.max_total)) - ) - ); - print_table all_total indent false n.children - -and print_table all_total indent first_level table = - let ls = Hashtbl.fold - (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) - table [] in - match ls with - | [(s,n)] when (not first_level) -> - print_node all_total indent (indent^"└") (s,n) - | _ -> - let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in - list_iter_is_last - (fun is_last -> - print_node - all_total - (indent^if first_level then "" else if is_last then " " else " │") - (indent^if first_level then "─" else if is_last then " └─" else " ├─") - ) - ls - -let print_results() = - let tree = (List.hd !stack).children in - let all_total = -. (List.hd !stack).entry.local in - let global = Hashtbl.create 20 in - let rec cumulate table = - Hashtbl.iter - (fun s node -> - let node' = get_node s global in - add_entry node'.entry true node.entry; - cumulate node.children - ) - table - in - cumulate tree; - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) - ) - ); - msgnl(str""); - header(); - print_table all_total "" true global; - msgnl(str""); - header(); - print_table all_total "" true tree - (* FOR DEBUGGING *) - (* ; - msgnl(str""); - print_stack(!stack) - *) - -let print_results_tactic tactic = - let tree = (List.hd !stack).children in - let table_tactic = Hashtbl.create 20 in - let rec cumulate table = - Hashtbl.iter - (fun s node -> - if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic - then add_node (get_node s table_tactic) node - else cumulate node.children - ) - table - in - cumulate tree; - let all_total = -. (List.hd !stack).entry.local in - let tactic_total = - Hashtbl.fold - (fun _ node all_total -> node.entry.total +. all_total) - table_tactic 0. in - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) - ) - ); - msgnl(h 0( - str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) - ) - ); - msgnl(str""); - header(); - print_table tactic_total "" true table_tactic - -let reset_profile() = - stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; - encountered_multi_success_backtracking := false - -let do_print_results_at_close () = - if !should_display_profile_at_close - then print_results () - else () - -let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltacprof/profile_ltac.mli b/ltacprof/profile_ltac.mli deleted file mode 100644 index 65c067e86..000000000 --- a/ltacprof/profile_ltac.mli +++ /dev/null @@ -1,17 +0,0 @@ -val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic - -val set_profiling : bool -> unit - -val get_profiling : unit -> bool - -val set_display_profile_at_close : bool -> unit - -val entered_call : unit -> unit - -val print_results : unit -> unit - -val print_results_tactic : string -> unit - -val reset_profile : unit -> unit - -val do_print_results_at_close : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index de0f73ff4..aab20650a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -549,7 +549,7 @@ let parse_args arglist = else native_compiler := true |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true - |"-profile-ltac" -> Profile_ltac.set_profiling true; Profile_ltac.set_display_profile_at_close true + |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio -- cgit v1.2.3 From 17a9fe474427291797e37183956b2bc5c6434ec6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 00:30:09 +0200 Subject: Adding Coq headers. --- ltac/profile_ltac.ml | 8 ++++++++ ltac/profile_ltac.mli | 8 ++++++++ ltac/profile_ltac_tactics.ml4 | 8 ++++++++ 3 files changed, 24 insertions(+) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 4f982f1eb..890b449a7 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 8889bd13c..a4ba5eab4 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Date: Tue, 14 Jun 2016 00:33:08 +0200 Subject: Better coding style (syntax). --- ltac/profile_ltac.ml | 289 ++++++++++++++++++++++-------------------- ltac/profile_ltac.mli | 2 + ltac/profile_ltac_tactics.ml4 | 18 +-- 3 files changed, 164 insertions(+), 145 deletions(-) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 890b449a7..b008d389f 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -11,65 +11,88 @@ open Pp open Printer open Util - -(** [is_profiling] and the profiling info ([stack]) should be synchronized with the document; the rest of the ref cells are either local to individual tactic invocations, or global flags, and need not be synchronized, since no document-level backtracking happens within tactics. We synchronize is_profiling via an option. *) +(** [is_profiling] and the profiling info ([stack]) should be synchronized with + the document; the rest of the ref cells are either local to individual + tactic invocations, or global flags, and need not be synchronized, since no + document-level backtracking happens within tactics. We synchronize + is_profiling via an option. *) let is_profiling = Flags.profile_ltac let set_profiling b = is_profiling := b let get_profiling () = !is_profiling let new_call = ref false -let entered_call() = new_call := true -let is_new_call() = let b = !new_call in new_call := false; b +let entered_call () = new_call := true +let is_new_call () = let b = !new_call in new_call := false; b (** Local versions of the old Pp.msgnl *) let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) let msgnl strm = msgnl_with !Pp_control.std_ft strm -(** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and possibly expensive, so instead we currently just emit a warning that profiling results will be off. *) +(** LtacProf cannot yet handle backtracking into multi-success tactics. + To properly support this, we'd have to somehow recreate our location in the + call-stack, and stop/restart the intervening timers. This is tricky and + possibly expensive, so instead we currently just emit a warning that + profiling results will be off. *) let encountered_multi_success_backtracking = ref false -let warn_encountered_multi_success_backtracking() = - if !encountered_multi_success_backtracking - then Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking into multi-success tactics; profiling results may be wildly inaccurate.") -let encounter_multi_success_backtracking() = + +let warn_encountered_multi_success_backtracking () = + if !encountered_multi_success_backtracking then + Feedback.msg_warning (str "Ltac Profiler cannot yet handle backtracking \ + into multi-success tactics; profiling results may be wildly inaccurate.") + +let encounter_multi_success_backtracking () = if not !encountered_multi_success_backtracking then begin encountered_multi_success_backtracking := true; - warn_encountered_multi_success_backtracking() + warn_encountered_multi_success_backtracking () end +type entry = { + mutable total : float; + mutable local : float; + mutable ncalls : int; + mutable max_total : float +} -type entry = {mutable total : float; mutable local : float; mutable ncalls : int; mutable max_total : float} -let empty_entry() = {total = 0.; local = 0.; ncalls = 0; max_total = 0.} -let add_entry e add_total {total; local; ncalls; max_total} = +let empty_entry () = { total = 0.; local = 0.; ncalls = 0; max_total = 0. } + +let add_entry e add_total { total; local; ncalls; max_total } = if add_total then e.total <- e.total +. total; e.local <- e.local +. local; e.ncalls <- e.ncalls + ncalls; if add_total then e.max_total <- max e.max_total max_total -type treenode = {entry : entry; children : (string, treenode) Hashtbl.t} +type treenode = { + entry : entry; + children : (string, treenode) Hashtbl.t +} + +let empty_treenode n = { entry = empty_entry (); children = Hashtbl.create n } -(** Tobias Tebbi wrote some tricky code involving mutation. Rather than rewriting it in a functional style, we simply freeze the state when we need to by issuing a deep copy of the profiling data. *) -let deepcopy_entry {total; local; ncalls; max_total} = - {total; local; ncalls; max_total} +(** Tobias Tebbi wrote some tricky code involving mutation. Rather than + rewriting it in a functional style, we simply freeze the state when we need + to by issuing a deep copy of the profiling data. *) +(** TODO: rewrite me in purely functional style *) +let deepcopy_entry { total; local; ncalls; max_total } = + { total; local; ncalls; max_total } -let rec deepcopy_treenode {entry; children} = - {entry = deepcopy_entry entry; - children = - (let children' = Hashtbl.create (Hashtbl.length children) in - Hashtbl.iter - (fun key subtree -> Hashtbl.add children' key (deepcopy_treenode subtree)) - children; - children')} +let rec deepcopy_treenode { entry; children } = + let children' = Hashtbl.create (Hashtbl.length children) in + let iter key subtree = Hashtbl.add children' key (deepcopy_treenode subtree) in + let () = Hashtbl.iter iter children in + { entry = deepcopy_entry entry; children = children' } -let stack = Summary.ref ~freeze:(fun _ -> List.map deepcopy_treenode) [{entry=empty_entry(); children=Hashtbl.create 20}] ~name:"LtacProf-stack" +let stack = + let freeze _ = List.map deepcopy_treenode in + Summary.ref ~freeze [empty_treenode 20] ~name:"LtacProf-stack" let on_stack = Hashtbl.create 5 let get_node c table = try Hashtbl.find table c with Not_found -> - let new_node = {entry=empty_entry(); children=Hashtbl.create 5} in + let new_node = empty_treenode 5 in Hashtbl.add table c new_node; new_node @@ -79,35 +102,33 @@ let rec add_node node node' = (fun s node' -> add_node (get_node s node.children) node') node'.children -let time() = - let times = Unix.times() in +let time () = + let times = Unix.times () in times.Unix.tms_utime +. times.Unix.tms_stime let rec print_treenode indent (tn : treenode) = - msgnl(str(indent^"{ entry = {")); - Feedback.msg_notice(str(indent^"total = ")); - msgnl(str (indent^(string_of_float (tn.entry.total)))); - Feedback.msg_notice(str(indent^"local = ")); - msgnl(str (indent^(string_of_float tn.entry.local))); - Feedback.msg_notice(str(indent^"ncalls = ")); - msgnl(str (indent^(string_of_int tn.entry.ncalls))); - Feedback.msg_notice(str(indent^"max_total = ")); - msgnl(str (indent^(string_of_float tn.entry.max_total))); - msgnl(str(indent^"}")); - msgnl(str(indent^"children = {")); + msgnl (str (indent^"{ entry = {")); + Feedback.msg_notice (str (indent^"total = ")); + msgnl (str (indent^(string_of_float (tn.entry.total)))); + Feedback.msg_notice (str (indent^"local = ")); + msgnl (str (indent^(string_of_float tn.entry.local))); + Feedback.msg_notice (str (indent^"ncalls = ")); + msgnl (str (indent^(string_of_int tn.entry.ncalls))); + Feedback.msg_notice (str (indent^"max_total = ")); + msgnl (str (indent^(string_of_float tn.entry.max_total))); + msgnl (str (indent^"}")); + msgnl (str (indent^"children = {")); Hashtbl.iter (fun s node -> - msgnl(str(indent^" "^s^" |-> ")); + msgnl (str (indent^" "^s^" |-> ")); print_treenode (indent^" ") node ) tn.children; - msgnl(str(indent^"} }")) - -let rec print_stack (st : treenode list) = - (match st with - | [] -> msgnl(str "[]") - | x::xs -> print_treenode "" x; msgnl(str("::")); print_stack xs) + msgnl (str (indent^"} }")) +let rec print_stack (st : treenode list) = match st with +| [] -> msgnl (str "[]") +| x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs let string_of_call ck = let s = @@ -115,14 +136,14 @@ let string_of_call ck = (match ck with | Tacexpr.LtacNotationCall s -> Names.KerName.print s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id,t) -> Nameops.pr_id id + | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> - (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.ghost,te))) - | Tacexpr.LtacConstrInterp (c,_) -> - pr_glob_constr_env (Global.env()) c + (Pptactic.pr_glob_tactic (Global.env ()) + (Tacexpr.TacAtom (Loc.ghost, te))) + | Tacexpr.LtacConstrInterp (c, _) -> + pr_glob_constr_env (Global.env ()) c | Tacexpr.LtacMLCall te -> - (Pptactic.pr_glob_tactic (Global.env()) + (Pptactic.pr_glob_tactic (Global.env ()) te) ) in for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done; @@ -135,48 +156,49 @@ let exit_tactic start_time add_total c = let parent = List.hd stack' in stack := stack'; if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time() -. start_time in + let diff = time () -. start_time in parent.entry.local <- parent.entry.local -. diff; - add_entry node.entry add_total {total = diff; local = diff; ncalls = 1; max_total = diff}; - with Failure("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking() + let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in + add_entry node.entry add_total node'; + with Failure ("hd") -> (* oops, our stack is invalid *) + encounter_multi_success_backtracking () let tclFINALLY tac (finally : unit Proofview.tactic) = let open Proofview.Notations in Proofview.tclIFCATCH tac (fun v -> finally <*> Proofview.tclUNIT v) - (fun (exn,info) -> finally <*> Proofview.tclZERO ~info exn) + (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) let do_profile s call_trace tac = let open Proofview.Notations in Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - if !is_profiling && is_new_call() then + if !is_profiling && is_new_call () then match call_trace with | (_, c) :: _ -> - let s = string_of_call c in - let parent = List.hd !stack in - let node, add_total = try Hashtbl.find on_stack s, false - with Not_found -> - let node = get_node s parent.children in - Hashtbl.add on_stack s node; - node, true - in - if not add_total && node = List.hd !stack then None else ( - stack := node :: !stack; - let start_time = time() in + let s = string_of_call c in + let parent = List.hd !stack in + let node, add_total = try Hashtbl.find on_stack s, false + with Not_found -> + let node = get_node s parent.children in + Hashtbl.add on_stack s node; + node, true + in + if not add_total && node = List.hd !stack then None else ( + stack := node :: !stack; + let start_time = time () in Some (start_time, add_total) - ) + ) | [] -> None else None)) >>= function | Some (start_time, add_total) -> tclFINALLY tac (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - (match call_trace with - | (_, c) :: _ -> + (match call_trace with + | (_, c) :: _ -> exit_tactic start_time add_total c - | [] -> ())))) + | [] -> ())))) | None -> tac @@ -187,91 +209,86 @@ let padl n s = ws (max 0 (n - utf8_length s)) ++ str s let padr n s = str s ++ ws (max 0 (n - utf8_length s)) let padr_with c n s = let ulength = utf8_length s in - str (utf8_sub s 0 n) ++ str(String.make (max 0 (n - ulength)) c) + str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) let rec list_iter_is_last f = function | [] -> () | [x] -> f true x | x :: xs -> f false x; list_iter_is_last f xs -let header() = - msgnl(str" tactic self total calls max"); - msgnl(str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") +let header () = + msgnl (str" tactic self total calls max"); + msgnl (str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") -let rec print_node all_total indent prefix (s,n) = +let rec print_node all_total indent prefix (s, n) = let e = n.entry in - msgnl( - h 0( + msgnl ( + h 0 ( padr_with '-' 40 (prefix ^ s ^ " ") - ++padl 7 (format_ratio (e.local /. all_total)) - ++padl 7 (format_ratio (e.total /. all_total)) - ++padl 8 (string_of_int e.ncalls) - ++padl 10 (format_sec(e.max_total)) + ++ padl 7 (format_ratio (e.local /. all_total)) + ++ padl 7 (format_ratio (e.total /. all_total)) + ++ padl 8 (string_of_int e.ncalls) + ++ padl 10 (format_sec (e.max_total)) ) ); print_table all_total indent false n.children and print_table all_total indent first_level table = - let ls = Hashtbl.fold - (fun s n l -> if n.entry.total /. all_total < 0.02 then l else (s, n) :: l) - table [] in + let fold s n l = if n.entry.total /. all_total < 0.02 then l else (s, n) :: l in + let ls = Hashtbl.fold fold table [] in match ls with - | [(s,n)] when (not first_level) -> - print_node all_total indent (indent^"└") (s,n) + | [s, n] when not first_level -> + print_node all_total indent (indent ^ "└") (s, n) | _ -> - let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in - list_iter_is_last - (fun is_last -> - print_node - all_total - (indent^if first_level then "" else if is_last then " " else " │") - (indent^if first_level then "─" else if is_last then " └─" else " ├─") - ) - ls - -let print_results() = + let ls = List.sort (fun (_, n1) (_, n2) -> compare n2.entry.total n1.entry.total) ls in + let iter is_last = + let sep0 = if first_level then "" else if is_last then " " else " │" in + let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in + print_node all_total (indent ^ sep0) (indent ^ sep1) + in + list_iter_is_last iter ls + +let print_results () = let tree = (List.hd !stack).children in let all_total = -. (List.hd !stack).entry.local in let global = Hashtbl.create 20 in let rec cumulate table = - Hashtbl.iter - (fun s node -> - let node' = get_node s global in - add_entry node'.entry true node.entry; - cumulate node.children - ) - table + let iter s node = + let node' = get_node s global in + add_entry node'.entry true node.entry; + cumulate node.children + in + Hashtbl.iter iter table in cumulate tree; - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) + warn_encountered_multi_success_backtracking (); + msgnl (str""); + msgnl (h 0 ( + str"total time: "++padl 11 (format_sec (all_total)) ) ); - msgnl(str""); - header(); + msgnl (str""); + header (); print_table all_total "" true global; - msgnl(str""); - header(); + msgnl (str""); + header (); print_table all_total "" true tree (* FOR DEBUGGING *) (* ; - msgnl(str""); - print_stack(!stack) + msgnl (str""); + print_stack (!stack) *) let print_results_tactic tactic = let tree = (List.hd !stack).children in let table_tactic = Hashtbl.create 20 in let rec cumulate table = - Hashtbl.iter - (fun s node -> - if String.sub (s^".") 0 (min (1+String.length s) (String.length tactic)) = tactic - then add_node (get_node s table_tactic) node - else cumulate node.children - ) - table + let iter s node = + if String.sub (s ^ ".") 0 (min (1 + String.length s) (String.length tactic)) = tactic + then add_node (get_node s table_tactic) node + else cumulate node.children + in + Hashtbl.iter iter table in cumulate tree; let all_total = -. (List.hd !stack).entry.local in @@ -279,22 +296,22 @@ let print_results_tactic tactic = Hashtbl.fold (fun _ node all_total -> node.entry.total +. all_total) table_tactic 0. in - warn_encountered_multi_success_backtracking(); - msgnl(str""); - msgnl(h 0( - str"total time: "++padl 11 (format_sec(all_total)) + warn_encountered_multi_success_backtracking (); + msgnl (str""); + msgnl (h 0 ( + str"total time: "++padl 11 (format_sec (all_total)) ) - ); - msgnl(h 0( - str"time spent in tactic: "++padl 11 (format_sec(tactic_total)) + ); + msgnl (h 0 ( + str"time spent in tactic: "++padl 11 (format_sec (tactic_total)) ) ); - msgnl(str""); - header(); + msgnl (str""); + header (); print_table tactic_total "" true table_tactic -let reset_profile() = - stack := [{entry=empty_entry(); children=Hashtbl.create 20}]; +let reset_profile () = + stack := [empty_treenode 20]; encountered_multi_success_backtracking := false let do_print_results_at_close () = if get_profiling () then print_results () diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli index bc4f90f04..7bbdca942 100644 --- a/ltac/profile_ltac.mli +++ b/ltac/profile_ltac.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Ltac profiling primitives *) + val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index a4ba5eab4..c092a0cb6 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -8,32 +8,32 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +(** Ltac profiling entrypoints *) + open Profile_ltac open Stdarg DECLARE PLUGIN "profile_ltac_plugin" let tclSET_PROFILING b = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> - set_profiling b)) + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) TACTIC EXTEND start_ltac_profiling - | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] +| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END TACTIC EXTEND stop_profiling - | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] -END;; +| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] +END VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] + [ "Reset" "Ltac" "Profile" ] -> [ reset_profile() ] END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" ] -> [ print_results() ] + [ "Show" "Ltac" "Profile" ] -> [ print_results() ] END - VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] + [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] END -- cgit v1.2.3 From 89b3335755910b659d6449d343bed69fae1d609e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 01:17:04 +0200 Subject: Better coding style (semantics). --- ltac/profile_ltac.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index b008d389f..405c494a6 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -150,18 +150,17 @@ let string_of_call ck = let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in CString.strip s -let exit_tactic start_time add_total c = - try - let node :: stack' = !stack in - let parent = List.hd stack' in - stack := stack'; - if add_total then Hashtbl.remove on_stack (string_of_call c); - let diff = time () -. start_time in - parent.entry.local <- parent.entry.local -. diff; - let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in - add_entry node.entry add_total node'; - with Failure ("hd") -> (* oops, our stack is invalid *) - encounter_multi_success_backtracking () +let exit_tactic start_time add_total c = match !stack with +| [] | [_] -> + (* oops, our stack is invalid *) + encounter_multi_success_backtracking () +| node :: (parent :: _ as stack') -> + stack := stack'; + if add_total then Hashtbl.remove on_stack (string_of_call c); + let diff = time () -. start_time in + parent.entry.local <- parent.entry.local -. diff; + let node' = { total = diff; local = diff; ncalls = 1; max_total = diff } in + add_entry node.entry add_total node' let tclFINALLY tac (finally : unit Proofview.tactic) = let open Proofview.Notations in -- cgit v1.2.3 From b21fefc0ec0aab2560d0b654f1a1f4203898388b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 01:20:19 +0200 Subject: Correct use of printing primitives. --- ltac/profile_ltac.ml | 72 ++++++++++++++++++++++++---------------------------- 1 file changed, 33 insertions(+), 39 deletions(-) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 405c494a6..aba7dde3c 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -211,25 +211,24 @@ let padr_with c n s = str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c) let rec list_iter_is_last f = function - | [] -> () - | [x] -> f true x - | x :: xs -> f false x; list_iter_is_last f xs + | [] -> [] + | [x] -> [f true x] + | x :: xs -> f false x :: list_iter_is_last f xs -let header () = - msgnl (str" tactic self total calls max"); - msgnl (str"────────────────────────────────────────┴──────┴──────┴───────┴─────────┘") +let header = + str " tactic self total calls max" ++ + fnl () ++ + str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" let rec print_node all_total indent prefix (s, n) = let e = n.entry in - msgnl ( - h 0 ( - padr_with '-' 40 (prefix ^ s ^ " ") - ++ padl 7 (format_ratio (e.local /. all_total)) - ++ padl 7 (format_ratio (e.total /. all_total)) - ++ padl 8 (string_of_int e.ncalls) - ++ padl 10 (format_sec (e.max_total)) - ) - ); + h 0 ( + padr_with '-' 40 (prefix ^ s ^ " ") + ++ padl 7 (format_ratio (e.local /. all_total)) + ++ padl 7 (format_ratio (e.total /. all_total)) + ++ padl 8 (string_of_int e.ncalls) + ++ padl 10 (format_sec (e.max_total)) + ) ++ print_table all_total indent false n.children and print_table all_total indent first_level table = @@ -245,7 +244,7 @@ and print_table all_total indent first_level table = let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in print_node all_total (indent ^ sep0) (indent ^ sep1) in - list_iter_is_last iter ls + prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls) let print_results () = let tree = (List.hd !stack).children in @@ -261,17 +260,16 @@ let print_results () = in cumulate tree; warn_encountered_multi_success_backtracking (); - msgnl (str""); - msgnl (h 0 ( - str"total time: "++padl 11 (format_sec (all_total)) - ) - ); - msgnl (str""); - header (); - print_table all_total "" true global; - msgnl (str""); - header (); - print_table all_total "" true tree + let msg = + h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ + fnl () ++ + header ++ + print_table all_total "" true global ++ + fnl () ++ + header ++ + print_table all_total "" true tree + in + Feedback.msg_notice msg (* FOR DEBUGGING *) (* ; msgnl (str""); @@ -296,18 +294,14 @@ let print_results_tactic tactic = (fun _ node all_total -> node.entry.total +. all_total) table_tactic 0. in warn_encountered_multi_success_backtracking (); - msgnl (str""); - msgnl (h 0 ( - str"total time: "++padl 11 (format_sec (all_total)) - ) - ); - msgnl (h 0 ( - str"time spent in tactic: "++padl 11 (format_sec (tactic_total)) - ) - ); - msgnl (str""); - header (); - print_table tactic_total "" true table_tactic + let msg = + h 0 (str"total time: " ++ padl 11 (format_sec (all_total))) ++ + h 0 (str"time spent in tactic: " ++ padl 11 (format_sec (tactic_total))) ++ + fnl () ++ + header ++ + print_table tactic_total "" true table_tactic + in + Feedback.msg_notice msg let reset_profile () = stack := [empty_treenode 20]; -- cgit v1.2.3 From d018d4148ef6cce96006bd76f83ccf46f6225e11 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 14 Jun 2016 01:31:30 +0200 Subject: Commenting out debugging code. --- ltac/profile_ltac.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index aba7dde3c..7a8ef32c3 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -25,10 +25,6 @@ let new_call = ref false let entered_call () = new_call := true let is_new_call () = let b = !new_call in new_call := false; b -(** Local versions of the old Pp.msgnl *) -let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) -let msgnl strm = msgnl_with !Pp_control.std_ft strm - (** LtacProf cannot yet handle backtracking into multi-success tactics. To properly support this, we'd have to somehow recreate our location in the call-stack, and stop/restart the intervening timers. This is tricky and @@ -106,6 +102,10 @@ let time () = let times = Unix.times () in times.Unix.tms_utime +. times.Unix.tms_stime +(* +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !Pp_control.std_ft strm + let rec print_treenode indent (tn : treenode) = msgnl (str (indent^"{ entry = {")); Feedback.msg_notice (str (indent^"total = ")); @@ -129,6 +129,7 @@ let rec print_treenode indent (tn : treenode) = let rec print_stack (st : treenode list) = match st with | [] -> msgnl (str "[]") | x :: xs -> print_treenode "" x; msgnl (str ("::")); print_stack xs +*) let string_of_call ck = let s = -- cgit v1.2.3