--- a/Admin/components/components.sha1 Sun Oct 22 11:59:44 2017 +0200
+++ b/Admin/components/components.sha1 Sun Oct 22 16:35:24 2017 +0200
@@ -156,6 +156,7 @@
5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz
+2b7c02b67feb2f44dda6938a7244f4257e7c580c polyml-test-905dae2ebfda.tar.gz
b4ceeaac47f3baae41c2491a8368b03217946166 polyml-test-e7a662f8f9c4.tar.gz
53123dc011b2d4b4e8fe307f3c9fa355718ad01a postgresql-42.1.1.tar.gz
3a5d31377ec07a5069957f5477a4848cfc89a594 postgresql-42.1.4.tar.gz
@@ -218,4 +219,5 @@
86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz
a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz
06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz
+93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
--- a/Admin/polyml/settings Sun Oct 22 11:59:44 2017 +0200
+++ b/Admin/polyml/settings Sun Oct 22 16:35:24 2017 +0200
@@ -48,15 +48,19 @@
case "$ML_PLATFORM" in
x86_64-windows)
+ POLYML_EXE="$ML_HOME/poly.exe"
ML_OPTIONS="-H 1000 --codepage utf8"
;;
x86-windows)
+ POLYML_EXE="$ML_HOME/poly.exe"
ML_OPTIONS="-H 500 --codepage utf8"
;;
x86_64-*)
+ POLYML_EXE="$ML_HOME/poly"
ML_OPTIONS="-H 1000"
;;
*)
+ POLYML_EXE="$ML_HOME/poly"
ML_OPTIONS="-H 500"
;;
esac
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 22 11:59:44 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Oct 22 16:35:24 2017 +0200
@@ -13,7 +13,7 @@
object Isabelle_Cronjob
{
- /* file-system state: owned by main cronjob */
+ /* global resources: owned by main cronjob */
val main_dir = Path.explode("~/cronjob")
val main_state_file = main_dir + Path.explode("run/main.state")
@@ -26,6 +26,9 @@
val jenkins_jobs = "identify" :: Jenkins.build_log_jobs
+ val build_log_dirs =
+ List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
+
/** particular tasks **/
@@ -130,13 +133,6 @@
def profile: Build_Status.Profile =
Build_Status.Profile(description, history = history, afp = afp, sql = sql)
- def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
- {
- val rev0 = hg.id(history_base)
- val nodes = hg.graph().all_succs(List(rev0)).toSet
- (item: Item) => nodes(item.isabelle_version)
- }
-
def pick(
options: Options,
rev: String = "",
@@ -192,7 +188,7 @@
detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
- val remote_builds: List[List[Remote_Build]] =
+ val remote_builds1: List[List[Remote_Build]] =
{
List(
List(Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
@@ -241,12 +237,6 @@
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
- List(
- Remote_Build("AFP slow", "lrzcloud1", shared_home = false,
- options = "-m64 -M6 -U30000 -s10 -t AFP",
- args = "-g slow",
- afp = true,
- detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
) :::
{
for { (host, n) <- List("lxbroy6" -> 1, "lxbroy7" -> 2) }
@@ -260,6 +250,15 @@
}
}
+ val remote_builds2: List[List[Remote_Build]] =
+ List(
+ List(
+ Remote_Build("AFP slow", "lrzcloud1", shared_home = false,
+ options = "-m64 -M6 -U30000 -s10 -t AFP",
+ args = "-g slow",
+ afp = true,
+ detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
+
private def remote_build_history(
rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
{
@@ -295,7 +294,7 @@
}
val build_status_profiles: List[Build_Status.Profile] =
- (remote_builds_old :: remote_builds).flatten.map(_.profile)
+ (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
@@ -431,29 +430,42 @@
})
+ /* repository structure */
+
+ val hg = Mercurial.repository(isabelle_repos)
+ val hg_graph = hg.graph()
+ val rev = hg.id()
+
+ def history_base_filter(r: Remote_Build): Item => Boolean =
+ {
+ val base_rev = hg.id(r.history_base)
+ val nodes = hg_graph.all_succs(List(base_rev)).toSet
+ (item: Item) => nodes(item.isabelle_version)
+ }
+
+
/* main */
val main_start_date = Date.now()
File.write(main_state_file, main_start_date + " " + log_service.hostname)
- val hg = Mercurial.repository(isabelle_repos)
- val rev = hg.id()
-
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
SEQ(List(build_release, build_history_base,
- PAR(remote_builds.map(seq =>
- SEQ(
- for {
- (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
- (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, r.history_base_filter(hg))
- } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
- Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
- Logger_Task("build_log_database",
- logger => Isabelle_Devel.build_log_database(logger.options)),
- Logger_Task("build_status",
- logger => Isabelle_Devel.build_status(logger.options)))))))
+ PAR(List(remote_builds1, remote_builds2).map(remote_builds =>
+ SEQ(List(
+ PAR(remote_builds.map(seq =>
+ SEQ(
+ for {
+ (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
+ (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, history_base_filter(r))
+ } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
+ Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
+ Logger_Task("build_log_database",
+ logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
+ Logger_Task("build_status",
+ logger => Isabelle_Devel.build_status(logger.options)))))))))))
log_service.shutdown()
--- a/src/Pure/Admin/isabelle_devel.scala Sun Oct 22 11:59:44 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala Sun Oct 22 16:35:24 2017 +0200
@@ -15,9 +15,6 @@
val BUILD_LOG_DB = "build_log.db"
val BUILD_STATUS = "build_status"
- val standard_log_dirs =
- List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
-
/* index */
@@ -67,7 +64,7 @@
/* maintain build_log database */
- def build_log_database(options: Options, log_dirs: List[Path] = standard_log_dirs)
+ def build_log_database(options: Options, log_dirs: List[Path])
{
val store = Build_Log.store(options)
using(store.open_database())(db =>
--- a/src/Pure/General/mercurial.scala Sun Oct 22 11:59:44 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sun Oct 22 16:35:24 2017 +0200
@@ -16,6 +16,9 @@
object Mercurial
{
+ type Graph = isabelle.Graph[String, Unit]
+
+
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
@@ -119,7 +122,7 @@
def known_files(): List[String] =
hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
- def graph(): Graph[String, Unit] =
+ def graph(): Graph =
{
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
val log_result =