# HG changeset patch # User wenzelm # Date 1300652891 -3600 # Node ID 2c3fe3cbebae1c6168c4accb9e10b85b412642e0 # Parent dee23d63d4662ed64c0ef68dfe443c22c9ca0dbb structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned; diff -r dee23d63d466 -r 2c3fe3cbebae src/HOL/Matrix/Compute_Oracle/report.ML --- a/src/HOL/Matrix/Compute_Oracle/report.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/report.ML Sun Mar 20 21:28:11 2011 +0100 @@ -11,9 +11,9 @@ fun timeit f = let - val t1 = start_timing () + val t1 = Timing.start () val x = f () - val t2 = #message (end_timing t1) + val t2 = Timing.message (Timing.result t1) val _ = writeln ((report_space ()) ^ "--> "^t2) in x diff -r dee23d63d466 -r 2c3fe3cbebae src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Mar 20 21:28:11 2011 +0100 @@ -209,11 +209,11 @@ | SOME NONE => error ("bad option: " ^ key) | NONE => default) -fun cpu_time f x = +fun cpu_time f x = (* FIXME !? *) let - val start = start_timing () + val start = Timing.start () val result = Exn.capture (fn () => f x) () - val time = Time.toMilliseconds (#cpu (end_timing start)) + val time = Time.toMilliseconds (#cpu (Timing.result start)) in (Exn.release result, time) end end diff -r dee23d63d466 -r 2c3fe3cbebae src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 20 21:28:11 2011 +0100 @@ -332,11 +332,11 @@ fun count x = (length oo filter o equal) x -fun cpu_time description f = +fun cpu_time description f = (* FIXME !? *) let - val start = start_timing () + val start = Timing.start () val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) + val time = Time.toMilliseconds (#cpu (Timing.result start)) in (Exn.release result, (description, time)) end (* fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t = diff -r dee23d63d466 -r 2c3fe3cbebae src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 21:28:11 2011 +0100 @@ -211,11 +211,11 @@ val mk_split_lambda = HOLogic.tupled_lambda o HOLogic.mk_tuple -fun cpu_time description f = +fun cpu_time description f = (* FIXME !? *) let - val start = start_timing () + val start = Timing.start () val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) + val time = Time.toMilliseconds (#cpu (Timing.result start)) in (Exn.release result, (description, time)) end fun compile_term compilation options ctxt t = diff -r dee23d63d466 -r 2c3fe3cbebae src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:20:07 2011 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:28:11 2011 +0100 @@ -536,13 +536,12 @@ fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc) | and_to_list fm acc = rev (fm :: acc) val clauses = and_to_list prop_fm [] - val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) - clauses - val cterms = map (Thm.cterm_of @{theory}) terms - val timer = start_timing () - val thm = sat.rawsat_thm @{context} cterms + val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses + val cterms = map (Thm.cterm_of @{theory}) terms + val start = Timing.start () + val thm = sat.rawsat_thm @{context} cterms in - (end_timing timer, !sat.counter) + (Timing.result start, ! sat.counter) end; *} diff -r dee23d63d466 -r 2c3fe3cbebae src/Provers/blast.ML --- a/src/Provers/blast.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Provers/blast.ML Sun Mar 20 21:28:11 2011 +0100 @@ -914,7 +914,7 @@ fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = if b then - writeln (#message (end_timing start) ^ " for search. Closed: " + writeln (Timing.message (Timing.result start) ^ " for search. Closed: " ^ string_of_int (!nclosed) ^ " tried: " ^ string_of_int (!ntried) ^ " tactics: " ^ string_of_int (length tacs)) @@ -1256,7 +1256,7 @@ val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem fun cont (tacs,_,choices) = - let val start = start_timing () + let val start = Timing.start () in case Seq.pull(EVERY' (rev tacs) i st) of NONE => (writeln ("PROOF FAILED for depth " ^ @@ -1265,7 +1265,7 @@ else (); backtrack choices) | cell => (if (!trace orelse !stats) - then writeln (#message (end_timing start) ^ " for reconstruction") + then writeln (Timing.message (Timing.result start) ^ " for reconstruction") else (); Seq.make(fn()=> cell)) end @@ -1273,13 +1273,13 @@ handle PROVE => Seq.empty (*Public version with fixed depth*) -fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st; +fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st; val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20); fun blast_tac cs i st = ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit) - (timing_depth_tac (start_timing ()) cs) 0) i + (timing_depth_tac (Timing.start ()) cs) 0) i THEN flexflex_tac) st handle TRANS s => ((if !trace then warning ("blast: " ^ s) else ()); @@ -1299,7 +1299,7 @@ let val state as State {fullTrace = ft, ...} = initialize thy; val res = timeap prove - (state, start_timing(), cs, [initBranch ([readGoal thy s], lim)], I); + (state, Timing.start (), cs, [initBranch ([readGoal thy s], lim)], I); val _ = fullTrace := !ft; in res end; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/General/markup.ML Sun Mar 20 21:28:11 2011 +0100 @@ -100,7 +100,7 @@ val elapsedN: string val cpuN: string val gcN: string - val timingN: string val timing: timing -> T + val timingN: string val timing: Timing.timing -> T val subgoalsN: string val proof_stateN: string val proof_state: int -> T val stateN: string val state: T @@ -312,7 +312,7 @@ val cpuN = "cpu"; val gcN = "gc"; -fun timing ({elapsed, cpu, gc, ...}: timing) = +fun timing {elapsed, cpu, gc} = (timingN, [(elapsedN, Time.toString elapsed), (cpuN, Time.toString cpu), diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/General/output.ML Sun Mar 20 21:28:11 2011 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/output.ML Author: Makarius, Hagia Maria Sion Abbey (Jerusalem) -Output channels and timing messages. +Isabelle output channels. *) signature BASIC_OUTPUT = @@ -10,11 +10,6 @@ val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit - val cond_timeit: bool -> string -> (unit -> 'a) -> 'a - val timeit: (unit -> 'a) -> 'a - val timeap: ('a -> 'b) -> 'a -> 'b - val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b - val timing: bool Unsynchronized.ref end; signature OUTPUT = @@ -111,31 +106,6 @@ fun legacy_feature s = warning ("Legacy feature! " ^ s); - - -(** timing **) - -(*conditional timing with message*) -fun cond_timeit flag msg e = - if flag then - let - val start = start_timing (); - val result = Exn.capture e (); - val end_msg = #message (end_timing start); - val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg); - in Exn.release result end - else e (); - -(*unconditional timing*) -fun timeit e = cond_timeit true "" e; - -(*timed application function*) -fun timeap f x = timeit (fn () => f x); -fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); - -(*global timing mode*) -val timing = Unsynchronized.ref false; - end; structure Basic_Output: BASIC_OUTPUT = Output; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/General/timing.ML Sun Mar 20 21:28:11 2011 +0100 @@ -4,19 +4,45 @@ Basic support for time measurement. *) -val seconds = Time.fromReal; +signature BASIC_TIMING = +sig + val cond_timeit: bool -> string -> (unit -> 'a) -> 'a + val timeit: (unit -> 'a) -> 'a + val timeap: ('a -> 'b) -> 'a -> 'b + val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b +end -fun start_timing () = +signature TIMING = +sig + include BASIC_TIMING + type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time} + type start + val start: unit -> start + val result: start -> timing + val message: timing -> string +end + +structure Timing: TIMING = +struct + +(* timer control *) + +type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}; + +abstype start = Start of + Timer.real_timer * Time.time * Timer.cpu_timer * + {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}} +with + +fun start () = let val real_timer = Timer.startRealTimer (); val real_time = Timer.checkRealTimer real_timer; val cpu_timer = Timer.startCPUTimer (); val cpu_times = Timer.checkCPUTimes cpu_timer; - in (real_timer, real_time, cpu_timer, cpu_times) end; + in Start (real_timer, real_time, cpu_timer, cpu_times) end; -type timing = {message: string, elapsed: Time.time, cpu: Time.time, gc: Time.time}; - -fun end_timing (real_timer, real_time, cpu_timer, cpu_times) : timing = +fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) = let val real_time2 = Timer.checkRealTimer real_timer; val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times; @@ -27,10 +53,34 @@ val elapsed = real_time2 - real_time; val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys; val cpu = usr2 - usr + sys2 - sys + gc; + in {elapsed = elapsed, cpu = cpu, gc = gc} end; - val message = - (toString elapsed ^ "s elapsed time, " ^ - toString cpu ^ "s cpu time, " ^ - toString gc ^ "s GC time") handle Time.Time => ""; - in {message = message, elapsed = elapsed, cpu = cpu, gc = gc} end; +end; + + +(* timing messages *) + +fun message {elapsed, cpu, gc} = + Time.toString elapsed ^ "s elapsed time, " ^ + Time.toString cpu ^ "s cpu time, " ^ + Time.toString gc ^ "s GC time" handle Time.Time => ""; +fun cond_timeit enabled msg e = + if enabled then + let + val timing_start = start (); + val res = Exn.capture e (); + val end_msg = message (result timing_start); + val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg); + in Exn.release res end + else e (); + +fun timeit e = cond_timeit true "" e; +fun timeap f x = timeit (fn () => f x); +fun timeap_msg msg f x = cond_timeit true msg (fn () => f x); + +end; + +structure Basic_Timing: BASIC_TIMING = Timing; +open Basic_Timing; + diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/IsaMakefile Sun Mar 20 21:28:11 2011 +0100 @@ -21,7 +21,6 @@ BOOTSTRAP_FILES = \ General/exn.ML \ - General/timing.ML \ ML-Systems/compiler_polyml-5.2.ML \ ML-Systems/compiler_polyml-5.3.ML \ ML-Systems/ml_name_space.ML \ @@ -101,6 +100,7 @@ General/symbol.ML \ General/symbol_pos.ML \ General/table.ML \ + General/timing.ML \ General/url.ML \ General/xml.ML \ General/xml_data.ML \ diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sun Mar 20 21:28:11 2011 +0100 @@ -271,7 +271,7 @@ fun load_thy name init pos text = let val (lexs, commands) = get_syntax (); - val time = ! Output.timing; + val time = ! Toplevel.timing; val _ = Present.init_theory name; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/Isar/toplevel.ML Sun Mar 20 21:28:11 2011 +0100 @@ -218,7 +218,7 @@ val quiet = Unsynchronized.ref false; val debug = Runtime.debug; val interact = Unsynchronized.ref false; -val timing = Output.timing; +val timing = Unsynchronized.ref false; val profiling = Unsynchronized.ref 0; val skip_proofs = Unsynchronized.ref false; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/ML-Systems/polyml_common.ML Sun Mar 20 21:28:11 2011 +0100 @@ -14,10 +14,12 @@ else use "ML-Systems/single_assignment_polyml.ML"; use "ML-Systems/multithreading.ML"; -use "General/timing.ML"; use "ML-Systems/ml_pretty.ML"; use "ML-Systems/use_context.ML"; +val seconds = Time.fromReal; + + (** ML system and platform related **) diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Sun Mar 20 21:28:11 2011 +0100 @@ -13,7 +13,6 @@ use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/multithreading.ML"; -use "General/timing.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/ml_pretty.ML"; structure PolyML = struct end; @@ -21,8 +20,9 @@ use "ML-Systems/use_context.ML"; +val seconds = Time.fromReal; + (*low-level pointer equality*) - CM.autoload "$smlnj/init/init.cmi"; val pointer_eq = InlineT.ptreql; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/PIDE/document.ML Sun Mar 20 21:28:11 2011 +0100 @@ -241,9 +241,9 @@ val is_proof = Keyword.is_proof (Toplevel.name_of tr); val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); - val start = start_timing (); + val start = Timing.start (); val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; - val _ = timing tr (end_timing start); + val _ = timing tr (Timing.result start); val _ = List.app (Toplevel.error_msg tr) errs; val res = (case result of diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Sun Mar 20 21:28:11 2011 +0100 @@ -156,7 +156,7 @@ bool_pref Pattern.trace_unify_fail "trace-unification" "Output error diagnostics during unification", - bool_pref Output.timing + bool_pref Toplevel.timing "global-timing" "Whether to enable timing in Isabelle.", bool_pref Toplevel.debug diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/ROOT.ML Sun Mar 20 21:28:11 2011 +0100 @@ -21,6 +21,7 @@ use "General/alist.ML"; use "General/table.ML"; use "General/output.ML"; +use "General/timing.ML"; use "General/properties.ML"; use "General/markup.ML"; use "General/scan.ML"; diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/System/session.ML --- a/src/Pure/System/session.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/System/session.ML Sun Mar 20 21:28:11 2011 +0100 @@ -101,13 +101,12 @@ (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())); if timing then let - val start = start_timing (); + val start = Timing.start (); val _ = use root; - val stop = end_timing start; val _ = Output.raw_stderr ("Timing " ^ item ^ " (" ^ string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ - #message stop ^ ")\n"); + Timing.message (Timing.result start) ^ ")\n"); in () end else use root; finish ())) diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/Tools/find_consts.ML Sun Mar 20 21:28:11 2011 +0100 @@ -69,7 +69,7 @@ fun find_consts ctxt raw_criteria = let - val start = start_timing (); + val start = Timing.start (); val thy = ProofContext.theory_of ctxt; val low_ranking = 10000; @@ -114,7 +114,7 @@ |> sort (rev_order o int_ord o pairself snd) |> map (apsnd fst o fst); - val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; + val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; in Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) :: Pretty.str "" :: diff -r dee23d63d466 -r 2c3fe3cbebae src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sun Mar 20 21:28:11 2011 +0100 @@ -464,7 +464,7 @@ fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let - val start = start_timing (); + val start = Timing.start (); val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt)) @@ -480,7 +480,7 @@ then " (" ^ string_of_int returned ^ " displayed)" else "")); - val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; + val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs"; in Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" :: diff -r dee23d63d466 -r 2c3fe3cbebae src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sun Mar 20 21:20:07 2011 +0100 +++ b/src/Tools/quickcheck.ML Sun Mar 20 21:28:11 2011 +0100 @@ -167,11 +167,11 @@ val frees = Term.add_frees t []; in (frees, list_abs_free (frees, t)) end -fun cpu_time description f = +fun cpu_time description f = (* FIXME !? *) let - val start = start_timing () + val start = Timing.start () val result = Exn.capture f () - val time = Time.toMilliseconds (#cpu (end_timing start)) + val time = Time.toMilliseconds (#cpu (Timing.result start)) in (Exn.release result, (description, time)) end fun limit ctxt (limit_time, is_interactive) f exc () =