# HG changeset patch # User smolkas # Date 1357259972 -3600 # Node ID 3e6eb9c4fc6d3285fa1394daf05d85a79137d94a # Parent eb67eec63a8b04850b6065892e91d37e26766cd4# Parent 32007a8db6bbe942ec709081dcefe16af1c6419c merged diff -r eb67eec63a8b -r 3e6eb9c4fc6d NEWS --- a/NEWS Thu Jan 03 15:05:48 2013 +0100 +++ b/NEWS Fri Jan 04 01:39:32 2013 +0100 @@ -82,6 +82,8 @@ * Dockable window "Symbols" provides some editing support for Isabelle symbols. +* Dockable window "Monitor" shows ML runtime statistics. + * Improved editing support for control styles: subscript, superscript, bold, reset of style -- operating on single symbols or text selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT. @@ -427,6 +429,8 @@ picked up from some surrounding directory. Potential INCOMPATIBILITY for home-made settings. +* Improved ML runtime statistics (heap, threads, future tasks etc.). + * Discontinued support for Poly/ML 5.2.1, which was the last version without exception positions and advanced ML compiler/toplevel configuration. diff -r eb67eec63a8b -r 3e6eb9c4fc6d etc/options --- a/etc/options Thu Jan 03 15:05:48 2013 +0100 +++ b/etc/options Fri Jan 04 01:39:32 2013 +0100 @@ -53,8 +53,6 @@ -- "level of parallel proof checking: 0, 1, 2" option parallel_proofs_threshold : int = 100 -- "threshold for sub-proof parallelization" -option ML_statistics : bool = false - -- "ML runtime statistics of parallel execution environment" section "Detail of Proof Recording" @@ -98,3 +96,6 @@ option editor_tracing_messages : int = 100 -- "initial number of tracing messages for each command transaction" + +option editor_chart_delay : real = 3.0 + -- "delay for chart repainting" diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Fri Jan 04 01:39:32 2013 +0100 @@ -1467,7 +1467,7 @@ also from ass_ok have "\ \ dom (locals (store (assign f v s2)))" - by (rule dom_locals_assign_mono) + by (rule dom_locals_assign_mono [where f = f]) finally show ?thesis by simp next case False diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Binary_Tree.thy --- a/src/HOL/Metis_Examples/Binary_Tree.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Binary_Tree.thy Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] datatype 'a bt = Lf diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Clausification.thy --- a/src/HOL/Metis_Examples/Clausification.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Clausification.thy Fri Jan 04 01:39:32 2013 +0100 @@ -10,10 +10,6 @@ imports Complex_Main begin -(* FIXME: shouldn't need this *) -declare [[unify_search_bound = 100]] -declare [[unify_trace_bound = 100]] - text {* Definitional CNF for facts *} @@ -22,7 +18,7 @@ axiomatization q :: "nat \ nat \ bool" where qax: "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "\b. \a. (q b a \ q a b)" by (metis qax) @@ -36,7 +32,7 @@ lemma "\b. \a. (q b a \ q 0 0 \ q 1 a \ q a 1) \ (q 0 1 \ q 1 0 \ q a b \ q 1 1)" by (metis (full_types) qax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "\b. \a. (q b a \ q a b)" by (metis qax) @@ -58,7 +54,7 @@ (r 2 0 \ r 2 1 \ r 2 2 \ r 2 3) \ (r 3 0 \ r 3 1 \ r 3 2 \ r 3 3)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis rax) @@ -66,7 +62,7 @@ lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis (full_types) rax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "r 0 0 \ r 1 1 \ r 2 2 \ r 3 3" by (metis rax) @@ -92,7 +88,7 @@ axiomatization p :: "nat \ nat \ bool" where pax: "\b. \a. (p b a \ p 0 0 \ p 1 a) \ (p 0 1 \ p 1 0 \ p a b)" -declare [[metis_new_skolemizer = false]] +declare [[metis_new_skolem = false]] lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" @@ -102,7 +98,7 @@ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" by (metis (full_types) pax) -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "\b. \a. \x. (p b a \ x) \ (p 0 0 \ x) \ (p 1 a \ x) \ (p 0 1 \ \ x) \ (p 1 0 \ \ x) \ (p a b \ \ x)" @@ -115,7 +111,7 @@ text {* New Skolemizer *} -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma fixes x :: real @@ -139,7 +135,7 @@ lemma "(\x \ set xs. P x) \ (\ys x zs. xs = ys @ x # zs \ P x \ (\z \ set zs. \ P z))" -by (metis split_list_last_prop [where P = P] in_set_conv_decomp) +by (metis split_list_last_prop[where P = P] in_set_conv_decomp) lemma ex_tl: "EX ys. tl ys = xs" using tl.simps(2) by fast diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Message.thy Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma strange_Un_eq [simp]: "A \ (B \ A) = B \ A" by (metis Un_commute Un_left_absorb) diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Sets.thy --- a/src/HOL/Metis_Examples/Sets.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Sets.thy Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) & (S(x,y) | ~S(y,z) | Q(Z,Z)) & diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Tarski.thy --- a/src/HOL/Metis_Examples/Tarski.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ imports Main "~~/src/HOL/Library/FuncSet" begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] (*Many of these higher-order problems appear to be impossible using the current linkup. They often seem to need either higher-order unification diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Trans_Closure.thy --- a/src/HOL/Metis_Examples/Trans_Closure.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] type_synonym addr = nat diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Jan 04 01:39:32 2013 +0100 @@ -12,7 +12,7 @@ imports Main begin -declare [[metis_new_skolemizer]] +declare [[metis_new_skolem]] sledgehammer_params [prover = spass, blocking, fact_filter = mepo, timeout = 30, preplay_timeout = 0, dont_minimize] diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jan 04 01:39:32 2013 +0100 @@ -1027,7 +1027,7 @@ | add_formula_vars bounds (AConn (_, phis)) = fold (add_formula_vars bounds) phis | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm - in mk_aquant AForall (add_formula_vars [] phi []) phi end + in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) = (if is_tptp_variable s andalso @@ -1039,6 +1039,7 @@ #> fold (add_term_vars bounds) tms | add_term_vars bounds (AAbs (((name, _), tm), args)) = add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args + fun close_formula_universally phi = close_universally add_term_vars phi fun add_iterm_vars bounds (IApp (tm1, tm2)) = @@ -1277,7 +1278,7 @@ handle TERM _ => @{const True} (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" - for obscure technical reasons. *) + for technical reasons. *) fun should_use_iff_for_eq CNF _ = false | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format) | should_use_iff_for_eq _ _ = true diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Jan 04 01:39:32 2013 +0100 @@ -522,23 +522,22 @@ fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof -fun map_term_names_in_term f (ATerm ((s, tys), ts)) = - ATerm ((f s, tys), map (map_term_names_in_term f) ts) -fun map_term_names_in_formula f (AQuant (q, xs, phi)) = - AQuant (q, xs, map_term_names_in_formula f phi) - | map_term_names_in_formula f (AConn (c, phis)) = - AConn (c, map (map_term_names_in_formula f) phis) - | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t) -fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) = - Definition_Step (name, map_term_names_in_formula f phi1, - map_term_names_in_formula f phi2) - | map_term_names_in_step f (Inference_Step (name, role, phi, rule, deps)) = - Inference_Step (name, role, map_term_names_in_formula f phi, rule, deps) -fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) +fun map_term_names_in_atp_proof f = + let + fun do_term (ATerm ((s, tys), ts)) = ATerm ((f s, tys), map do_term ts) + fun do_formula (AQuant (q, xs, phi)) = + AQuant (q, map (apfst f) xs, do_formula phi) + | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) + | do_formula (AAtom t) = AAtom (do_term t) + fun do_step (Definition_Step (name, phi1, phi2)) = + Definition_Step (name, do_formula phi1, do_formula phi2) + | do_step (Inference_Step (name, role, phi, rule, deps)) = + Inference_Step (name, role, do_formula phi, rule, deps) + in map do_step end fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s + fun nasty_atp_proof pool = - if Symtab.is_empty pool then I - else map_term_names_in_atp_proof (nasty_name pool) + not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool) end; diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Jan 04 01:39:32 2013 +0100 @@ -131,7 +131,7 @@ fun repair_var_name s = let fun subscript_name s n = s ^ nat_subscript n - val s = String.map Char.toLower s + val s = s |> String.map Char.toLower in case space_explode "_" s of [_] => (case take_suffix Char.isDigit (String.explode s) of @@ -158,6 +158,8 @@ fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT +val vampire_skolem_prefix = "sK" + (* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to be inferred. *) fun term_from_atp ctxt textual sym_tab = @@ -246,7 +248,11 @@ end with a digit and "variant_frees" appends letters. *) fun fresh_up s = [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst - val term_ts = map (do_term [] NONE) us + val term_ts = + map (do_term [] NONE) us + (* Vampire (2.6) passes arguments to Skolem functions in reverse + order *) + |> String.isPrefix vampire_skolem_prefix s ? rev val ts = term_ts @ extra_ts val T = case opt_T of diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Fri Jan 04 01:39:32 2013 +0100 @@ -167,21 +167,36 @@ (rename_bound_vars_RS th rl handle THM _ => tryall rls) in tryall rls end; +(* Special version of "rtac" that works around an explosion in the unifier. + If the goal has the form "?P c", the danger is that resolving it against a + property of the form "... c ... c ... c ..." will lead to a huge unification + problem, due to the (spurious) choices between projection and imitation. The + workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *) +fun quant_rtac th i st = + case (concl_of st, prop_of th) of + (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) => + let + val cc = cterm_of (theory_of_thm th) c + val ct = Thm.dest_arg (cprop_of th) + in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end + | _ => rtac th i st + (*Permits forward proof from rules that discharge assumptions. The supplied proof state st, e.g. from conj_forward, should have the form "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) fun forward_res ctxt nf st = - let fun forward_tacf [prem] = rtac (nf prem) 1 - | forward_tacf prems = - error (cat_lines - ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: - Display.string_of_thm ctxt st :: - "Premises:" :: map (Display.string_of_thm ctxt) prems)) + let + fun tacf [prem] = quant_rtac (nf prem) 1 + | tacf prems = + error (cat_lines + ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: + Display.string_of_thm ctxt st :: + "Premises:" :: map (Display.string_of_thm ctxt) prems)) in - case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st) - of SOME(th,_) => th - | NONE => raise THM("forward_res", 0, [st]) + case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of + SOME (th, _) => th + | NONE => raise THM ("forward_res", 0, [st]) end; (*Are any of the logical connectives in "bs" present in the term?*) @@ -635,7 +650,6 @@ val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv -(* "RS" can fail if "unify_search_bound" is too small. *) fun try_skolemize_etc ctxt th = let val thy = Proof_Context.theory_of ctxt diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Jan 04 01:39:32 2013 +0100 @@ -300,20 +300,20 @@ |> Skip_Proof.make_thm @{theory} (* Converts an Isabelle theorem into NNF. *) -fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = +fun nnf_axiom choice_ths new_skolem ax_no th ctxt = let val thy = Proof_Context.theory_of ctxt val th = th |> transform_elim_theorem |> zero_var_indexes - |> new_skolemizer ? forall_intr_vars + |> new_skolem ? forall_intr_vars val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single val th = th |> Conv.fconv_rule Object_Logic.atomize |> cong_extensionalize_thm thy |> abs_extensionalize_thm ctxt |> make_nnf ctxt in - if new_skolemizer then + if new_skolem then let fun skolemize choice_ths = skolemize_with_choice_theorems ctxt choice_ths @@ -364,14 +364,14 @@ end (* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th = +fun cnf_axiom ctxt0 new_skolem combinators ax_no th = let val thy = Proof_Context.theory_of ctxt0 val choice_ths = choice_theorems thy val (opt, (nnf_th, ctxt)) = - nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 + nnf_axiom choice_ths new_skolem ax_no th ctxt0 fun clausify th = - make_cnf (if new_skolemizer orelse null choice_ths then [] + make_cnf (if new_skolem orelse null choice_ths then [] else map (old_skolem_theorem_from_def thy) (old_skolem_defs th)) th ctxt ctxt val (cnf_ths, ctxt) = clausify nnf_th diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Jan 04 01:39:32 2013 +0100 @@ -11,7 +11,7 @@ sig val trace : bool Config.T val verbose : bool Config.T - val new_skolemizer : bool Config.T + val new_skolem : bool Config.T val advisory_simp : bool Config.T val type_has_top_sort : typ -> bool val metis_tac : @@ -29,8 +29,8 @@ open Metis_Generate open Metis_Reconstruct -val new_skolemizer = - Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) +val new_skolem = + Attrib.setup_config_bool @{binding metis_new_skolem} (K false) val advisory_simp = Attrib.setup_config_bool @{binding metis_advisory_simp} (K true) @@ -137,8 +137,8 @@ (* Main function to start Metis proof and reconstruction *) fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt - val new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) + val new_skolem = + Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) val do_lams = (lam_trans = liftingN orelse lam_trans = lam_liftingN) ? introduce_lam_wrappers ctxt @@ -146,7 +146,7 @@ map2 (fn j => fn th => (Thm.get_name_hint th, th |> Drule.eta_contraction_rule - |> Meson_Clausify.cnf_axiom ctxt new_skolemizer + |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j ||> map do_lams)) (0 upto length ths0 - 1) ths0 diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jan 04 01:39:32 2013 +0100 @@ -482,8 +482,8 @@ #> simplify_spaces #> maybe_quote val reconstr = Metis (type_enc, lam_trans) - fun do_metis ind (ls, ss) = - "\n" ^ do_indent (ind + 1) ^ + fun do_metis ind options (ls, ss) = + "\n" ^ do_indent (ind + 1) ^ options ^ reconstructor_command reconstr 1 1 [] 0 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) @@ -495,15 +495,19 @@ do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = do_indent ind ^ do_obtain qs xs ^ " " ^ - do_label l ^ do_term t ^ do_metis ind facts ^ "\n" + do_label l ^ do_term t ^ + (* The new skolemizer puts the arguments in the same order as the ATPs + (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding + Vampire). *) + do_metis ind "using [[metis_new_skolem]] " facts ^ "\n" | do_step ind (Prove (qs, l, t, By_Metis facts)) = do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ do_metis ind facts ^ "\n" + do_label l ^ do_term t ^ do_metis ind "" facts ^ "\n" | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) proofs) ^ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ - do_metis ind facts ^ "\n" + do_metis ind "" facts ^ "\n" and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/ML/ml_statistics.scala Fri Jan 04 01:39:32 2013 +0100 @@ -24,6 +24,8 @@ def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) def apply(log: Path): ML_Statistics = apply(read_log(log)) + val empty = apply(Nil) + /* standard fields */ @@ -84,11 +86,12 @@ final class ML_Statistics private(val stats: List[Properties.T]) { val Now = new Properties.Double("now") - - require(!stats.isEmpty && stats.forall(props => Now.unapply(props).isDefined)) + def now(props: Properties.T): Double = Now.unapply(props).get - val time_start = Now.unapply(stats.head).get - val duration = Now.unapply(stats.last).get - time_start + require(stats.forall(props => Now.unapply(props).isDefined)) + + val time_start = if (stats.isEmpty) 0.0 else now(stats.head) + val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start val fields: Set[String] = SortedSet.empty[String] ++ @@ -97,7 +100,7 @@ val content: List[ML_Statistics.Entry] = stats.map(props => { - val time = Now.unapply(props).get - time_start + val time = now(props) - time_start require(time >= 0.0) val data = SortedMap.empty[String, Double] ++ @@ -109,10 +112,9 @@ /* charts */ - def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) { - val data = new XYSeriesCollection - + data.removeAllSeries for { field <- selected_fields.iterator series = new XYSeries(field) @@ -120,20 +122,23 @@ content.foreach(entry => series.add(entry.time, entry.data(field))) data.addSeries(series) } + } + + def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + { + val data = new XYSeriesCollection + update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } - def chart_panel(title: String, selected_fields: Iterable[String]): ChartPanel = - new ChartPanel(chart(title, selected_fields)) + def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) def standard_frames: Unit = - for ((title, selected_fields) <- ML_Statistics.standard_fields) { - val c = chart(title, selected_fields) + ML_Statistics.standard_fields.map(chart(_)).foreach(c => Swing_Thread.later { new Frame { contents = Component.wrap(new ChartPanel(c)); visible = true } - } - } + }) } diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/System/isabelle_process.ML Fri Jan 04 01:39:32 2013 +0100 @@ -238,7 +238,7 @@ protocol_command "Isabelle_Process.options" (fn [options_yxml] => let val options = Options.decode (YXML.parse_body options_yxml) in - Future.ML_statistics := Options.bool options "ML_statistics"; + Future.ML_statistics := true; Multithreading.trace := Options.int options "threads_trace"; Multithreading.max_threads := Options.int options "threads"; if Multithreading.max_threads_value () < 2 diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/System/session.ML --- a/src/Pure/System/session.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/System/session.ML Fri Jan 04 01:39:32 2013 +0100 @@ -8,6 +8,7 @@ sig val id: unit -> string list val name: unit -> string + val path: unit -> string list val welcome: unit -> string val finish: unit -> unit val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list -> diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/System/session.scala Fri Jan 04 01:39:32 2013 +0100 @@ -22,7 +22,7 @@ /* events */ //{{{ - case class Statistics(stats: Properties.T) + case class Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(edits: List[Document.Edit_Text]) @@ -361,8 +361,8 @@ case None => } - case Markup.ML_Statistics(stats) if output.is_protocol => - statistics.event(Session.Statistics(stats)) + case Markup.ML_Statistics(props) if output.is_protocol => + statistics.event(Session.Statistics(props)) case _ if output.is_init => phase = Session.Ready diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/Thy/html.scala Fri Jan 04 01:39:32 2013 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Thy/html.scala Author: Makarius -Basic HTML output. +HTML presentation elements. */ package isabelle @@ -29,75 +29,19 @@ } - /// FIXME unused stuff - - // common elements and attributes - - val BODY = "body" - val DIV = "div" - val SPAN = "span" - val BR = "br" - val PRE = "pre" - val CLASS = "class" - val STYLE = "style" - + // common markup elements - // document markup - - def span(cls: String, body: XML.Body): XML.Elem = - XML.Elem(Markup(SPAN, List((CLASS, cls))), body) - - def user_font(font: String, txt: String): XML.Elem = - XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt))) - - def hidden(txt: String): XML.Elem = - span(Markup.HIDDEN, List(XML.Text(txt))) - - def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt))) - def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) - def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt))) + def session_entry(name: String): String = + XML.string_of_tree( + XML.elem("li", + List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), + List(XML.Text(name)))))) + "\n" - def spans(input: XML.Tree): XML.Body = - { - def html_spans(tree: XML.Tree): XML.Body = - tree match { - case XML.Wrapped_Elem(markup, _, ts) => - List(span(markup.name, ts.flatMap(html_spans))) - case XML.Elem(markup, ts) => - List(span(markup.name, ts.flatMap(html_spans))) - case XML.Text(txt) => - val ts = new ListBuffer[XML.Tree] - val t = new StringBuilder - def flush() { - if (!t.isEmpty) { - ts += XML.Text(t.toString) - t.clear - } - } - def add(elem: XML.Tree) { - flush() - ts += elem - } - val syms = Symbol.iterator(txt) - while (syms.hasNext) { - val s1 = syms.next - def s2() = if (syms.hasNext) syms.next else "" - if (s1 == "\n") add(XML.elem(BR)) - else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded) - { add(hidden(s1)); add(sub(s2())) } - else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded) - { add(hidden(s1)); add(sup(s2())) } - else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME - else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME - else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME - else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME - else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) } - else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) } - else t ++= s1 - } - flush() - ts.toList - } - html_spans(input) - } + def session_entries(names: List[String]): String = + if (names.isEmpty) "" + else + "\n\n
\n" + + "

Sessions

\n
    \n" + names.map(session_entry).mkString + "
"; + + val end_document = "\n
\n\n\n" } diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/Thy/present.ML Fri Jan 04 01:39:32 2013 +0100 @@ -213,7 +213,7 @@ (** document preparation **) -(* maintain index *) +(* maintain session index *) val session_entries = HTML.session_entries o diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/Thy/present.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/present.scala Fri Jan 04 01:39:32 2013 +0100 @@ -0,0 +1,41 @@ +/* Title: Pure/Thy/present.scala + Author: Makarius + +Theory presentation: HTML. +*/ + +package isabelle + + +object Present +{ + /* maintain session index -- NOT thread-safe */ + + private val index_path = Path.basic("index.html") + private val session_entries_path = Path.explode(".session/entries") + private val pre_index_path = Path.explode(".session/pre-index") + + private def get_entries(dir: Path): List[String] = + split_lines(File.read(dir + session_entries_path)) + + private def put_entries(entries: List[String], dir: Path): Unit = + File.write(dir + session_entries_path, cat_lines(entries)) + + def create_index(dir: Path): Unit = + File.write(dir + index_path, + File.read(dir + pre_index_path) + + HTML.session_entries(get_entries(dir)) + + HTML.end_document) + + def update_index(dir: Path, names: List[String]): Unit = + try { + put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir) + create_index(dir) + } + catch { + case ERROR(msg) => + java.lang.System.err.println( + "### " + msg + "\n### Browser info: failed to update session index of " + dir) + } +} + diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/Tools/build.ML Fri Jan 04 01:39:32 2013 +0100 @@ -43,7 +43,7 @@ (Options.int options "parallel_proofs_threshold") |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") - |> Unsynchronized.setmp Future.ML_statistics (Options.bool options "ML_statistics") + |> Unsynchronized.setmp Future.ML_statistics true |> no_document options ? Present.no_document |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty") |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs") @@ -89,6 +89,10 @@ | dups => error ("Duplicate document variants: " ^ commas_quote dups)); val _ = + (case Session.path () of + [] => () + | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path)); + val _ = Session.init do_output false (Options.bool options "browser_info") browser_info (Options.string options "document") diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/Tools/build.scala Fri Jan 04 01:39:32 2013 +0100 @@ -412,7 +412,7 @@ /* jobs */ - private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean, + private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean, verbose: Boolean, browser_info: Path) { // global browser info dir @@ -515,6 +515,8 @@ private def log(name: String): Path = LOG + Path.basic(name) private def log_gz(name: String): Path = log(name).ext("gz") + private val SESSION_PARENT_PATH = "\fSession.parent_path = " + private def sources_stamp(digests: List[SHA1.Digest]): String = digests.map(_.toString).sorted.mkString("sources: ", " ", "") @@ -600,7 +602,7 @@ } // scheduler loop - case class Result(current: Boolean, heap: String, rc: Int) + case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int) def sleep(): Unit = Thread.sleep(500) @@ -620,9 +622,10 @@ //{{{ finish job val (out, err, rc) = job.join + val out_lines = split_lines(out) progress.echo(Library.trim_line(err)) - val heap = + val (parent_path, heap) = if (rc == 0) { (output_dir + log(name)).file.delete @@ -631,7 +634,13 @@ File.write_gzip(output_dir + log_gz(name), sources + "\n" + parent_heap + "\n" + heap + "\n" + out) - heap + val parent_path = + if (job.info.options.bool("browser_info")) + out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line => + line.substring(SESSION_PARENT_PATH.length)) + else None + + (parent_path, heap) } else { (output_dir + Path.basic(name)).file.delete @@ -641,14 +650,14 @@ progress.echo(name + " FAILED") if (rc != 130) { progress.echo("(see also " + (output_dir + log(name)).file.toString + ")") - val lines = split_lines(out) - val tail = lines.drop(lines.length - 20 max 0) + val tail = out_lines.drop(out_lines.length - 20 max 0) progress.echo("\n" + cat_lines(tail)) } - no_heap + (None, no_heap) } - loop(pending - name, running - name, results + (name -> Result(false, heap, rc))) + loop(pending - name, running - name, + results + (name -> Result(false, parent_path, heap, rc))) //}}} case None if (running.size < (max_jobs max 1)) => //{{{ check/start next job @@ -656,7 +665,7 @@ case Some((name, info)) => val parent_result = info.parent match { - case None => Result(true, no_heap, 0) + case None => Result(true, None, no_heap, 0) case Some(parent) => results(parent) } val output = output_dir + Path.basic(name) @@ -679,10 +688,10 @@ val all_current = current && parent_result.current if (all_current) - loop(pending - name, running, results + (name -> Result(true, heap, 0))) + loop(pending - name, running, results + (name -> Result(true, None, heap, 0))) else if (no_build) { if (verbose) progress.echo("Skipping " + name + " ...") - loop(pending - name, running, results + (name -> Result(false, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) } else if (parent_result.rc == 0) { progress.echo((if (do_output) "Building " else "Running ") + name + " ...") @@ -691,7 +700,7 @@ } else { progress.echo(name + " CANCELLED") - loop(pending - name, running, results + (name -> Result(false, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) } case None => sleep(); loop(pending, running, results) } @@ -703,10 +712,17 @@ val results = if (deps.is_empty) { progress.echo("### Nothing to build") - Map.empty + Map.empty[String, Result] } else loop(queue, Map.empty, Map.empty) + val session_entries = + (for ((name, res) <- results.iterator if res.parent_path.isDefined) + yield (res.parent_path.get, name)).toList.groupBy(_._1).map( + { case (p, es) => (p, es.map(_._2).sorted) }) + for ((p, names) <- session_entries) + Present.update_index(browser_info + Path.explode(p), names) + val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc }) if (rc != 0 && (verbose || !no_build)) { val unfinished = diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Pure/build-jars --- a/src/Pure/build-jars Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Pure/build-jars Fri Jan 04 01:39:32 2013 +0100 @@ -57,6 +57,7 @@ System/utf8.scala Thy/completion.scala Thy/html.scala + Thy/present.scala Thy/thy_header.scala Thy/thy_info.scala Thy/thy_load.scala diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Jan 04 01:39:32 2013 +0100 @@ -43,9 +43,9 @@ private val relevant_options = Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit", "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin", - "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics", + "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit", - "editor_tracing_messages", "editor_update_delay") + "editor_tracing_messages", "editor_update_delay", "editor_chart_delay") relevant_options.foreach(PIDE.options.value.check_name _) diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Fri Jan 04 01:39:32 2013 +0100 @@ -12,59 +12,38 @@ import scala.actors.Actor._ import scala.swing.{TextArea, ScrollPane, Component} -import org.jfree.chart.{ChartFactory, ChartPanel} -import org.jfree.data.time.{Millisecond, TimeSeries, TimeSeriesCollection} +import org.jfree.chart.ChartPanel +import org.jfree.data.xy.XYSeriesCollection import org.gjt.sp.jedit.View class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) { - /* properties */ // FIXME avoid hardwired stuff - - private val Now = new Properties.Double("now") - private val Size_Heap = new Properties.Double("size_heap") + /* chart data -- owned by Swing thread */ - private val series = new TimeSeries("ML heap size", classOf[Millisecond]) - - - /* chart */ + private val chart = ML_Statistics.empty.chart(null, Nil) + private val data = chart.getXYPlot.getDataset.asInstanceOf[XYSeriesCollection] + private var rev_stats: List[Properties.T] = Nil - private val chart_panel = - { - val data = new TimeSeriesCollection(series) - val chart = ChartFactory.createTimeSeriesChart(null, "Time", "Value", data, true, true, false) - val plot = chart.getXYPlot() + private val delay_update = + Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { + ML_Statistics(rev_stats.reverse) + .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields + } - val x_axis = plot.getDomainAxis() - x_axis.setAutoRange(true) - x_axis.setFixedAutoRange(60000.0) - - val y_axis = plot.getRangeAxis() - y_axis.setAutoRange(true) - - new ChartPanel(chart) - } - set_content(chart_panel) + set_content(new ChartPanel(chart)) /* main actor */ private val main_actor = actor { - var t0: Option[Double] = None loop { react { - case Session.Statistics(stats) => - java.lang.System.err.println(stats) - stats match { - case Now(t1) => - if (t0.isEmpty) t0 = Some(t1) - val t = t1 - t0.get - stats match { - case Size_Heap(x) => series.add(new Millisecond(), x) // FIXME proper time point - case _ => - } - case _ => + case Session.Statistics(props) => + Swing_Thread.later { + rev_stats ::= props + delay_update.invoke() } case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad) } diff -r eb67eec63a8b -r 3e6eb9c4fc6d src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Jan 03 15:05:48 2013 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 04 01:39:32 2013 +0100 @@ -13,7 +13,7 @@ import scala.swing.{ListView, ScrollPane} -import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View} +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} import org.gjt.sp.jedit.syntax.ModeProvider import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} @@ -271,6 +271,8 @@ override def start() { try { + Debug.DISABLE_SEARCH_DIALOG_POOL = true + PIDE.plugin = this Isabelle_System.init() Isabelle_System.install_fonts()