# HG changeset patch
# User wenzelm
# Date 1494592437 -7200
# Node ID d3c5898f1a5e6c276374e54c2a1b7aae4b06e6fb
# Parent  73ed0ebac3b0565cbe4036fc325261b032e3128b
updated to polyml-5.7 for testing (not yet ready for production use);

diff -r 73ed0ebac3b0 -r d3c5898f1a5e Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri May 12 11:56:41 2017 +0200
+++ b/Admin/components/components.sha1	Fri May 12 14:33:57 2017 +0200
@@ -140,6 +140,7 @@
 5b70c12c95a90d858f90c1945011289944ea8e17  polyml-5.6-20160118.tar.gz
 5b19dc93082803b82aa553a5cfb3e914606c0ffd  polyml-5.6.tar.gz
 80b923fca3533bf291ff9da991f2262a98b68cc4  polyml-5.7-20170217.tar.gz
+5fbcab1da2b5eb97f24da2590ece189d55b3a105  polyml-5.7.tar.gz
 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e  polyml-test-7a7b742897e9.tar.gz
 c629cd499a724bbe37b962f727e4ff340c50299d  polyml-test-8529546198aa.tar.gz
 f132329ca1045858ef456cc08b197c9eeea6881b  postgresql-9.4.1212.tar.gz
diff -r 73ed0ebac3b0 -r d3c5898f1a5e Admin/polyml/README
--- a/Admin/polyml/README	Fri May 12 11:56:41 2017 +0200
+++ b/Admin/polyml/README	Fri May 12 14:33:57 2017 +0200
@@ -1,27 +1,27 @@
 Poly/ML for Isabelle
 ====================
 
-This compilation of Poly/ML (http://www.polyml.org) is based on the repository
-version https://github.com/polyml/polyml/commit/6307085deb18
+This compilation of Poly/ML 5.7 (http://www.polyml.org) is based on the
+source distribution from https://github.com/polyml/polyml/releases/tag/v5.7
 
-The Isabelle repository provides the administrative tool "build_polyml", which
-can be used in the polyml component directory as follows.
+The Isabelle repository provides the administrative tool "build_polyml",
+which can be used in the polyml component directory as follows.
 
 * Linux:
 
-  isabelle build_polyml -m32 -s sha1 src --with-gmp
-  isabelle build_polyml -m64 -s sha1 src --with-gmp
+  $ isabelle build_polyml -m32 -s sha1 src --with-gmp
+  $ isabelle build_polyml -m64 -s sha1 src --with-gmp
 
 * Mac OS X:
 
-  isabelle build_polyml -m32 -s sha1 src --without-gmp
-  isabelle build_polyml -m64 -s sha1 src --without-gmp
+  $ isabelle build_polyml -m32 -s sha1 src --without-gmp
+  $ isabelle build_polyml -m64 -s sha1 src --without-gmp
 
 * Windows (Cygwin shell)
 
-  isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp
-  isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp
+  $ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp
+  $ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp
 
 
         Makarius
-        17-Feb-2017
+        12-May-2017
diff -r 73ed0ebac3b0 -r d3c5898f1a5e src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 11:56:41 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri May 12 14:33:57 2017 +0200
@@ -141,10 +141,10 @@
   private val remote_builds: List[List[Remote_Build]] =
   {
     List(
-      List(Remote_Build("Poly/ML test", "lxbroy8",
-        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
+      List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
+        options = "-m32 -B -M1x2,2 -t polyml-5.7 -e 'init_component /home/isabelle/contrib/polyml-5.7'",
         args = "-N -g timing",
-        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test"))),
+        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7"))),
       List(Remote_Build("Linux A", "lxbroy9",
         options = "-m32 -B -M1x2,2", args = "-N -g timing")),
       List(Remote_Build("Linux B", "lxbroy10", history = 90,
@@ -173,9 +173,14 @@
 
   private val remote_builds_old: List[Remote_Build] =
     List(
+      Remote_Build("Poly/ML test", "lxbroy8",
+        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
+        args = "-N -g timing",
+        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
       Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
         detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
 
+                      
   private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
   {
     val task_name = "build_history-" + r.host