# HG changeset patch # User immler # Date 1550957518 18000 # Node ID 9b4901bda2a78043482aeab04b90bf72ce3c628f # Parent b1dfaa25130e3500146959f5df81beba46b91953# Parent 58ef3b8a84600dd1b17733921b0f2a0aaed2f81d merged diff -r b1dfaa25130e -r 9b4901bda2a7 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Sat Feb 23 16:03:32 2019 -0500 +++ b/src/Pure/Admin/build_status.scala Sat Feb 23 16:31:58 2019 -0500 @@ -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(" ")))) @@ -466,12 +483,12 @@ val heap_plots = List( - """ using 1:6 smooth sbezier title "maximum heap (smooth)" """, - """ using 1:6 smooth csplines title "maximum heap" """, - """ using 1:7 smooth sbezier title "average heap (smooth)" """, - """ using 1:7 smooth csplines title "average heap" """, - """ using 1:8 smooth sbezier title "stored heap (smooth)" """, - """ using 1:8 smooth csplines title "stored heap" """) + """ using 1:6 smooth sbezier title "heap maximum (smooth)" """, + """ using 1:6 smooth csplines title "heap maximum" """, + """ using 1:7 smooth sbezier title "heap average (smooth)" """, + """ using 1:7 smooth csplines title "heap average" """, + """ using 1:8 smooth sbezier title "heap stored (smooth)" """, + """ using 1:8 smooth csplines title "heap stored" """) def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = { @@ -530,12 +547,20 @@ 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 => - HTML.text("maximum heap:") -> HTML.text(s)).toList ::: - print_heap(session.head.average_heap).map(s => - HTML.text("average heap:") -> HTML.text(s)).toList ::: - print_heap(session.head.stored_heap).map(s => - HTML.text("stored heap:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.maximum_code).map(s => + HTML.text("code maximum:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.average_code).map(s => + HTML.text("code average:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.maximum_stack).map(s => + HTML.text("stack maximum:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.average_stack).map(s => + HTML.text("stack average:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.maximum_heap).map(s => + HTML.text("heap maximum:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.average_heap).map(s => + HTML.text("heap average:") -> HTML.text(s)).toList ::: + ML_Statistics.mem_print(session.head.stored_heap).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 ::: proper_string(session.head.afp_version).map(s => diff -r b1dfaa25130e -r 9b4901bda2a7 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sat Feb 23 16:03:32 2019 -0500 +++ b/src/Pure/ML/ml_process.scala Sat Feb 23 16:31:58 2019 -0500 @@ -52,19 +52,6 @@ fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, - if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") - """ - structure FixedInt = IntInf; - structure RunCall = - struct - open RunCall - val loadWord: word * word -> word = - run_call2 RuntimeCalls.POLY_SYS_load_word; - val storeWord: word * word * word -> unit = - run_call3 RuntimeCalls.POLY_SYS_assign_word; - end; - """ - else "", if (Platform.is_windows) "fun exit 0 = OS.Process.exit OS.Process.success" + " | exit 1 = OS.Process.exit OS.Process.failure" + diff -r b1dfaa25130e -r 9b4901bda2a7 src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Sat Feb 23 16:03:32 2019 -0500 +++ b/src/Pure/ML/ml_statistics.scala Sat Feb 23 16:31:58 2019 -0500 @@ -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) }