--- a/src/Pure/Tools/profiling.scala Mon Jul 24 16:11:16 2023 +0200
+++ b/src/Pure/Tools/profiling.scala Mon Jul 24 21:05:11 2023 +0200
@@ -31,6 +31,7 @@
sealed case class Session_Statistics(
theories: Int = 0,
+ garbage_theories: Int = 0,
locales: Int = 0,
locale_thms: Int = 0,
global_thms: Int = 0,
@@ -48,21 +49,22 @@
private val decode_result: XML.Decode.T[Session_Statistics] =
(body: XML.Body) =>
{
- val (a, (b, (c, (d, (e, (f, (g, (h, i)))))))) = {
+ val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = {
import XML.Decode._
- pair(int, pair(int, pair(int, pair(int,
- pair(long, pair(long, pair(long, pair(long, long))))))))(body)
+ pair(int, pair(int, pair(int, pair(int, pair(int,
+ pair(long, pair(long, pair(long, pair(long, long)))))))))(body)
}
Session_Statistics(
theories = a,
- locales = b,
- locale_thms = c,
- global_thms = d,
- sizeof_thys_id = Space.bytes(e),
- sizeof_thms_id = Space.bytes(f),
- sizeof_terms = Space.bytes(g),
- sizeof_types = Space.bytes(h),
- sizeof_spaces = Space.bytes(i))
+ garbage_theories = b,
+ locales = c,
+ locale_thms = d,
+ global_thms = e,
+ sizeof_thys_id = Space.bytes(f),
+ sizeof_thms_id = Space.bytes(g),
+ sizeof_terms = Space.bytes(h),
+ sizeof_types = Space.bytes(i),
+ sizeof_spaces = Space.bytes(j))
}
def make(
@@ -91,6 +93,7 @@
new Statistics(parent = parent, session = session_name,
theories = session.theories,
+ garbage_theories = session.garbage_theories,
locales = session.locales,
locale_thms = session.locale_thms,
global_thms = session.global_thms,
@@ -107,6 +110,7 @@
val header0: List[String] =
List(
"theories",
+ "garbage_theories%",
"locales",
"locale_thms",
"global_thms",
@@ -127,6 +131,7 @@
val parent: Option[Statistics] = None,
val session: String = "",
val theories: Int = 0,
+ val garbage_theories: Int = 0,
val locales: Int = 0,
val locale_thms: Int = 0,
val global_thms: Int = 0,
@@ -137,6 +142,9 @@
val types_size: Space = Space.zero,
val spaces_size: Space = Space.zero
) {
+ def garbage_theories_percentage: Percentage =
+ percentage(garbage_theories, theories + garbage_theories)
+
private def size_percentage(space: Space): Percentage =
percentage_space(space, heap_size)
@@ -146,6 +154,7 @@
val fields0: List[Any] =
List(
theories,
+ garbage_theories_percentage.toString,
locales,
locale_thms,
global_thms,
@@ -168,6 +177,7 @@
new Statistics(parent = None,
session = session,
theories = other.cumulative.theories + theories,
+ garbage_theories = other.cumulative.garbage_theories + garbage_theories,
locales = other.cumulative.locales + locales,
locale_thms = other.cumulative.locale_thms + locale_thms,
global_thms = other.cumulative.global_thms + global_thms,
--- a/src/Tools/profiling.ML Mon Jul 24 16:11:16 2023 +0200
+++ b/src/Tools/profiling.ML Mon Jul 24 21:05:11 2023 +0200
@@ -13,6 +13,7 @@
val all_thms: theory -> thm list
type session_statistics =
{theories: int,
+ garbage_theories: int,
locales: int,
locale_thms: int,
global_thms: int,
@@ -84,6 +85,7 @@
type session_statistics =
{theories: int,
+ garbage_theories: int,
locales: int,
locale_thms: int,
global_thms: int,
@@ -103,6 +105,7 @@
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;
@@ -111,8 +114,12 @@
types = all_types, 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;
+
+ val n = length loaded_thys;
+ val m = length loaded_context_thys - n;
in
- {theories = length loaded_thys,
+ {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),
@@ -133,16 +140,17 @@
val encode_result : session_statistics XML.Encode.T =
(fn {theories = a,
- locales = b,
- locale_thms = c,
- global_thms = d,
- sizeof_thys_id = e,
- sizeof_thms_id = f,
- sizeof_terms = g,
- sizeof_types = h,
- sizeof_spaces = i} => (a, (b, (c, (d, (e, (f, (g, (h, i))))))))) #>
+ 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_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 int))))))) end;
+ in pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int int)))))))) end;
in