updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
authorwenzelm
Wed Feb 20 12:10:40 2019 +0100 (6 months ago)
changeset 698228c587dd44f51
parent 69821 8432b771f12e
child 69823 93784805c6c5
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
Admin/components/components.sha1
Admin/components/main
Admin/polyml/README
Admin/polyml/settings
NEWS
src/Pure/Admin/build_status.scala
src/Pure/ML/ml_statistics.ML
src/Pure/ML/ml_statistics.scala
     1.1 --- a/Admin/components/components.sha1	Wed Feb 20 07:57:29 2019 +0100
     1.2 +++ b/Admin/components/components.sha1	Wed Feb 20 12:10:40 2019 +0100
     1.3 @@ -197,6 +197,7 @@
     1.4  1430533c09b17f8be73798a47a5f409d43a04cf4  polyml-5.7.1-8.tar.gz
     1.5  171b5783b88522a35e4822b19ef8ba838c04f494  polyml-5.7.1.tar.gz
     1.6  5fbcab1da2b5eb97f24da2590ece189d55b3a105  polyml-5.7.tar.gz
     1.7 +51e024225b460900da5279f0b91b217085f98cf9  polyml-5.8-20190220.tar.gz
     1.8  49f1adfacdd6d29fa9f72035d94a31eaac411a97  polyml-test-0a6ebca445fc.tar.gz
     1.9  2a8c4421e0a03c0d6ad556b3c36c34eb11568adb  polyml-test-1236652ebd55.tar.gz
    1.10  a0064c157a59e2706e18512a49a6dca914fa17fc  polyml-test-1b2dcf8f5202.tar.gz
     2.1 --- a/Admin/components/main	Wed Feb 20 07:57:29 2019 +0100
     2.2 +++ b/Admin/components/main	Wed Feb 20 12:10:40 2019 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  kodkodi-1.5.2-1
     2.5  nunchaku-0.5
     2.6  opam-1.2.2
     2.7 -polyml-test-8fda4fd22441
     2.8 +polyml-5.8-20190220
     2.9  postgresql-42.2.5
    2.10  scala-2.12.8
    2.11  smbc-0.4.1
     3.1 --- a/Admin/polyml/README	Wed Feb 20 07:57:29 2019 +0100
     3.2 +++ b/Admin/polyml/README	Wed Feb 20 12:10:40 2019 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4  
     3.5  This compilation of Poly/ML (https://www.polyml.org) is based on the
     3.6  repository version
     3.7 -https://github.com/polyml/polyml/commit/8fda4fd22441 (master).
     3.8 +https://github.com/polyml/polyml/commit/c3a630fcc6a6 (master).
     3.9  
    3.10  The Isabelle repository provides the administrative tool
    3.11  "build_polyml", which can be used in the polyml component directory as
    3.12 @@ -48,4 +48,4 @@
    3.13  
    3.14  
    3.15          Makarius
    3.16 -        17-Feb-2019
    3.17 +        20-Feb-2019
     4.1 --- a/Admin/polyml/settings	Wed Feb 20 07:57:29 2019 +0100
     4.2 +++ b/Admin/polyml/settings	Wed Feb 20 12:10:40 2019 +0100
     4.3 @@ -12,6 +12,6 @@
     4.4    ML_OPTIONS="--minheap 500"
     4.5  fi
     4.6  
     4.7 -ML_SYSTEM=polyml-5.7.1
     4.8 +ML_SYSTEM=polyml-5.8
     4.9  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    4.10  ML_SOURCES="$POLYML_HOME/src"
     5.1 --- a/NEWS	Wed Feb 20 07:57:29 2019 +0100
     5.2 +++ b/NEWS	Wed Feb 20 12:10:40 2019 +0100
     5.3 @@ -290,6 +290,16 @@
     5.4  * System option "checkpoint" has been discontinued: obsolete thanks to
     5.5  improved memory management in Poly/ML.
     5.6  
     5.7 +* Poly/ML 5.8 allows to use the native x86_64 platform without the full
     5.8 +overhead of 64-bit values everywhere. This special x86_64_32 mode
     5.9 +provides up to 16GB ML heap, while program code and stacks are allocated
    5.10 +elsewhere. Thus approx. 5 times more memory is available for
    5.11 +applications compared to old x86 mode (which is no longer used by
    5.12 +Isabelle). The switch to the x86_64 CPU architecture also avoids
    5.13 +compatibility problems with Linux and macOS, where 32-bit applications
    5.14 +are gradually phased out.
    5.15 +
    5.16 +
    5.17  
    5.18  New in Isabelle2018 (August 2018)
    5.19  ---------------------------------
     6.1 --- a/src/Pure/Admin/build_status.scala	Wed Feb 20 07:57:29 2019 +0100
     6.2 +++ b/src/Pure/Admin/build_status.scala	Wed Feb 20 12:10:40 2019 +0100
     6.3 @@ -58,8 +58,8 @@
     6.4      image_size: (Int, Int) = default_image_size)
     6.5    {
     6.6      val ml_statistics_domain =
     6.7 -      Iterator(ML_Statistics.heap_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields).
     6.8 -        flatMap(_._2).toSet
     6.9 +      Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields,
    6.10 +        ML_Statistics.workers_fields).flatMap(_._2).toSet
    6.11  
    6.12      val data =
    6.13        read_data(options, progress = progress, profiles = profiles,
    6.14 @@ -494,7 +494,8 @@
    6.15                    List(gnuplot(plot_name("heap"), heap_plots, "[0:]"))
    6.16                   else Nil) :::
    6.17                  (if (session.ml_statistics.content.nonEmpty)
    6.18 -                  List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) :::
    6.19 +                  List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields),
    6.20 +                    jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) :::
    6.21                    (if (session.threads > 1)
    6.22                      List(
    6.23                        jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields),
     7.1 --- a/src/Pure/ML/ml_statistics.ML	Wed Feb 20 07:57:29 2019 +0100
     7.2 +++ b/src/Pure/ML/ml_statistics.ML	Wed Feb 20 12:10:40 2019 +0100
     7.3 @@ -17,19 +17,24 @@
     7.4      val
     7.5       {gcFullGCs,
     7.6        gcPartialGCs,
     7.7 +      gcSharePasses,
     7.8        sizeAllocation,
     7.9        sizeAllocationFree,
    7.10 +      sizeCode,
    7.11        sizeHeap,
    7.12        sizeHeapFreeLastFullGC,
    7.13        sizeHeapFreeLastGC,
    7.14 +      sizeStacks,
    7.15        threadsInML,
    7.16        threadsTotal,
    7.17        threadsWaitCondVar,
    7.18        threadsWaitIO,
    7.19        threadsWaitMutex,
    7.20        threadsWaitSignal,
    7.21 +      timeGCReal,
    7.22        timeGCSystem,
    7.23        timeGCUser,
    7.24 +      timeNonGCReal,
    7.25        timeNonGCSystem,
    7.26        timeNonGCUser,
    7.27        userCounters} = PolyML.Statistics.getLocalStats ();
    7.28 @@ -40,17 +45,22 @@
    7.29    in
    7.30      [("full_GCs", Value.print_int gcFullGCs),
    7.31       ("partial_GCs", Value.print_int gcPartialGCs),
    7.32 +     ("share_passes", Value.print_int gcSharePasses),
    7.33       ("size_allocation", Value.print_int sizeAllocation),
    7.34       ("size_allocation_free", Value.print_int sizeAllocationFree),
    7.35 +     ("size_code", Value.print_int sizeCode),
    7.36       ("size_heap", Value.print_int sizeHeap),
    7.37       ("size_heap_free_last_full_GC", Value.print_int sizeHeapFreeLastFullGC),
    7.38       ("size_heap_free_last_GC", Value.print_int sizeHeapFreeLastGC),
    7.39 +     ("size_stacks", Value.print_int sizeStacks),
    7.40       ("threads_in_ML", Value.print_int threadsInML),
    7.41       ("threads_total", Value.print_int threadsTotal),
    7.42       ("threads_wait_condvar", Value.print_int threadsWaitCondVar),
    7.43       ("threads_wait_IO", Value.print_int threadsWaitIO),
    7.44       ("threads_wait_mutex", Value.print_int threadsWaitMutex),
    7.45       ("threads_wait_signal", Value.print_int threadsWaitSignal),
    7.46 +     ("time_elapsed", Value.print_real (Time.toReal timeNonGCReal)),
    7.47 +     ("time_elapsed_GC", Value.print_real (Time.toReal timeGCReal)),
    7.48       ("time_CPU", Value.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
    7.49       ("time_GC", Value.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
    7.50      user_counters
     8.1 --- a/src/Pure/ML/ml_statistics.scala	Wed Feb 20 07:57:29 2019 +0100
     8.2 +++ b/src/Pure/ML/ml_statistics.scala	Wed Feb 20 12:10:40 2019 +0100
     8.3 @@ -46,25 +46,30 @@
     8.4      ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
     8.5  
     8.6    val GC_fields: Fields =
     8.7 -    ("GCs", List("partial_GCs", "full_GCs"))
     8.8 +    ("GCs", List("partial_GCs", "full_GCs", "share_passes"))
     8.9  
    8.10    val heap_fields: Fields =
    8.11      ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
    8.12        "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
    8.13  
    8.14 +  val program_fields: Fields =
    8.15 +    ("Program", List("size_code", "size_stacks"))
    8.16 +
    8.17    val threads_fields: Fields =
    8.18      ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
    8.19        "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
    8.20  
    8.21    val time_fields: Fields =
    8.22 -    ("Time", List("time_CPU", "time_GC"))
    8.23 +    ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
    8.24  
    8.25    val speed_fields: Fields =
    8.26      ("Speed", List("speed_CPU", "speed_GC"))
    8.27  
    8.28 +  private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
    8.29 +
    8.30  
    8.31    val all_fields: List[Fields] =
    8.32 -    List(tasks_fields, workers_fields, GC_fields, heap_fields, threads_fields,
    8.33 +    List(tasks_fields, workers_fields, GC_fields, heap_fields, program_fields, threads_fields,
    8.34        time_fields, speed_fields)
    8.35  
    8.36    val main_fields: List[Fields] =
    8.37 @@ -107,21 +112,20 @@
    8.38          val speeds =
    8.39            (for {
    8.40              (key, value) <- props.iterator
    8.41 -            a <- Library.try_unprefix("time", key)
    8.42 -            b = "speed" + a if domain(b)
    8.43 -          }
    8.44 -          yield {
    8.45 -            val (x0, y0, s0) = last_edge.getOrElse(a, (0.0, 0.0, 0.0))
    8.46 +            key1 <- time_speed.get(key)
    8.47 +            if domain(key1)
    8.48 +          } yield {
    8.49 +            val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0))
    8.50  
    8.51              val x1 = time
    8.52              val y1 = java.lang.Double.parseDouble(value)
    8.53              val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
    8.54  
    8.55              if (y1 > y0) {
    8.56 -              last_edge += (a -> (x1, y1, s1))
    8.57 -              (b, s1.toString)
    8.58 +              last_edge += (key -> (x1, y1, s1))
    8.59 +              (key1, s1.toString)
    8.60              }
    8.61 -            else (b, s0.toString)
    8.62 +            else (key1, s0.toString)
    8.63            }).toList
    8.64  
    8.65          val data =