# HG changeset patch # User wenzelm # Date 1550661040 -3600 # Node ID 8c587dd44f51e67e1314b5fffe731f0baa8ca3a5 # Parent 8432b771f12e82b5df36076ef58d9212040d8e66 updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8); diff -r 8432b771f12e -r 8c587dd44f51 Admin/components/components.sha1 --- 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 diff -r 8432b771f12e -r 8c587dd44f51 Admin/components/main --- 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 diff -r 8432b771f12e -r 8c587dd44f51 Admin/polyml/README --- 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 diff -r 8432b771f12e -r 8c587dd44f51 Admin/polyml/settings --- 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" diff -r 8432b771f12e -r 8c587dd44f51 NEWS --- 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) --------------------------------- diff -r 8432b771f12e -r 8c587dd44f51 src/Pure/Admin/build_status.scala --- 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), diff -r 8432b771f12e -r 8c587dd44f51 src/Pure/ML/ml_statistics.ML --- 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 diff -r 8432b771f12e -r 8c587dd44f51 src/Pure/ML/ml_statistics.scala --- 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 =