# HG changeset patch # User wenzelm # Date 1701358380 -3600 # Node ID 3bdd3cf5f5e03c7d496112b6f60572190bce7a49 # Parent 58bb68b9470fd08ff92103f647136be4120e5d31 more detailed profiling including "names"; avoid overlapping results; diff -r 58bb68b9470f -r 3bdd3cf5f5e0 src/Pure/Tools/profiling.scala --- a/src/Pure/Tools/profiling.scala Thu Nov 30 13:35:17 2023 +0100 +++ b/src/Pure/Tools/profiling.scala Thu Nov 30 16:33:00 2023 +0100 @@ -39,6 +39,7 @@ sizeof_thms_id: Space = Space.zero, sizeof_terms: Space = Space.zero, sizeof_types: Space = Space.zero, + sizeof_names: Space = Space.zero, sizeof_spaces: Space = Space.zero) object Statistics { @@ -49,10 +50,10 @@ private val decode_result: XML.Decode.T[Session_Statistics] = (body: XML.Body) => { - val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = { + val (a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))) = { import XML.Decode._ pair(int, pair(int, pair(int, pair(int, pair(int, - pair(long, pair(long, pair(long, pair(long, long)))))))))(body) + pair(long, pair(long, pair(long, pair(long, pair(long, long))))))))))(body) } Session_Statistics( theories = a, @@ -64,7 +65,8 @@ sizeof_thms_id = Space.bytes(g), sizeof_terms = Space.bytes(h), sizeof_types = Space.bytes(i), - sizeof_spaces = Space.bytes(j)) + sizeof_names = Space.bytes(j), + sizeof_spaces = Space.bytes(k)) } def make( @@ -102,6 +104,7 @@ thms_id_size = session.sizeof_thms_id, terms_size = session.sizeof_terms, types_size = session.sizeof_types, + names_size = session.sizeof_names, spaces_size = session.sizeof_spaces) } @@ -121,6 +124,7 @@ "thms_id_size%", "terms_size%", "types_size%", + "names_size%", "spaces_size%") def header: List[String] = @@ -140,6 +144,7 @@ val thms_id_size: Space = Space.zero, val terms_size: Space = Space.zero, val types_size: Space = Space.zero, + val names_size: Space = Space.zero, val spaces_size: Space = Space.zero ) { private def print_total_theories: String = @@ -169,6 +174,7 @@ size_percentage(thms_id_size).toString, size_percentage(terms_size).toString, size_percentage(types_size).toString, + size_percentage(names_size).toString, size_percentage(spaces_size).toString) def fields: List[Any] = @@ -190,6 +196,7 @@ thms_id_size = other.cumulative.thms_id_size + thms_id_size, terms_size = other.cumulative.terms_size + terms_size, types_size = other.cumulative.types_size + types_size, + names_size = other.cumulative.names_size + names_size, spaces_size = other.cumulative.spaces_size + spaces_size) } diff -r 58bb68b9470f -r 3bdd3cf5f5e0 src/Tools/profiling.ML --- a/src/Tools/profiling.ML Thu Nov 30 13:35:17 2023 +0100 +++ b/src/Tools/profiling.ML Thu Nov 30 16:33:00 2023 +0100 @@ -21,6 +21,7 @@ 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 @@ -76,8 +77,14 @@ Locale.locale_space, Attrib.attribute_space o Context.Theory, Method.method_space o Context.Theory]; - in {thys_id = thys_id, thms_id = thms_id, terms = terms, types = types, spaces = spaces} end; + val names = maps 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; @@ -93,6 +100,7 @@ sizeof_thms_id: int, sizeof_terms: int, sizeof_types: int, + sizeof_names: int, sizeof_spaces: int}; fun session_statistics theories : session_statistics = @@ -111,9 +119,9 @@ 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, spaces = all_spaces} = session_content all_thys; + 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, spaces = base_spaces} = session_content base_thys; + 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); @@ -123,11 +131,22 @@ 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 = sizeof_diff (all_thys_id, base_thys_id), - sizeof_thms_id = sizeof_diff (all_thms_id, base_thms_id), - sizeof_terms = sizeof_diff (all_terms, base_terms), - sizeof_types = sizeof_diff (all_types, base_types), - sizeof_spaces = sizeof_diff (all_spaces, base_spaces)} + 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; @@ -148,9 +167,12 @@ sizeof_thms_id = g, sizeof_terms = h, sizeof_types = i, - sizeof_spaces = j} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))))) #> - let open XML.Encode - in pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int int)))))))) end; + 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