Re: [isabelle] Performance bottleneck in Theory_Data.merge






On 22. Sep 2021, at 13:03, Makarius <makarius at sketis.net> wrote:

2. Whether position information is displayed or not seems to depend on how the
structure is actually generated, ie.
via. Theory_Data’, Theory_Data, or Generic_Data and also how the arguments are
declared. Some observations:
* Theory_Data’ seems to result in a filename as position
* Generic_Data(struct Type T = … end) seems to result in a link as position
* Generic_Data(Type T = …) (without the explicit struct) seems to have no
position information.

I could not reproduce this observation.


Below is some example output from my debug-version (based on Isabelle2021) were I have explicitly named the data slots (cf. "name" below). Note the difference in the output for 
sign.ML, locale.ML (locale), classical.ML. My guess was that it might be related to how the data slot is declared. Or is it related to the build (bootstrap) process of the sessions?


From context.ML:

type kind =
 {pos: Position.T,
  name: string, 
  empty: Any.T,
  extend: Any.T -> Any.T,
  merge: theory * theory -> Any.T * Any.T -> Any.T};

fun invoke name f k x =
  (case Datatab.lookup (Synchronized.value kinds) k of
    SOME kind =>
      if ! timing andalso name <> "" then
        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind) ^ " " ^ (#name kind))
          (fn () => f kind x)
      else f kind x
  | NONE => raise Fail "Invalid theory data identifier");



From sign.ML: 

structure Data = "">
(
  type T = sign;
  val name = "sign.ML";
  val extend = I;
  val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
  fun merge old_thys (sign1, sign2) =
    let
      val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
      val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;

      val syn = Syntax.merge_syntax (syn1, syn2);
      val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
      val consts = Consts.merge (consts1, consts2);
    in make_sign (syn, tsig, consts) end;
);

From locale.ML:

structure Locales = Theory_Data
(
  type T = locale Name_Space.table;
  val name = "locale.ML (locale)";
  val empty : T = Name_Space.empty_table "locale";
  val extend = I;
  val merge = Name_Space.join_tables (K merge_locale);
);

From classical.ML:

structure Claset = Generic_Data
(
  type T = claset;
  val name = "classical.ML";
  val empty = empty_cs;
  val extend = I;
  val merge = merge_cs;
);



=======================================
Theory_Data.merge (file "sign.ML") sign.ML
0.223s elapsed time, 1.291s cpu time, 0.707s GC time 
Theory_Data.merge (file "theory.ML") theory.ML
0.017s elapsed time, 0.105s cpu time, 0.000s GC time 
Theory_Data.merge (file "thm.ML") thm.ML
0.003s elapsed time, 0.020s cpu time, 0.000s GC time 
Theory_Data.merge (file "global_theory.ML") global_theory.ML
0.073s elapsed time, 0.432s cpu time, 0.000s GC time 
Theory_Data.merge (file "raw_simplifier.ML") raw_simplifier.ML (simpset)
0.005s elapsed time, 0.032s cpu time, 0.000s GC time 
Theory_Data.merge (file "ML/ml_env.ML") ml_env.ML
0.000s elapsed time, 0.001s cpu time, 0.000s GC time 
Theory_Data.merge attrib.ML (attribute)
0.000s elapsed time, 0.001s cpu time, 0.000s GC time 
Theory_Data.merge context_rules.ML
0.006s elapsed time, 0.047s cpu time, 0.000s GC time 
Theory_Data.merge locale.ML (locale)
0.000s elapsed time, 0.001s cpu time, 0.000s GC time 
Theory_Data.merge locale.ML (idents)
0.017s elapsed time, 0.089s cpu time, 0.000s GC time 
Theory_Data.merge locale.ML (global_registrations)
0.000s elapsed time, 0.006s cpu time, 0.000s GC time 
Theory_Data.merge locale.ML (thms)
0.001s elapsed time, 0.004s cpu time, 0.000s GC time 
Theory_Data.merge bundle.ML
0.000s elapsed time, 0.002s cpu time, 0.000s GC time 
Theory_Data.merge axclass.ML
0.000s elapsed time, 0.005s cpu time, 0.000s GC time 
Theory_Data.merge class.ML
0.000s elapsed time, 0.002s cpu time, 0.000s GC time 
Theory_Data.merge code.ML
0.001s elapsed time, 0.014s cpu time, 0.000s GC time 
Theory_Data.merge spec_rules.ML
0.002s elapsed time, 0.010s cpu time, 0.000s GC time 
Theory_Data.merge named_theorems.ML
0.003s elapsed time, 0.011s cpu time, 0.000s GC time 
Theory_Data.merge generated_files.ML
0.000s elapsed time, 0.001s cpu time, 0.000s GC time 
Theory_Data.merge (line 788 of "~~/src/HOL/HOL.thy") classical.ML
0.002s elapsed time, 0.009s cpu time, 0.000s GC time 
Theory_Data.merge (line 1529 of "~~/src/HOL/HOL.thy") induct.ML
0.001s elapsed time, 0.006s cpu time, 0.000s GC time 
Theory_Data.merge (line 416 of "~~/src/HOL/Inductive.thy") inductive.ML
0.000s elapsed time, 0.001s cpu time, 0.000s GC time 
Theory_Data.merge (line 13 of "~~/src/HOL/Fun_Def_Base.thy") function_common.ML
0.000s elapsed time, 0.006s cpu time, 0.000s GC time 
Theory_Data.merge (line 14 of "~~/src/HOL/Fun_Def_Base.thy") function_context_tree.ML
0.000s elapsed time, 0.004s cpu time, 0.000s GC time 
Theory_Data.merge (line 260 of "~~/src/HOL/Transfer.thy") transfer.ML
0.001s elapsed time, 0.007s cpu time, 0.000s GC time

Regards,
Norbert

--

Norbert Schirmer (nschirmer at apple.com)
 SEG Formal Verification



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.