--- a/src/Pure/Admin/build_status.scala Sat Jan 28 16:06:38 2023 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Jan 28 16:08:43 2023 +0100
@@ -109,9 +109,9 @@
def check_heap: Boolean =
finished_entries_size >= 3 &&
finished_entries.forall(entry =>
- entry.maximum_heap > 0 ||
- entry.average_heap > 0 ||
- entry.stored_heap > 0)
+ entry.maximum_heap.is_proper ||
+ entry.average_heap.is_proper ||
+ entry.stored_heap.is_proper)
def make_csv: CSV.File = {
val header =
@@ -170,13 +170,13 @@
afp_version: String,
timing: Timing,
ml_timing: Timing,
- maximum_code: Long,
- average_code: Long,
- maximum_stack: Long,
- average_stack: Long,
- maximum_heap: Long,
- average_heap: Long,
- stored_heap: Long,
+ maximum_code: Space,
+ average_code: Space,
+ maximum_stack: Space,
+ average_stack: Space,
+ maximum_heap: Space,
+ average_heap: Space,
+ stored_heap: Space,
status: Build_Log.Session_Status.Value,
errors: List[String]
) {
@@ -320,13 +320,13 @@
Build_Log.Data.ml_timing_elapsed,
Build_Log.Data.ml_timing_cpu,
Build_Log.Data.ml_timing_gc),
- maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong,
- average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong,
- maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong,
- average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong,
- maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong,
- average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
- stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
+ maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)),
+ average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)),
+ maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)),
+ average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)),
+ maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)),
+ average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)),
+ stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)),
status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
errors =
Build_Log.uncompress_errors(
@@ -430,13 +430,13 @@
entry.timing.resources.minutes.toString,
entry.ml_timing.elapsed.minutes.toString,
entry.ml_timing.resources.minutes.toString,
- entry.maximum_code.toString,
- entry.average_code.toString,
- entry.maximum_stack.toString,
- entry.average_stack.toString,
- entry.maximum_heap.toString,
- entry.average_heap.toString,
- entry.stored_heap.toString).mkString(" "))))
+ entry.maximum_code.MiB.toString,
+ entry.average_code.MiB.toString,
+ entry.maximum_stack.MiB.toString,
+ entry.average_stack.MiB.toString,
+ entry.maximum_heap.MiB.toString,
+ entry.average_heap.MiB.toString,
+ entry.stored_heap.MiB.toString).mkString(" "))))
val max_time =
(session.finished_entries.foldLeft(0.0) {
@@ -554,19 +554,19 @@
List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))),
HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
- ML_Statistics.mem_print(session.head.maximum_code).map(s =>
+ session.head.maximum_code.print_relevant.map(s =>
HTML.text("code maximum:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.average_code).map(s =>
+ session.head.average_code.print_relevant.map(s =>
HTML.text("code average:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
+ session.head.maximum_stack.print_relevant.map(s =>
HTML.text("stack maximum:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.average_stack).map(s =>
+ session.head.average_stack.print_relevant.map(s =>
HTML.text("stack average:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
+ session.head.maximum_heap.print_relevant.map(s =>
HTML.text("heap maximum:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.average_heap).map(s =>
+ session.head.average_heap.print_relevant.map(s =>
HTML.text("heap average:") -> HTML.text(s)).toList :::
- ML_Statistics.mem_print(session.head.stored_heap).map(s =>
+ session.head.stored_heap.print_relevant.map(s =>
HTML.text("heap stored:") -> HTML.text(s)).toList :::
proper_string(session.head.isabelle_version).map(s =>
HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
--- a/src/Pure/ML/ml_statistics.scala Sat Jan 28 16:06:38 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sat Jan 28 16:08:43 2023 +0100
@@ -108,12 +108,7 @@
}
- /* memory fields (mega bytes) */
-
- def mem_print(x: Long): Option[String] =
- if (x == 0L) None else Some(x.toString + " M")
-
- def mem_scale(x: Long): Long = x / 1024 / 1024
+ /* memory fields */
val scale_MiB: Double = 1.0 / 1024 / 1024
@@ -235,7 +230,7 @@
(x, y) <- props.iterator ++ speeds.iterator
if x != Now.name && domain(x)
z = java.lang.Double.parseDouble(y) if z != 0.0
- } yield { (x.intern, field_scale(x, z)) })
+ } yield { (x.intern, z) })
result += ML_Statistics.Entry(time, data)
}
@@ -285,7 +280,7 @@
data.removeAllSeries()
for (field <- selected_fields) {
val series = new XYSeries(field)
- content.foreach(e => series.add(e.time, e.get(field)))
+ content.foreach(e => series.add(e.time, ML_Statistics.field_scale(field, e.get(field))))
data.addSeries(series)
}
}