merged
authorwenzelm
Sat Feb 23 21:51:40 2019 +0100 (8 weeks ago ago)
changeset 7001558ef3b8a8460
parent 70011 54d19f1f0ba6
parent 70014 c3500cec8290
child 70017 9b4901bda2a7
merged
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat Feb 23 19:50:21 2019 +0000
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat Feb 23 21:51:40 2019 +0100
     1.3 @@ -116,6 +116,10 @@
     1.4            "ml_timing_elapsed",
     1.5            "ml_timing_cpu",
     1.6            "ml_timing_gc",
     1.7 +          "maximum_code",
     1.8 +          "average_code",
     1.9 +          "maximum_stack",
    1.10 +          "average_stack",
    1.11            "maximum_heap",
    1.12            "average_heap",
    1.13            "stored_heap",
    1.14 @@ -135,6 +139,10 @@
    1.15              entry.ml_timing.elapsed.ms,
    1.16              entry.ml_timing.cpu.ms,
    1.17              entry.ml_timing.gc.ms,
    1.18 +            entry.maximum_code,
    1.19 +            entry.average_code,
    1.20 +            entry.maximum_stack,
    1.21 +            entry.average_stack,
    1.22              entry.maximum_heap,
    1.23              entry.average_heap,
    1.24              entry.stored_heap,
    1.25 @@ -151,6 +159,10 @@
    1.26      afp_version: String,
    1.27      timing: Timing,
    1.28      ml_timing: Timing,
    1.29 +    maximum_code: Long,
    1.30 +    average_code: Long,
    1.31 +    maximum_stack: Long,
    1.32 +    average_stack: Long,
    1.33      maximum_heap: Long,
    1.34      average_heap: Long,
    1.35      stored_heap: Long,
    1.36 @@ -299,9 +311,13 @@
    1.37                      Build_Log.Data.ml_timing_elapsed,
    1.38                      Build_Log.Data.ml_timing_cpu,
    1.39                      Build_Log.Data.ml_timing_gc),
    1.40 -                maximum_heap = ml_stats.maximum_heap_size,
    1.41 -                average_heap = ml_stats.average_heap_size,
    1.42 -                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
    1.43 +                maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong,
    1.44 +                average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong,
    1.45 +                maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong,
    1.46 +                average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong,
    1.47 +                maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong,
    1.48 +                average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
    1.49 +                stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
    1.50                  status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
    1.51                  errors =
    1.52                    Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
    1.53 @@ -353,9 +369,6 @@
    1.54      def clean_name(name: String): String =
    1.55        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.56  
    1.57 -    def print_heap(x: Long): Option[String] =
    1.58 -      if (x == 0L) None else Some(x.toString + " M")
    1.59 -
    1.60      HTML.write_document(target_dir, "index.html",
    1.61        List(HTML.title("Isabelle build status")),
    1.62        List(HTML.chapter("Isabelle build status"),
    1.63 @@ -409,7 +422,11 @@
    1.64                        entry.timing.resources.minutes,
    1.65                        entry.ml_timing.elapsed.minutes,
    1.66                        entry.ml_timing.resources.minutes,
    1.67 -                      entry.maximum_heap,
    1.68 +                      entry.maximum_code,
    1.69 +                      entry.maximum_code,
    1.70 +                      entry.average_stack,
    1.71 +                      entry.maximum_stack,
    1.72 +                      entry.average_heap,
    1.73                        entry.average_heap,
    1.74                        entry.stored_heap).mkString(" "))))
    1.75  
    1.76 @@ -466,12 +483,12 @@
    1.77  
    1.78                val heap_plots =
    1.79                  List(
    1.80 -                  """ using 1:6 smooth sbezier title "maximum heap (smooth)" """,
    1.81 -                  """ using 1:6 smooth csplines title "maximum heap" """,
    1.82 -                  """ using 1:7 smooth sbezier title "average heap (smooth)" """,
    1.83 -                  """ using 1:7 smooth csplines title "average heap" """,
    1.84 -                  """ using 1:8 smooth sbezier title "stored heap (smooth)" """,
    1.85 -                  """ using 1:8 smooth csplines title "stored heap" """)
    1.86 +                  """ using 1:6 smooth sbezier title "heap maximum (smooth)" """,
    1.87 +                  """ using 1:6 smooth csplines title "heap maximum" """,
    1.88 +                  """ using 1:7 smooth sbezier title "heap average (smooth)" """,
    1.89 +                  """ using 1:7 smooth csplines title "heap average" """,
    1.90 +                  """ using 1:8 smooth sbezier title "heap stored (smooth)" """,
    1.91 +                  """ using 1:8 smooth csplines title "heap stored" """)
    1.92  
    1.93                def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
    1.94                {
    1.95 @@ -530,12 +547,20 @@
    1.96                      List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))),
    1.97                    HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
    1.98                    HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
    1.99 -                print_heap(session.head.maximum_heap).map(s =>
   1.100 -                  HTML.text("maximum heap:") -> HTML.text(s)).toList :::
   1.101 -                print_heap(session.head.average_heap).map(s =>
   1.102 -                  HTML.text("average heap:") -> HTML.text(s)).toList :::
   1.103 -                print_heap(session.head.stored_heap).map(s =>
   1.104 -                  HTML.text("stored heap:") -> HTML.text(s)).toList :::
   1.105 +                ML_Statistics.mem_print(session.head.maximum_code).map(s =>
   1.106 +                  HTML.text("code maximum:") -> HTML.text(s)).toList :::
   1.107 +                ML_Statistics.mem_print(session.head.average_code).map(s =>
   1.108 +                  HTML.text("code average:") -> HTML.text(s)).toList :::
   1.109 +                ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
   1.110 +                  HTML.text("stack maximum:") -> HTML.text(s)).toList :::
   1.111 +                ML_Statistics.mem_print(session.head.average_stack).map(s =>
   1.112 +                  HTML.text("stack average:") -> HTML.text(s)).toList :::
   1.113 +                ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
   1.114 +                  HTML.text("heap maximum:") -> HTML.text(s)).toList :::
   1.115 +                ML_Statistics.mem_print(session.head.average_heap).map(s =>
   1.116 +                  HTML.text("heap average:") -> HTML.text(s)).toList :::
   1.117 +                ML_Statistics.mem_print(session.head.stored_heap).map(s =>
   1.118 +                  HTML.text("heap stored:") -> HTML.text(s)).toList :::
   1.119                  proper_string(session.head.isabelle_version).map(s =>
   1.120                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
   1.121                  proper_string(session.head.afp_version).map(s =>
     2.1 --- a/src/Pure/ML/ml_process.scala	Sat Feb 23 19:50:21 2019 +0000
     2.2 +++ b/src/Pure/ML/ml_process.scala	Sat Feb 23 21:51:40 2019 +0100
     2.3 @@ -52,19 +52,6 @@
     2.4            fun subparagraph (_: string) = ();
     2.5            val ML_file = PolyML.use;
     2.6            """,
     2.7 -          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
     2.8 -            """
     2.9 -              structure FixedInt = IntInf;
    2.10 -              structure RunCall =
    2.11 -              struct
    2.12 -                open RunCall
    2.13 -                val loadWord: word * word -> word =
    2.14 -                  run_call2 RuntimeCalls.POLY_SYS_load_word;
    2.15 -                val storeWord: word * word * word -> unit =
    2.16 -                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
    2.17 -              end;
    2.18 -            """
    2.19 -          else "",
    2.20            if (Platform.is_windows)
    2.21              "fun exit 0 = OS.Process.exit OS.Process.success" +
    2.22              " | exit 1 = OS.Process.exit OS.Process.failure" +
     3.1 --- a/src/Pure/ML/ml_statistics.scala	Sat Feb 23 19:50:21 2019 +0000
     3.2 +++ b/src/Pure/ML/ml_statistics.scala	Sat Feb 23 21:51:40 2019 +0100
     3.3 @@ -25,13 +25,22 @@
     3.4    def now(props: Properties.T): Double = Now.unapply(props).get
     3.5  
     3.6  
     3.7 -  /* heap */
     3.8 +  /* memory fields (mega bytes) */
     3.9 +
    3.10 +  def mem_print(x: Long): Option[String] =
    3.11 +    if (x == 0L) None else Some(x.toString + " M")
    3.12 +
    3.13 +  def mem_scale(x: Long): Long = x / 1024 / 1024
    3.14  
    3.15 +  def mem_field_scale(name: String, x: Double): Double =
    3.16 +    if (heap_fields._2.contains(name) || program_fields._2.contains(name))
    3.17 +      mem_scale(x.toLong).toDouble
    3.18 +    else x
    3.19 +
    3.20 +  val CODE_SIZE = "size_code"
    3.21 +  val STACK_SIZE = "size_stacks"
    3.22    val HEAP_SIZE = "size_heap"
    3.23  
    3.24 -  def heap_scale(x: Long): Long = x / 1024 / 1024
    3.25 -  def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong
    3.26 -
    3.27  
    3.28    /* standard fields */
    3.29  
    3.30 @@ -134,7 +143,7 @@
    3.31                (x, y) <- props.iterator ++ speeds.iterator
    3.32                if x != Now.name && domain(x)
    3.33                z = java.lang.Double.parseDouble(y) if z != 0.0
    3.34 -            } yield { (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z) })
    3.35 +            } yield { (x.intern, mem_field_scale(x, z)) })
    3.36  
    3.37          result += ML_Statistics.Entry(time, data)
    3.38        }
    3.39 @@ -173,19 +182,14 @@
    3.40      }
    3.41    }
    3.42  
    3.43 -  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
    3.44 -  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
    3.45 -
    3.46  
    3.47    /* charts */
    3.48  
    3.49    def update_data(data: XYSeriesCollection, selected_fields: List[String])
    3.50    {
    3.51      data.removeAllSeries
    3.52 -    for {
    3.53 -      field <- selected_fields.iterator
    3.54 -      series = new XYSeries(field)
    3.55 -    } {
    3.56 +    for (field <- selected_fields) {
    3.57 +      val series = new XYSeries(field)
    3.58        content.foreach(entry => series.add(entry.time, entry.get(field)))
    3.59        data.addSeries(series)
    3.60      }