# HG changeset patch # User wenzelm # Date 1614634653 -3600 # Node ID 0bf768567d9f7b920eeef933d39196c2f395d271 # Parent 2dd1fd9112d94837ac0d4e586948c0c60ff56104 tuned --- avoid deprecated Predef.any2stringadd; diff -r 2dd1fd9112d9 -r 0bf768567d9f src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon Mar 01 22:26:33 2021 +0100 +++ b/src/Pure/Admin/build_log.scala Mon Mar 01 22:37:33 2021 +0100 @@ -765,8 +765,8 @@ val version1 = Prop.isabelle_version val version2 = Prop.afp_version - val eq1 = version1(table) + " = " + SQL.string(rev) - val eq2 = version2(table) + " = " + SQL.string(rev2) + val eq1 = version1(table).toString + " = " + SQL.string(rev) + val eq2 = version2(table).toString + " = " + SQL.string(rev2) SQL.Table("recent_pull_date", table.columns, table.select(table.columns, @@ -1136,7 +1136,7 @@ if (ml_statistics) { val columns = columns1 ::: List(Data.ml_statistics(table2)) val join = - table1 + SQL.join_outer + table2 + " ON " + + table1.toString + SQL.join_outer + table2 + " ON " + Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " + Data.session_name(table1) + " = " + Data.session_name(table2) (columns, SQL.enclose(join)) diff -r 2dd1fd9112d9 -r 0bf768567d9f src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 01 22:26:33 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Mar 01 22:37:33 2021 +0100 @@ -159,7 +159,7 @@ permissive = proxy_host.nonEmpty) def sql: SQL.Source = - Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " + + Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " + SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + (if (detect == "") "" else " AND " + SQL.enclose(detect)) @@ -219,7 +219,7 @@ " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" + " -e ISABELLE_SWIPL=swipl", args = "-N -a -d '~~/src/Benchmarks'", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")), Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3", options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'"), @@ -229,36 +229,36 @@ args = "-g large -g slow", afp = true, bulky = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP old", "lxbroy7", args = "-N -X large -X slow", afp = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history_base = "37074e22e8be", options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-N -g timing", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " + + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " + Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-N -g timing", detect = - Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + + Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("Poly/ML 5.7 macOS", "macbroy2", history_base = "37074e22e8be", options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", args = "-a", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")), Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2", history_base = "a9d5b59c3e12", options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", args = "-a", detect = - Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + - Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), + Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + + Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), Remote_Build("macOS", "macbroy2", options = "-m32 -M8" + " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + @@ -271,21 +271,21 @@ history_base = "2c0f24e927dd"), Remote_Build("macOS, quick_and_dirty", "macbroy2", options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"), history_base = "2c0f24e927dd"), Remote_Build("macOS, skip_proofs", "macbroy2", options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"), history_base = "2c0f24e927dd"), Remote_Build("Poly/ML test", "lxbroy8", options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", args = "-N -g timing", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")), Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a", - detect = Build_Log.Prop.build_start + " > date '2017-03-03'"), + detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"), Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"), Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", - detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) ::: + detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) ::: { for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } yield { @@ -297,7 +297,7 @@ " -e ISABELLE_SMLNJ=sml", args = "-N -X large -X slow", afp = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")) + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")) } } @@ -330,10 +330,10 @@ Remote_Build("macOS, quick_and_dirty", "mini2", options = "-m32 -M4 -t quick_and_dirty -p pide_session=false", self_update = true, args = "-a -o quick_and_dirty", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")), Remote_Build("macOS, skip_proofs", "mini2", options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs", - detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))), List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", proxy_host = "laraserver", proxy_user = "makarius", self_update = true, @@ -348,7 +348,7 @@ " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", detect = - Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows") + " OR " + + Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " + Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")), Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, options = "-m64 -M4" + @@ -357,7 +357,7 @@ " -e ISABELLE_GHC_SETUP=true" + " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", args = "-a", - detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))) + detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows")))) } val remote_builds2: List[List[Remote_Build]] = @@ -373,7 +373,7 @@ " -e ISABELLE_SMLNJ=sml", args = "-a -X large -X slow", afp = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")), Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true, proxy_host = "lxbroy10", proxy_user = "i21isatest", java_heap = "8g", @@ -381,7 +381,7 @@ args = "-g large -g slow", afp = true, bulky = true, - detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))) + detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")))) def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build) : Logger_Task = @@ -570,7 +570,7 @@ /* main */ val main_start_date = Date.now() - File.write(main_state_file, main_start_date + " " + log_service.hostname) + File.write(main_state_file, main_start_date.toString + " " + log_service.hostname) run(main_start_date, Logger_Task("isabelle_cronjob", logger => diff -r 2dd1fd9112d9 -r 0bf768567d9f src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Mon Mar 01 22:26:33 2021 +0100 +++ b/src/Pure/Admin/jenkins.scala Mon Mar 01 22:37:33 2021 +0100 @@ -56,8 +56,8 @@ build_log_jobs.map(job_name => Build_Status.Profile("jenkins " + job_name, sql = - Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " + - Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " + + Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_Log.Jenkins.engine) + + " AND " + Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " + Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) + " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))