--- a/Admin/components/components.sha1 Wed Feb 20 07:57:29 2019 +0100
+++ b/Admin/components/components.sha1 Wed Feb 20 12:10:40 2019 +0100
@@ -197,6 +197,7 @@
1430533c09b17f8be73798a47a5f409d43a04cf4 polyml-5.7.1-8.tar.gz
171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
+51e024225b460900da5279f0b91b217085f98cf9 polyml-5.8-20190220.tar.gz
49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz
2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz
a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz
--- a/Admin/components/main Wed Feb 20 07:57:29 2019 +0100
+++ b/Admin/components/main Wed Feb 20 12:10:40 2019 +0100
@@ -12,7 +12,7 @@
kodkodi-1.5.2-1
nunchaku-0.5
opam-1.2.2
-polyml-test-8fda4fd22441
+polyml-5.8-20190220
postgresql-42.2.5
scala-2.12.8
smbc-0.4.1
--- a/Admin/polyml/README Wed Feb 20 07:57:29 2019 +0100
+++ b/Admin/polyml/README Wed Feb 20 12:10:40 2019 +0100
@@ -3,7 +3,7 @@
This compilation of Poly/ML (https://www.polyml.org) is based on the
repository version
-https://github.com/polyml/polyml/commit/8fda4fd22441 (master).
+https://github.com/polyml/polyml/commit/c3a630fcc6a6 (master).
The Isabelle repository provides the administrative tool
"build_polyml", which can be used in the polyml component directory as
@@ -48,4 +48,4 @@
Makarius
- 17-Feb-2019
+ 20-Feb-2019
--- a/Admin/polyml/settings Wed Feb 20 07:57:29 2019 +0100
+++ b/Admin/polyml/settings Wed Feb 20 12:10:40 2019 +0100
@@ -12,6 +12,6 @@
ML_OPTIONS="--minheap 500"
fi
-ML_SYSTEM=polyml-5.7.1
+ML_SYSTEM=polyml-5.8
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_SOURCES="$POLYML_HOME/src"
--- a/NEWS Wed Feb 20 07:57:29 2019 +0100
+++ b/NEWS Wed Feb 20 12:10:40 2019 +0100
@@ -290,6 +290,16 @@
* System option "checkpoint" has been discontinued: obsolete thanks to
improved memory management in Poly/ML.
+* Poly/ML 5.8 allows to use the native x86_64 platform without the full
+overhead of 64-bit values everywhere. This special x86_64_32 mode
+provides up to 16GB ML heap, while program code and stacks are allocated
+elsewhere. Thus approx. 5 times more memory is available for
+applications compared to old x86 mode (which is no longer used by
+Isabelle). The switch to the x86_64 CPU architecture also avoids
+compatibility problems with Linux and macOS, where 32-bit applications
+are gradually phased out.
+
+
New in Isabelle2018 (August 2018)
---------------------------------
--- a/src/Pure/Admin/build_status.scala Wed Feb 20 07:57:29 2019 +0100
+++ b/src/Pure/Admin/build_status.scala Wed Feb 20 12:10:40 2019 +0100
@@ -58,8 +58,8 @@
image_size: (Int, Int) = default_image_size)
{
val ml_statistics_domain =
- Iterator(ML_Statistics.heap_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).
- flatMap(_._2).toSet
+ Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields,
+ ML_Statistics.workers_fields).flatMap(_._2).toSet
val data =
read_data(options, progress = progress, profiles = profiles,
@@ -494,7 +494,8 @@
List(gnuplot(plot_name("heap"), heap_plots, "[0:]"))
else Nil) :::
(if (session.ml_statistics.content.nonEmpty)
- List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) :::
+ List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields),
+ jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) :::
(if (session.threads > 1)
List(
jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields),
--- a/src/Pure/ML/ml_statistics.ML Wed Feb 20 07:57:29 2019 +0100
+++ b/src/Pure/ML/ml_statistics.ML Wed Feb 20 12:10:40 2019 +0100
@@ -17,19 +17,24 @@
val
{gcFullGCs,
gcPartialGCs,
+ gcSharePasses,
sizeAllocation,
sizeAllocationFree,
+ sizeCode,
sizeHeap,
sizeHeapFreeLastFullGC,
sizeHeapFreeLastGC,
+ sizeStacks,
threadsInML,
threadsTotal,
threadsWaitCondVar,
threadsWaitIO,
threadsWaitMutex,
threadsWaitSignal,
+ timeGCReal,
timeGCSystem,
timeGCUser,
+ timeNonGCReal,
timeNonGCSystem,
timeNonGCUser,
userCounters} = PolyML.Statistics.getLocalStats ();
@@ -40,17 +45,22 @@
in
[("full_GCs", Value.print_int gcFullGCs),
("partial_GCs", Value.print_int gcPartialGCs),
+ ("share_passes", Value.print_int gcSharePasses),
("size_allocation", Value.print_int sizeAllocation),
("size_allocation_free", Value.print_int sizeAllocationFree),
+ ("size_code", Value.print_int sizeCode),
("size_heap", Value.print_int sizeHeap),
("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
+ ("size_stacks", Value.print_int sizeStacks),
("threads_in_ML", Value.print_int threadsInML),
("threads_total", Value.print_int threadsTotal),
("threads_wait_condvar", Value.print_int threadsWaitCondVar),
("threads_wait_IO", Value.print_int threadsWaitIO),
("threads_wait_mutex", Value.print_int threadsWaitMutex),
("threads_wait_signal", Value.print_int threadsWaitSignal),
+ ("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)),
+ ("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)),
("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
user_counters
--- a/src/Pure/ML/ml_statistics.scala Wed Feb 20 07:57:29 2019 +0100
+++ b/src/Pure/ML/ml_statistics.scala Wed Feb 20 12:10:40 2019 +0100
@@ -46,25 +46,30 @@
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
val GC_fields: Fields =
- ("GCs", List("partial_GCs", "full_GCs"))
+ ("GCs", List("partial_GCs", "full_GCs", "share_passes"))
val heap_fields: Fields =
("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
"size_heap_free_last_full_GC", "size_heap_free_last_GC"))
+ val program_fields: Fields =
+ ("Program", List("size_code", "size_stacks"))
+
val threads_fields: Fields =
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
val time_fields: Fields =
- ("Time", List("time_CPU", "time_GC"))
+ ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
val speed_fields: Fields =
("Speed", List("speed_CPU", "speed_GC"))
+ private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
+
val all_fields: List[Fields] =
- List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
+ List(tasks_fields, workers_fields, GC_fields, heap_fields, program_fields, threads_fields,
time_fields, speed_fields)
val main_fields: List[Fields] =
@@ -107,21 +112,20 @@
val speeds =
(for {
(key, value) <- props.iterator
- a <- Library.try_unprefix("time", key)
- b = "speed" + a if domain(b)
- }
- yield {
- val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
+ key1 <- time_speed.get(key)
+ if domain(key1)
+ } yield {
+ val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0))
val x1 = time
val y1 = java.lang.Double.parseDouble(value)
val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
if (y1 > y0) {
- last_edge += (a -> (x1, y1, s1))
- (b, s1.toString)
+ last_edge += (key -> (x1, y1, s1))
+ (key1, s1.toString)
}
- else (b, s0.toString)
+ else (key1, s0.toString)
}).toList
val data =