# HG changeset patch # User wenzelm # Date 1754852985 -7200 # Node ID 85c982ddc82d97906a890bee529ad3dbb9831a5b # Parent 35b0ef2558daf530f9506dd57f529d9ee11986bb prefer compact theory + ML module; diff -r 35b0ef2558da -r 85c982ddc82d src/Tools/Profiling.thy --- a/src/Tools/Profiling.thy Sun Aug 10 18:00:53 2025 +0200 +++ b/src/Tools/Profiling.thy Sun Aug 10 21:09:45 2025 +0200 @@ -1,4 +1,4 @@ -(* Title: Tools/profiling.ML +(* Title: Tools/profiling.thy Author: Makarius Session profiling based on loaded ML image. @@ -8,7 +8,195 @@ imports Pure begin -ML_file "profiling.ML" +ML \ +signature PROFILING = +sig + val locales: theory -> string list + val locale_thms: theory -> string -> thm list + val locales_thms: theory -> thm list + val global_thms: theory -> thm list + val all_thms: theory -> thm list + type session_statistics = + {theories: int, + garbage_theories: int, + locales: int, + locale_thms: int, + global_thms: int, + sizeof_thys_id: int, + sizeof_thms_id: int, + sizeof_terms: int, + sizeof_types: int, + sizeof_names: int, + sizeof_spaces: int} + val session_statistics: string list -> session_statistics + val main: unit -> unit +end; + +structure Profiling: PROFILING = +struct + +(* theory content *) + +fun locales thy = + let + val parent_spaces = map Locale.locale_space (Theory.parents_of thy); + fun add name = + if exists (fn space => Name_Space.declared space name) parent_spaces then I + else cons name; + in fold add (Locale.get_locales thy) [] end; + +fun proper_thm thm = not (Thm.eq_thm_prop (Drule.dummy_thm, thm)); + +fun locale_thms thy loc = + (Locale.locale_notes thy loc, []) |-> + (fold (#2 #> fold (#2 #> (fold (#1 #> fold (fn thm => proper_thm thm ? cons thm )))))); + +fun locales_thms thy = + maps (locale_thms thy) (locales thy); + +fun global_thms thy = + Facts.dest_static true + (map Global_Theory.facts_of (Theory.parents_of thy)) (Global_Theory.facts_of thy) + |> maps #2; + +fun all_thms thy = locales_thms thy @ global_thms thy; + + +(* session content *) + +fun session_content thys = + let + val thms = maps all_thms thys; + val thys_id = map Context.theory_id thys; + val thms_id = map Thm.theory_id thms; + val terms = + Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty); + val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty); + val spaces = + maps (fn f => map f thys) + [Sign.class_space, + Sign.type_space, + Sign.const_space, + Theory.axiom_space, + Thm.oracle_space, + Global_Theory.fact_space, + Locale.locale_space, + Attrib.attribute_space o Context.Theory, + Method.method_space o Context.Theory]; + val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces)); + in + {thys_id = thys_id, thms_id = thms_id, terms = terms, + types = types, names = names, spaces = spaces} + end; + +fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b; +fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b; +fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b; + + +(* session statistics *) + +type session_statistics = + {theories: int, + garbage_theories: int, + locales: int, + locale_thms: int, + global_thms: int, + sizeof_thys_id: int, + sizeof_thms_id: int, + sizeof_terms: int, + sizeof_types: int, + sizeof_names: int, + sizeof_spaces: int}; + +fun session_statistics theories : session_statistics = + let + val theories_member = Symtab.defined (Symtab.make_set theories) o Context.theory_long_name; + + val context_thys = + #contexts (Context.finish_tracing ()) + |> map_filter (fn (Context.Theory thy, _) => SOME thy | _ => NONE); + + val loader_thys = map Thy_Info.get_theory (Thy_Info.get_names ()); + val loaded_thys = filter theories_member loader_thys; + val loaded_context_thys = filter theories_member context_thys; + + val all_thys = loader_thys @ context_thys; + val base_thys = filter_out theories_member all_thys; + + val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms, + types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys; + val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms, + types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys; + + val n = length loaded_thys; + val m = (case length loaded_context_thys of 0 => 0 | l => l - n); + in + {theories = n, + garbage_theories = m, + locales = Integer.sum (map (length o locales) loaded_thys), + locale_thms = Integer.sum (map (length o locales_thms) loaded_thys), + global_thms = Integer.sum (map (length o global_thms) loaded_thys), + sizeof_thys_id = + sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) - + sizeof_list_diff (all_thys_id, base_thys_id), + sizeof_thms_id = + sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) - + sizeof_list_diff (all_thms_id, base_thms_id), + sizeof_terms = + sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) - + sizeof_list_diff (all_terms, base_terms), + sizeof_types = + sizeof1_diff ((all_types, all_names), (base_types, all_names)) - + sizeof_list_diff (all_types, base_types), + sizeof_spaces = + sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) - + sizeof_list_diff (all_spaces, base_spaces), + sizeof_names = sizeof_diff (all_names, base_names)} + end; + + +(* main entry point for external process *) + +local + +val decode_args : string list XML.Decode.T = + let open XML.Decode in list string end; + +val encode_result : session_statistics XML.Encode.T = + (fn {theories = a, + garbage_theories = b, + locales = c, + locale_thms = d, + global_thms = e, + sizeof_thys_id = f, + sizeof_thms_id = g, + sizeof_terms = h, + sizeof_types = i, + sizeof_names = j, + sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #> + let open XML.Encode in + pair int (pair int (pair int (pair int (pair int (pair int (pair int + (pair int (pair int (pair int int))))))))) + end; + +in + +fun main () = + (case getenv "ISABELLE_PROFILING" of + "" => () + | dir_name => + let + val dir = Path.explode dir_name; + val args = decode_args (YXML.parse_body (File.read (dir + \<^path>\args.yxml\))); + val result = session_statistics args; + in File.write (dir + \<^path>\result.yxml\) (YXML.string_of_body (encode_result result)) end); + +end; + +end; +\ + ML_command \Profiling.main ()\ end diff -r 35b0ef2558da -r 85c982ddc82d src/Tools/profiling.ML --- a/src/Tools/profiling.ML Sun Aug 10 18:00:53 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,192 +0,0 @@ -(* Title: Tools/profiling.ML - Author: Makarius - -Session profiling based on loaded ML image. -*) - -signature PROFILING = -sig - val locales: theory -> string list - val locale_thms: theory -> string -> thm list - val locales_thms: theory -> thm list - val global_thms: theory -> thm list - val all_thms: theory -> thm list - type session_statistics = - {theories: int, - garbage_theories: int, - locales: int, - locale_thms: int, - global_thms: int, - sizeof_thys_id: int, - sizeof_thms_id: int, - sizeof_terms: int, - sizeof_types: int, - sizeof_names: int, - sizeof_spaces: int} - val session_statistics: string list -> session_statistics - val main: unit -> unit -end; - -structure Profiling: PROFILING = -struct - -(* theory content *) - -fun locales thy = - let - val parent_spaces = map Locale.locale_space (Theory.parents_of thy); - fun add name = - if exists (fn space => Name_Space.declared space name) parent_spaces then I - else cons name; - in fold add (Locale.get_locales thy) [] end; - -fun proper_thm thm = not (Thm.eq_thm_prop (Drule.dummy_thm, thm)); - -fun locale_thms thy loc = - (Locale.locale_notes thy loc, []) |-> - (fold (#2 #> fold (#2 #> (fold (#1 #> fold (fn thm => proper_thm thm ? cons thm )))))); - -fun locales_thms thy = - maps (locale_thms thy) (locales thy); - -fun global_thms thy = - Facts.dest_static true - (map Global_Theory.facts_of (Theory.parents_of thy)) (Global_Theory.facts_of thy) - |> maps #2; - -fun all_thms thy = locales_thms thy @ global_thms thy; - - -(* session content *) - -fun session_content thys = - let - val thms = maps all_thms thys; - val thys_id = map Context.theory_id thys; - val thms_id = map Thm.theory_id thms; - val terms = - Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty); - val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty); - val spaces = - maps (fn f => map f thys) - [Sign.class_space, - Sign.type_space, - Sign.const_space, - Theory.axiom_space, - Thm.oracle_space, - Global_Theory.fact_space, - Locale.locale_space, - Attrib.attribute_space o Context.Theory, - Method.method_space o Context.Theory]; - val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces)); - in - {thys_id = thys_id, thms_id = thms_id, terms = terms, - types = types, names = names, spaces = spaces} - end; - -fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b; -fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b; -fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b; - - -(* session statistics *) - -type session_statistics = - {theories: int, - garbage_theories: int, - locales: int, - locale_thms: int, - global_thms: int, - sizeof_thys_id: int, - sizeof_thms_id: int, - sizeof_terms: int, - sizeof_types: int, - sizeof_names: int, - sizeof_spaces: int}; - -fun session_statistics theories : session_statistics = - let - val theories_member = Symtab.defined (Symtab.make_set theories) o Context.theory_long_name; - - val context_thys = - #contexts (Context.finish_tracing ()) - |> map_filter (fn (Context.Theory thy, _) => SOME thy | _ => NONE); - - val loader_thys = map Thy_Info.get_theory (Thy_Info.get_names ()); - val loaded_thys = filter theories_member loader_thys; - val loaded_context_thys = filter theories_member context_thys; - - val all_thys = loader_thys @ context_thys; - val base_thys = filter_out theories_member all_thys; - - val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms, - types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys; - val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms, - types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys; - - val n = length loaded_thys; - val m = (case length loaded_context_thys of 0 => 0 | l => l - n); - in - {theories = n, - garbage_theories = m, - locales = Integer.sum (map (length o locales) loaded_thys), - locale_thms = Integer.sum (map (length o locales_thms) loaded_thys), - global_thms = Integer.sum (map (length o global_thms) loaded_thys), - sizeof_thys_id = - sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) - - sizeof_list_diff (all_thys_id, base_thys_id), - sizeof_thms_id = - sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) - - sizeof_list_diff (all_thms_id, base_thms_id), - sizeof_terms = - sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) - - sizeof_list_diff (all_terms, base_terms), - sizeof_types = - sizeof1_diff ((all_types, all_names), (base_types, all_names)) - - sizeof_list_diff (all_types, base_types), - sizeof_spaces = - sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) - - sizeof_list_diff (all_spaces, base_spaces), - sizeof_names = sizeof_diff (all_names, base_names)} - end; - - -(* main entry point for external process *) - -local - -val decode_args : string list XML.Decode.T = - let open XML.Decode in list string end; - -val encode_result : session_statistics XML.Encode.T = - (fn {theories = a, - garbage_theories = b, - locales = c, - locale_thms = d, - global_thms = e, - sizeof_thys_id = f, - sizeof_thms_id = g, - sizeof_terms = h, - sizeof_types = i, - sizeof_names = j, - sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #> - let open XML.Encode in - pair int (pair int (pair int (pair int (pair int (pair int (pair int - (pair int (pair int (pair int int))))))))) - end; - -in - -fun main () = - (case getenv "ISABELLE_PROFILING" of - "" => () - | dir_name => - let - val dir = Path.explode dir_name; - val args = decode_args (YXML.parse_body (File.read (dir + \<^path>\args.yxml\))); - val result = session_statistics args; - in File.write (dir + \<^path>\result.yxml\) (YXML.string_of_body (encode_result result)) end); - -end; - -end;