--- a/src/Pure/Tools/profiling.scala Thu Jul 13 10:36:27 2023 +0200
+++ b/src/Pure/Tools/profiling.scala Thu Jul 13 13:04:15 2023 +0200
@@ -27,37 +27,13 @@
}
- /* session and theory statistics */
-
- object Theory_Statistics {
- def sum(name: String, theories: List[Theory_Statistics]): Theory_Statistics =
- theories.foldLeft(Theory_Statistics(name = name))(_ + _)
+ /* session statistics */
- val header: List[String] =
- List("name", "locales", "locale_thms", "global_thms",
- "locale_thms_percentage", "global_thms_percentage")
- }
-
- sealed case class Theory_Statistics(
- name: String = "",
+ sealed case class Session_Statistics(
+ theories: Int = 0,
locales: Int = 0,
locale_thms: Int = 0,
- global_thms: Int = 0
- ) {
- def + (other: Theory_Statistics): Theory_Statistics =
- copy(
- locales = other.locales + locales,
- locale_thms = other.locale_thms + locale_thms,
- global_thms = other.global_thms + global_thms)
-
- def thms: Int = locale_thms + global_thms
-
- def fields: List[Any] =
- List(name, locales, locale_thms, global_thms,
- percentage(locale_thms, thms), percentage(global_thms, thms))
- }
-
- sealed case class Session_Statistics(
+ global_thms: Int = 0,
sizeof_thys_id: Space = Space.zero,
sizeof_thms_id: Space = Space.zero,
sizeof_terms: Space = Space.zero,
@@ -69,53 +45,37 @@
(args: List[String]) =>
{ import XML.Encode._; list(string)(args) }
- private val decode_theories_result: XML.Decode.T[List[Theory_Statistics]] =
- (body: XML.Body) =>
- { import XML.Decode._; list(pair(string, pair(int, pair(int, int))))(body) } map {
- case (a, (b, (c, d))) =>
- Theory_Statistics(
- name = a,
- locales = b,
- locale_thms = c,
- global_thms = d)
- }
-
- private val decode_session_result: XML.Decode.T[Session_Statistics] =
+ private val decode_result: XML.Decode.T[Session_Statistics] =
(body: XML.Body) =>
{
- val (a, (b, (c, (d, e)))) = {
+ val (a, (b, (c, (d, (e, (f, (g, (h, i)))))))) = {
import XML.Decode._
- pair(long, pair(long, pair(long, pair(long, long))))(body)
+ pair(int, pair(int, pair(int, pair(int,
+ pair(long, pair(long, pair(long, pair(long, long))))))))(body)
}
Session_Statistics(
- sizeof_thys_id = Space.bytes(a),
- sizeof_thms_id = Space.bytes(b),
- sizeof_terms = Space.bytes(c),
- sizeof_types = Space.bytes(d),
- sizeof_spaces = Space.bytes(e))
+ 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))
}
- private val decode_result: XML.Decode.T[(List[Theory_Statistics], Session_Statistics)] =
- (body: XML.Body) =>
- { import XML.Decode._; pair(decode_theories_result, decode_session_result)(body) }
def make(
store: Store,
session_background: Sessions.Background,
- parent: Option[Statistics] = None,
- anonymous_theories: Boolean = false
+ parent: Option[Statistics] = None
): Statistics = {
val session_base = session_background.base
val session_name = session_base.session_name
val sessions_structure = session_background.sessions_structure
- val theories_name = session_base.used_theories.map(p => p._1.theory)
- val theories_index =
- Map.from(
- for ((name, i) <- theories_name.zipWithIndex)
- yield name -> String.format(Locale.ROOT, "%s.%04d", session_name, i + 1))
-
- val (theories0, session) = {
- val args = theories_name
+ val session = {
+ val args = session_base.used_theories.map(p => p._1.theory)
val eval_args =
List("--eval", "use_thy " + ML_Syntax.print_string_bytes("~~/src/Tools/Profiling"))
Isabelle_System.with_tmp_dir("profiling") { dir =>
@@ -129,11 +89,11 @@
}
}
- val theories =
- if (anonymous_theories) theories0.map(a => a.copy(name = theories_index(a.name)))
- else theories0
-
- new Statistics(parent = parent, session_name = session_name, theories = theories,
+ new Statistics(parent = parent, session = session_name,
+ theories = session.theories,
+ locales = session.locales,
+ locale_thms = session.locale_thms,
+ global_thms = session.global_thms,
heap_size = Space.bytes(store.the_heap(session_name).file.length),
thys_id_size = session.sizeof_thys_id,
thms_id_size = session.sizeof_thms_id,
@@ -144,21 +104,31 @@
val empty: Statistics = new Statistics()
- val header: List[String] =
- Theory_Statistics.header :::
- List("heap_size",
- "thys_id_size_percentage",
- "thms_id_size_percentage",
- "terms_size_percentage",
- "types_size_percentage",
- "spaces_size_percentage")
- val header_cumulative: List[String] = header ::: header.tail.map(_ + "_cumulative")
+ val header0: List[String] =
+ List(
+ "theories",
+ "locales",
+ "locale_thms",
+ "global_thms",
+ "locale_thms_percentage",
+ "global_thms_percentage",
+ "heap_size",
+ "thys_id_size_percentage",
+ "thms_id_size_percentage",
+ "terms_size_percentage",
+ "types_size_percentage",
+ "spaces_size_percentage")
+
+ def header: List[String] = "session" :: header0 ::: header0.map(_ + "_cumulative")
}
final class Statistics private(
val parent: Option[Statistics] = None,
- val session_name: String = "",
- val theories: List[Theory_Statistics] = Nil,
+ val session: String = "",
+ val theories: Int = 0,
+ val locales: Int = 0,
+ val locale_thms: Int = 0,
+ val global_thms: Int = 0,
val heap_size: Space = Space.zero,
val thys_id_size: Space = Space.zero,
val thms_id_size: Space = Space.zero,
@@ -169,26 +139,36 @@
private def size_percentage(space: Space): Percentage =
percentage_space(space, heap_size)
- def fields: List[Any] =
- session.fields :::
- List(heap_size.print,
- size_percentage(thys_id_size).toString,
- size_percentage(thms_id_size).toString,
- size_percentage(terms_size).toString,
- size_percentage(types_size).toString,
- size_percentage(spaces_size).toString)
- def fields_cumulative: List[Any] = fields ::: cumulative.fields.tail
+ private def thms_percentage(thms: Int): Percentage =
+ percentage(thms, locale_thms + global_thms)
- lazy val session: Theory_Statistics =
- Theory_Statistics.sum(session_name, theories)
+ def fields0: List[Any] =
+ List(
+ theories,
+ locales,
+ locale_thms,
+ global_thms,
+ thms_percentage(locale_thms).toString,
+ thms_percentage(global_thms).toString,
+ heap_size.print,
+ size_percentage(thys_id_size).toString,
+ size_percentage(thms_id_size).toString,
+ size_percentage(terms_size).toString,
+ size_percentage(types_size).toString,
+ size_percentage(spaces_size).toString)
+
+ def fields: List[Any] = session :: fields0 ::: cumulative.fields0
lazy val cumulative: Statistics =
parent match {
case None => this
case Some(other) =>
new Statistics(parent = None,
- session_name = session_name,
- theories = other.cumulative.theories ::: theories,
+ session = session,
+ theories = other.cumulative.theories + theories,
+ locales = other.cumulative.locales + locales,
+ locale_thms = other.cumulative.locale_thms + locale_thms,
+ global_thms = other.cumulative.global_thms + global_thms,
heap_size = other.cumulative.heap_size + heap_size,
thys_id_size = other.cumulative.thys_id_size + thys_id_size,
thms_id_size = other.cumulative.thms_id_size + thms_id_size,
@@ -197,7 +177,7 @@
spaces_size = other.cumulative.spaces_size + spaces_size)
}
- override def toString: String = "Statistics(" + session_name + ")"
+ override def toString: String = "Statistics(" + session + ")"
}
@@ -210,14 +190,8 @@
): Unit = {
progress.echo("Output directory " + output_dir.absolute)
Isabelle_System.make_directory(output_dir)
-
- val sessions_records =
- for (stats <- sessions) yield {
- CSV.File("session_" + stats.session_name, Theory_Statistics.header,
- stats.theories.map(thy => CSV.Record(thy.fields:_*))).write(output_dir)
- CSV.Record(stats.fields_cumulative:_*)
- }
- CSV.File("all_sessions", Statistics.header_cumulative, sessions_records).write(output_dir)
+ val csv_records = for (session <- sessions) yield CSV.Record(session.fields:_*)
+ CSV.File("sessions", Statistics.header, csv_records).write(output_dir)
}
}
@@ -228,8 +202,7 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
numa_shuffling: Boolean = false,
- max_jobs: Int = 1,
- anonymous_theories: Boolean = false
+ max_jobs: Int = 1
): Results = {
/* sessions structure */
@@ -286,8 +259,7 @@
val stats =
Statistics.make(store,
build_results.deps.background(session_name),
- parent = parent,
- anonymous_theories = anonymous_theories)
+ parent = parent)
seen += (session_name -> stats)
stats
}
@@ -314,7 +286,6 @@
var dirs: List[Path] = Nil
var session_groups: List[String] = Nil
var max_jobs = 1
- var anonymous_theories = false
var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -332,7 +303,6 @@
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
- -n anonymous theories: suppress details of private projects
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose
-x NAME exclude session NAME and all descendants
@@ -348,7 +318,6 @@
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
- "n" -> (_ => anonymous_theories = true),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
@@ -371,8 +340,7 @@
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = Host.numa_check(progress, numa_shuffling),
- max_jobs = max_jobs,
- anonymous_theories = anonymous_theories)
+ max_jobs = max_jobs)
}
results.output(output_dir = output_dir.absolute, progress = progress)