# HG changeset patch # User wenzelm # Date 1550953989 -3600 # Node ID b614e3e4146ad22d863e337e0e38233003b2971f # Parent b35c3839d5d1d65e0edb4f5825c5a579fac3bd64 more memory fields; diff -r b35c3839d5d1 -r b614e3e4146a src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Sat Feb 23 21:32:29 2019 +0100 +++ b/src/Pure/Admin/build_status.scala Sat Feb 23 21:33:09 2019 +0100 @@ -116,6 +116,10 @@ "ml_timing_elapsed", "ml_timing_cpu", "ml_timing_gc", + "maximum_code", + "average_code", + "maximum_stack", + "average_stack", "maximum_heap", "average_heap", "stored_heap", @@ -135,6 +139,10 @@ entry.ml_timing.elapsed.ms, entry.ml_timing.cpu.ms, entry.ml_timing.gc.ms, + entry.maximum_code, + entry.average_code, + entry.maximum_stack, + entry.average_stack, entry.maximum_heap, entry.average_heap, entry.stored_heap, @@ -151,6 +159,10 @@ 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, @@ -299,9 +311,13 @@ Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc), - maximum_heap = ml_stats.maximum_heap_size, - average_heap = ml_stats.average_heap_size, - stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)), + 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)), status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors), @@ -353,9 +369,6 @@ def clean_name(name: String): String = name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) - def print_heap(x: Long): Option[String] = - if (x == 0L) None else Some(x.toString + " M") - HTML.write_document(target_dir, "index.html", List(HTML.title("Isabelle build status")), List(HTML.chapter("Isabelle build status"), @@ -409,7 +422,11 @@ entry.timing.resources.minutes, entry.ml_timing.elapsed.minutes, entry.ml_timing.resources.minutes, - entry.maximum_heap, + entry.maximum_code, + entry.maximum_code, + entry.average_stack, + entry.maximum_stack, + entry.average_heap, entry.average_heap, entry.stored_heap).mkString(" ")))) @@ -530,11 +547,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)) ::: - print_heap(session.head.maximum_heap).map(s => + ML_Statistics.mem_print(session.head.maximum_code).map(s => + HTML.text("maximum code:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.average_code).map(s => + HTML.text("average code:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.maximum_stack).map(s => + HTML.text("maximum stack:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.average_stack).map(s => + HTML.text("average stack:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.maximum_heap).map(s => HTML.text("maximum heap:") -> HTML.text(s)).toList ::: - print_heap(session.head.average_heap).map(s => + ML_Statistics.mem_print(session.head.average_heap).map(s => HTML.text("average heap:") -> HTML.text(s)).toList ::: - print_heap(session.head.stored_heap).map(s => + ML_Statistics.mem_print(session.head.stored_heap).map(s => HTML.text("stored heap:") -> HTML.text(s)).toList ::: proper_string(session.head.isabelle_version).map(s => HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: diff -r b35c3839d5d1 -r b614e3e4146a src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Sat Feb 23 21:32:29 2019 +0100 +++ b/src/Pure/ML/ml_statistics.scala Sat Feb 23 21:33:09 2019 +0100 @@ -25,13 +25,22 @@ def now(props: Properties.T): Double = Now.unapply(props).get - /* heap */ + /* 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 + def mem_field_scale(name: String, x: Double): Double = + if (heap_fields._2.contains(name) || program_fields._2.contains(name)) + mem_scale(x.toLong).toDouble + else x + + val CODE_SIZE = "size_code" + val STACK_SIZE = "size_stacks" val HEAP_SIZE = "size_heap" - def heap_scale(x: Long): Long = x / 1024 / 1024 - def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong - /* standard fields */ @@ -134,7 +143,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, if (heap_fields._2.contains(x)) heap_scale(z) else z) }) + } yield { (x.intern, mem_field_scale(x, z)) }) result += ML_Statistics.Entry(time, data) } @@ -173,19 +182,14 @@ } } - def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong - def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong - /* charts */ def update_data(data: XYSeriesCollection, selected_fields: List[String]) { data.removeAllSeries - for { - field <- selected_fields.iterator - series = new XYSeries(field) - } { + for (field <- selected_fields) { + val series = new XYSeries(field) content.foreach(entry => series.add(entry.time, entry.get(field))) data.addSeries(series) }