# HG changeset patch # User wenzelm # Date 1674918523 -3600 # Node ID ceee2a01322eb7f4dbd189f8dd912a88d444648e # Parent 8c14be9beb58fa603e100942317ebaa8d61a471b clarified signature: more explicit types; scale chart output, instead of stored data; diff -r 8c14be9beb58 -r ceee2a01322e src/Pure/Admin/build_status.scala --- 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 ::: diff -r 8c14be9beb58 -r ceee2a01322e src/Pure/ML/ml_statistics.scala --- 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) } }