author | wenzelm |
Sun, 25 Apr 2021 22:33:15 +0200 | |
changeset 73604 | 51b291ae3e2d |
parent 73522 | b219774a71ae |
child 73716 | 00ef0f401a29 |
permissions | -rw-r--r-- |
65477 | 1 |
/* Title: Pure/ML/ml_statistics.scala |
50685 | 2 |
Author: Makarius |
3 |
||
4 |
ML runtime statistics. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
65858 | 10 |
import scala.annotation.tailrec |
51432 | 11 |
import scala.collection.mutable |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
12 |
import scala.collection.immutable.{SortedSet, SortedMap} |
50691 | 13 |
import scala.swing.{Frame, Component} |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
14 |
|
50689 | 15 |
import org.jfree.data.xy.{XYSeries, XYSeriesCollection} |
16 |
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} |
|
17 |
import org.jfree.chart.plot.PlotOrientation |
|
18 |
||
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
19 |
|
50685 | 20 |
object ML_Statistics |
21 |
{ |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
22 |
/* properties */ |
50690 | 23 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
24 |
val Now = new Properties.Double("now") |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
25 |
def now(props: Properties.T): Double = Now.unapply(props).get |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
26 |
|
50690 | 27 |
|
72138 | 28 |
/* memory status */ |
29 |
||
30 |
val Heap_Size = new Properties.Long("size_heap") |
|
31 |
val Heap_Free = new Properties.Long("size_heap_free_last_GC") |
|
32 |
val GC_Percent = new Properties.Int("GC_percent") |
|
33 |
||
34 |
sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int) |
|
35 |
{ |
|
36 |
def heap_used: Long = (heap_size - heap_free) max 0 |
|
37 |
def heap_used_fraction: Double = |
|
38 |
if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size |
|
39 |
def gc_progress: Option[Double] = |
|
40 |
if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None |
|
41 |
} |
|
42 |
||
43 |
def memory_status(props: Properties.T): Memory_Status = |
|
44 |
{ |
|
45 |
val heap_size = Heap_Size.get(props) |
|
46 |
val heap_free = Heap_Free.get(props) |
|
47 |
val gc_percent = GC_Percent.get(props) |
|
48 |
Memory_Status(heap_size, heap_free, gc_percent) |
|
49 |
} |
|
50 |
||
51 |
||
72035 | 52 |
/* monitor process */ |
53 |
||
54 |
def monitor(pid: Long, |
|
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
55 |
stats_dir: String = "", |
72035 | 56 |
delay: Time = Time.seconds(0.5), |
73340 | 57 |
consume: Properties.T => Unit = Console.println): Unit = |
72035 | 58 |
{ |
73340 | 59 |
def progress_stdout(line: String): Unit = |
72035 | 60 |
{ |
61 |
val props = |
|
62 |
Library.space_explode(',', line).flatMap((entry: String) => |
|
63 |
Library.space_explode('=', entry) match { |
|
64 |
case List(a, b) => Some((a, b)) |
|
65 |
case _ => None |
|
66 |
}) |
|
67 |
if (props.nonEmpty) consume(props) |
|
68 |
} |
|
69 |
||
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
70 |
val env_prefix = |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
71 |
if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n" |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
72 |
|
73604 | 73 |
Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + |
72044
efd169aed4dc
more robust: avoid potential problems with encoding of directory name;
wenzelm
parents:
72037
diff
changeset
|
74 |
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + |
efd169aed4dc
more robust: avoid potential problems with encoding of directory name;
wenzelm
parents:
72037
diff
changeset
|
75 |
ML_Syntax.print_double(delay.seconds)), |
73522 | 76 |
cwd = Path.ISABELLE_HOME.file) |
72035 | 77 |
.result(progress_stdout = progress_stdout, strict = false).check |
78 |
} |
|
79 |
||
80 |
||
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
81 |
/* protocol handler */ |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
82 |
|
72157 | 83 |
class Handler extends Session.Protocol_Handler |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
84 |
{ |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
85 |
private var session: Session = null |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
86 |
private var monitoring: Future[Unit] = Future.value(()) |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
87 |
|
72213 | 88 |
override def init(session: Session): Unit = synchronized |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
89 |
{ |
72213 | 90 |
this.session = session |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
91 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
92 |
|
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
93 |
override def exit(): Unit = synchronized |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
94 |
{ |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
95 |
session = null |
73367 | 96 |
monitoring.cancel() |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
97 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
98 |
|
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
99 |
private def consume(props: Properties.T): Unit = synchronized |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
100 |
{ |
72136
98dca728fc9c
removed pointless option "ML_statistics": always enabled;
wenzelm
parents:
72119
diff
changeset
|
101 |
if (session != null) { |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
72250
diff
changeset
|
102 |
val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics())) |
72149 | 103 |
session.runtime_statistics.post(Session.Runtime_Statistics(props1)) |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
104 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
105 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
106 |
|
72116 | 107 |
private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
108 |
{ |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
109 |
msg.properties match { |
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
110 |
case Markup.ML_Statistics(pid, stats_dir) => |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
111 |
monitoring = |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
112 |
Future.thread("ML_statistics") { |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
113 |
monitor(pid, stats_dir = stats_dir, consume = consume) |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72117
diff
changeset
|
114 |
} |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
115 |
true |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
116 |
case _ => false |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
117 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
118 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
119 |
|
72212 | 120 |
override val functions = List(Markup.ML_Statistics.name -> ml_statistics) |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
121 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
122 |
|
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72044
diff
changeset
|
123 |
|
69832 | 124 |
/* memory fields (mega bytes) */ |
125 |
||
126 |
def mem_print(x: Long): Option[String] = |
|
127 |
if (x == 0L) None else Some(x.toString + " M") |
|
128 |
||
129 |
def mem_scale(x: Long): Long = x / 1024 / 1024 |
|
50690 | 130 |
|
69832 | 131 |
def mem_field_scale(name: String, x: Double): Double = |
132 |
if (heap_fields._2.contains(name) || program_fields._2.contains(name)) |
|
133 |
mem_scale(x.toLong).toDouble |
|
134 |
else x |
|
135 |
||
136 |
val CODE_SIZE = "size_code" |
|
137 |
val STACK_SIZE = "size_stacks" |
|
65858 | 138 |
val HEAP_SIZE = "size_heap" |
139 |
||
65866 | 140 |
|
141 |
/* standard fields */ |
|
142 |
||
65864 | 143 |
type Fields = (String, List[String]) |
65051 | 144 |
|
145 |
val tasks_fields: Fields = |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
57869
diff
changeset
|
146 |
("Future tasks", |
68129 | 147 |
List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", |
148 |
"tasks_urgent", "tasks_total")) |
|
57869 | 149 |
|
65051 | 150 |
val workers_fields: Fields = |
57869 | 151 |
("Worker threads", List("workers_total", "workers_active", "workers_waiting")) |
152 |
||
65051 | 153 |
val GC_fields: Fields = |
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
154 |
("GCs", List("partial_GCs", "full_GCs", "share_passes")) |
50690 | 155 |
|
65051 | 156 |
val heap_fields: Fields = |
65858 | 157 |
("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", |
50690 | 158 |
"size_heap_free_last_full_GC", "size_heap_free_last_GC")) |
159 |
||
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
160 |
val program_fields: Fields = |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
161 |
("Program", List("size_code", "size_stacks")) |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
162 |
|
65051 | 163 |
val threads_fields: Fields = |
50690 | 164 |
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", |
165 |
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) |
|
166 |
||
65051 | 167 |
val time_fields: Fields = |
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
168 |
("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC")) |
51432 | 169 |
|
65051 | 170 |
val speed_fields: Fields = |
171 |
("Speed", List("speed_CPU", "speed_GC")) |
|
50690 | 172 |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
173 |
private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
174 |
|
72149 | 175 |
val java_heap_fields: Fields = |
176 |
("Java heap", List("java_heap_size", "java_heap_used")) |
|
177 |
||
178 |
val java_thread_fields: Fields = |
|
179 |
("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) |
|
180 |
||
65053 | 181 |
|
72143 | 182 |
val main_fields: List[Fields] = |
183 |
List(heap_fields, tasks_fields, workers_fields) |
|
184 |
||
72149 | 185 |
val other_fields: List[Fields] = |
186 |
List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, |
|
187 |
java_heap_fields, java_thread_fields) |
|
188 |
||
189 |
val all_fields: List[Fields] = main_fields ::: other_fields |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
190 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
191 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
192 |
/* content interpretation */ |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
193 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
194 |
final case class Entry(time: Double, data: Map[String, Double]) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
195 |
{ |
65858 | 196 |
def get(field: String): Double = data.getOrElse(field, 0.0) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
197 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
198 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
199 |
val empty: ML_Statistics = apply(Nil) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
200 |
|
72224 | 201 |
def apply(ml_statistics0: List[Properties.T], heading: String = "", |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
202 |
domain: String => Boolean = (key: String) => true): ML_Statistics = |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
203 |
{ |
73120
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents:
73031
diff
changeset
|
204 |
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field") |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
205 |
|
72224 | 206 |
val ml_statistics = ml_statistics0.sortBy(now) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
207 |
val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
208 |
val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
209 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
210 |
val fields = |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
211 |
SortedSet.empty[String] ++ |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
212 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
213 |
props <- ml_statistics.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
214 |
(x, _) <- props.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
215 |
if x != Now.name && domain(x) } yield x) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
216 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
217 |
val content = |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
218 |
{ |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
219 |
var last_edge = Map.empty[String, (Double, Double, Double)] |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
220 |
val result = new mutable.ListBuffer[ML_Statistics.Entry] |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
221 |
for (props <- ml_statistics) { |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
222 |
val time = now(props) - time_start |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
223 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
224 |
// rising edges -- relative speed |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
225 |
val speeds = |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
226 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
227 |
(key, value) <- props.iterator |
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
228 |
key1 <- time_speed.get(key) |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
229 |
if domain(key1) |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
230 |
} yield { |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
231 |
val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0)) |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
232 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
233 |
val x1 = time |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
234 |
val y1 = java.lang.Double.parseDouble(value) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
235 |
val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
236 |
|
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
237 |
if (y1 > y0) { |
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
238 |
last_edge += (key -> (x1, y1, s1)) |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
239 |
(key1, s1.toString) |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
240 |
} |
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
68129
diff
changeset
|
241 |
else (key1, s0.toString) |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
242 |
}).toList |
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
243 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
244 |
val data = |
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
245 |
SortedMap.empty[String, Double] ++ |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
246 |
(for { |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
247 |
(x, y) <- props.iterator ++ speeds.iterator |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
248 |
if x != Now.name && domain(x) |
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
249 |
z = java.lang.Double.parseDouble(y) if z != 0.0 |
69832 | 250 |
} yield { (x.intern, mem_field_scale(x, z)) }) |
65866 | 251 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
252 |
result += ML_Statistics.Entry(time, data) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
253 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
254 |
result.toList |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
255 |
} |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
256 |
|
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
257 |
new ML_Statistics(heading, fields, content, time_start, duration) |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
258 |
} |
50685 | 259 |
} |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
260 |
|
65855
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
261 |
final class ML_Statistics private( |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
262 |
val heading: String, |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
263 |
val fields: Set[String], |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
264 |
val content: List[ML_Statistics.Entry], |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
265 |
val time_start: Double, |
33b3e76114f8
store processed content instead of somewhat bulky properties;
wenzelm
parents:
65854
diff
changeset
|
266 |
val duration: Double) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
267 |
{ |
65858 | 268 |
/* content */ |
269 |
||
270 |
def maximum(field: String): Double = |
|
73359 | 271 |
content.foldLeft(0.0) { case (m, e) => m max e.get(field) } |
65858 | 272 |
|
273 |
def average(field: String): Double = |
|
274 |
{ |
|
275 |
@tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = |
|
276 |
list match { |
|
277 |
case Nil => acc |
|
278 |
case e :: es => |
|
279 |
val t = e.time |
|
280 |
sum(t, es, (t - t0) * e.get(field) + acc) |
|
281 |
} |
|
282 |
content match { |
|
283 |
case Nil => 0.0 |
|
284 |
case List(e) => e.get(field) |
|
285 |
case e :: es => sum(e.time, es, 0.0) / duration |
|
286 |
} |
|
287 |
} |
|
288 |
||
50689 | 289 |
|
290 |
/* charts */ |
|
291 |
||
73340 | 292 |
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit = |
50689 | 293 |
{ |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
294 |
data.removeAllSeries |
69832 | 295 |
for (field <- selected_fields) { |
296 |
val series = new XYSeries(field) |
|
67760
553d9ad7d679
more compact ML_Statistics, to make build_status work with less than 2GB heap;
wenzelm
parents:
65866
diff
changeset
|
297 |
content.foreach(entry => series.add(entry.time, entry.get(field))) |
50689 | 298 |
data.addSeries(series) |
299 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
300 |
} |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
301 |
|
65864 | 302 |
def chart(title: String, selected_fields: List[String]): JFreeChart = |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
303 |
{ |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
304 |
val data = new XYSeriesCollection |
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
305 |
update_data(data, selected_fields) |
50689 | 306 |
|
307 |
ChartFactory.createXYLineChart(title, "time", "value", data, |
|
308 |
PlotOrientation.VERTICAL, true, true, true) |
|
309 |
} |
|
310 |
||
65051 | 311 |
def chart(fields: ML_Statistics.Fields): JFreeChart = |
312 |
chart(fields._1, fields._2) |
|
50691 | 313 |
|
65053 | 314 |
def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = |
71601 | 315 |
fields.map(chart).foreach(c => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
53189
diff
changeset
|
316 |
GUI_Thread.later { |
50854 | 317 |
new Frame { |
51615
072a7249e1ac
separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
51432
diff
changeset
|
318 |
iconImage = GUI.isabelle_image() |
65851 | 319 |
title = heading |
50854 | 320 |
contents = Component.wrap(new ChartPanel(c)) |
321 |
visible = true |
|
322 |
} |
|
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50691
diff
changeset
|
323 |
}) |
50688
f02864682307
some support for ML statistics content interpretation;
wenzelm
parents:
50685
diff
changeset
|
324 |
} |