# HG changeset patch # User wenzelm # Date 1495401039 -7200 # Node ID 54f621d5fa005ea62841b91dd1f3473e2fb8569b # Parent 77d922eff5acceb58f811e95fac4c53d35b413e2# Parent 20656a4709d6bc8b37e34f36602dbfdcf189d443 merged diff -r 77d922eff5ac -r 54f621d5fa00 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sun May 21 21:37:31 2017 +0200 +++ b/Admin/components/components.sha1 Sun May 21 23:10:39 2017 +0200 @@ -169,6 +169,7 @@ b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz 43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz +b016a785f1f78855c00d351ff598355c3b87450f sqlite-jdbc-3.18.0-1.tar.gz b85b5bc071a59ef2a8326ceb1617d5a9a5be41cf sqlite-jdbc-3.18.0.tar.gz 8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz 2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz diff -r 77d922eff5ac -r 54f621d5fa00 Admin/components/main --- a/Admin/components/main Sun May 21 21:37:31 2017 +0200 +++ b/Admin/components/main Sun May 21 23:10:39 2017 +0200 @@ -15,6 +15,6 @@ scala-2.12.2 ssh-java-20161009 spass-3.8ds -sqlite-jdbc-3.18.0 +sqlite-jdbc-3.18.0-1 xz-java-1.6 z3-4.4.0pre diff -r 77d922eff5ac -r 54f621d5fa00 etc/isabelle.css --- a/etc/isabelle.css Sun May 21 21:37:31 2017 +0200 +++ b/etc/isabelle.css Sun May 21 23:10:39 2017 +0200 @@ -75,3 +75,13 @@ .comment { color: #CC0000; } .improper { color: #FF5050; } .bad { background-color: #FF6A6A; } + + +/* message background */ + +.writeln_message { background-color: #F0F0F0; } +.information_message { background-color: #DCEAF3; } +.tracing_message { background-color: #F0F8FF; } +.warning_message { background-color: #EEE8AA; } +.legacy_message { background-color: #EEE8AA; } +.error_message { background-color: #FFC1C1; } diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/Admin/build_history.scala Sun May 21 23:10:39 2017 +0200 @@ -169,6 +169,7 @@ val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") + val build_out = isabelle_output_log + Path.explode("build.out") if (first_build) { other_isabelle.resolve_components(verbose) @@ -194,7 +195,11 @@ val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: build_args val build_result = - other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose) + { + val progress1 = new Seq_Progress(progress, new File_Progress(build_out)) + val other_isabelle1 = new Other_Isabelle(progress1, hg.root, isabelle_identifier) + other_isabelle1("build " + Bash.strings(build_args1), redirect = true, echo = verbose) + } val build_end = Date.now() val log_path = @@ -203,9 +208,6 @@ Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) - Isabelle_System.mkdirs(isabelle_output_log) - File.write(isabelle_output_log + Path.explode("build.log"), build_result.out) - val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.base.implode, build_result.out_lines). parse_build_info(ml_statistics = true) @@ -264,6 +266,8 @@ /* next build */ + build_out.file.delete + if (multicore_base && first_build && isabelle_output_log.is_dir) Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Sun May 21 23:10:39 2017 +0200 @@ -33,7 +33,10 @@ Build_Log.Data.universal_table.select(columns, distinct = true, sql = "WHERE " + Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " + - Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) + + SQL.member(Build_Log.Data.status.ident, + List( + Build_Log.Session_Status.finished.toString, + Build_Log.Session_Status.failed.toString)) + (if (only_sessions.isEmpty) "" else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) + " AND " + SQL.enclose(sql) + @@ -66,6 +69,10 @@ sealed case class Data(date: Date, entries: List[Data_Entry]) sealed case class Data_Entry( name: String, hosts: List[String], stretch: Double, sessions: List[Session]) + { + def failed_sessions: List[Session] = + sessions.filter(_.head.failed).sortBy(_.name) + } sealed case class Session( name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics) { @@ -74,10 +81,12 @@ def head: Entry = entries.head def order: Long = - head.timing.elapsed.ms - def check_timing: Boolean = entries.length >= 3 + def finished_entries: List[Entry] = entries.filter(_.finished) + + def check_timing: Boolean = finished_entries.length >= 3 def check_heap: Boolean = - entries.length >= 3 && - entries.forall(entry => + finished_entries.length >= 3 && + finished_entries.forall(entry => entry.maximum_heap > 0 || entry.average_heap > 0 || entry.stored_heap > 0) @@ -90,7 +99,12 @@ ml_timing: Timing, maximum_heap: Long, average_heap: Long, - stored_heap: Long) + stored_heap: Long, + status: Build_Log.Session_Status.Value) + { + def finished: Boolean = status == Build_Log.Session_Status.finished + def failed: Boolean = status == Build_Log.Session_Status.failed + } sealed case class Image(name: String, width: Int, height: Int) { @@ -134,7 +148,8 @@ Build_Log.Data.ml_timing_elapsed, Build_Log.Data.ml_timing_cpu, Build_Log.Data.ml_timing_gc, - Build_Log.Data.heap_size) ::: + Build_Log.Data.heap_size, + Build_Log.Data.status) ::: (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil) val Threads_Option = """threads\s*=\s*(\d+)""".r @@ -193,7 +208,8 @@ Build_Log.Data.ml_timing_gc), maximum_heap = ml_stats.maximum_heap_size, average_heap = ml_stats.average_heap_size, - stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size))) + stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)), + status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status))) val sessions = data_entries.getOrElse(data_name, Map.empty) val entries = sessions.get(session_name).map(_.entries) getOrElse Nil @@ -240,8 +256,17 @@ List(HTML.text("status date:") -> HTML.text(data.date.toString))))), HTML.par( List(HTML.itemize(data.entries.map({ case data_entry => - List(HTML.link(clean_name(data_entry.name) + "/index.html", - HTML.text(data_entry.name))) })))))) + List( + HTML.link(clean_name(data_entry.name) + "/index.html", + HTML.text(data_entry.name))) ::: + (data_entry.failed_sessions match { + case Nil => Nil + case sessions => + HTML.break ::: List(HTML.error_message_span("Failed:")) ::: + HTML.text(" " + + commas(sessions.map(s => s.name + " (" + s.head.isabelle_version + ")"))) + }) + })))))) for (data_entry <- data.entries) { val data_name = data_entry.name @@ -263,7 +288,7 @@ File.write(data_file, cat_lines( - session.entries.map(entry => + session.finished_entries.map(entry => List(entry.pull_date.unix_epoch, entry.timing.elapsed.minutes, entry.timing.resources.minutes, @@ -274,7 +299,7 @@ entry.stored_heap).mkString(" ")))) val max_time = - ((0.0 /: session.entries){ case (m, entry) => + ((0.0 /: session.finished_entries){ case (m, entry) => m.max(entry.timing.elapsed.minutes). max(entry.timing.resources.minutes). max(entry.ml_timing.elapsed.minutes). diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Sun May 21 23:10:39 2017 +0200 @@ -200,15 +200,16 @@ List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")), List( Remote_Build("Windows", "vmnipkow9", history = 90, shared_home = false, - options = "-m32 -M4 -N build_history_32", args = "-a", + options = "-m32 -M4", args = "-a", detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")), Remote_Build("Windows", "vmnipkow9", history = 90, shared_home = false, - options = "-m64 -M4 -N build_history_64", args = "-a", + options = "-m64 -M4", args = "-a", detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))) } - private def remote_build_history(rev: String, r: Remote_Build): Logger_Task = + private def remote_build_history(arg: (String, Int), r: Remote_Build): Logger_Task = { + val (rev, index) = arg val task_name = "build_history-" + r.host Logger_Task(task_name, logger => { @@ -226,7 +227,9 @@ self_update = self_update, push_isabelle_home = push_isabelle_home, options = - "-r " + Bash.string(rev) + " -N " + Bash.string(task_name) + " -f " + r.options, + "-r " + Bash.string(rev) + + " -N " + Bash.string(task_name) + (index + 1).toString + + " -f " + r.options, args = "-o timeout=10800 " + r.args) for ((log_name, bytes) <- results) { @@ -388,7 +391,7 @@ SEQ(List(build_release, build_history_base, PAR(remote_builds.map(seq => SEQ(seq.flatMap(r => - r.pick(logger.options, rev, r.history_base_filter(hg)). + r.pick(logger.options, rev, r.history_base_filter(hg)).zipWithIndex. map(remote_build_history(_, r)))))), Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)), Logger_Task("build_log_database", diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/General/sql.scala Sun May 21 23:10:39 2017 +0200 @@ -384,7 +384,19 @@ // see https://www.sqlite.org/lang_datefunc.html val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x") - lazy val init_jdbc: Unit = Class.forName("org.sqlite.JDBC") + lazy val init_jdbc: Unit = + { + val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform) + val lib_name = + File.find_files(lib_path.file) match { + case List(file) => file.getName + case _ => error("Exactly file expected in directory " + lib_path.expand) + } + System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path)) + System.setProperty("org.sqlite.lib.name", lib_name) + + Class.forName("org.sqlite.JDBC") + } def open_database(path: Path): Database = { diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/System/progress.scala Sun May 21 23:10:39 2017 +0200 @@ -54,3 +54,29 @@ is_stopped } } + +class File_Progress(path: Path, verbose: Boolean = false) extends Progress +{ + override def echo(msg: String): Unit = + File.append(path, msg + "\n") + + override def theory(session: String, theory: String): Unit = + if (verbose) echo(session + ": theory " + theory) + + override def toString: String = path.toString +} + +class Seq_Progress(progress1: Progress, progress2: Progress) extends Progress +{ + override def echo(msg: String) + { + progress1.echo(msg) + progress2.echo(msg) + } + + override def theory(session: String, theory: String) + { + progress1.theory(session, theory) + progress2.theory(session, theory) + } +} diff -r 77d922eff5ac -r 54f621d5fa00 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Sun May 21 21:37:31 2017 +0200 +++ b/src/Pure/Thy/html.scala Sun May 21 23:10:39 2017 +0200 @@ -92,6 +92,7 @@ def id(s: String): XML.Attribute = ("id" -> s) def width(w: Int): XML.Attribute = ("width" -> w.toString) def height(h: Int): XML.Attribute = ("height" -> h.toString) + def css_class(name: String): XML.Attribute = ("class" -> name) /* structured markup operators */ @@ -137,6 +138,21 @@ XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil) + /* messages */ + + val writeln_message_class: XML.Attribute = css_class("writeln_message") + val warning_message_class: XML.Attribute = css_class("warning_message") + val error_message_class: XML.Attribute = css_class("error_message") + + def writeln_message(msg: String): XML.Elem = par(text(msg)) + writeln_message_class + def warning_message(msg: String): XML.Elem = par(text(msg)) + warning_message_class + def error_message(msg: String): XML.Elem = par(text(msg)) + error_message_class + + def writeln_message_span(msg: String): XML.Elem = span(text(msg)) + writeln_message_class + def warning_message_span(msg: String): XML.Elem = span(text(msg)) + warning_message_class + def error_message_span(msg: String): XML.Elem = span(text(msg)) + error_message_class + + /* document */ val header: String = diff -r 77d922eff5ac -r 54f621d5fa00 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sun May 21 21:37:31 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Sun May 21 23:10:39 2017 +0200 @@ -145,13 +145,13 @@ "postinstall": "node ./node_modules/vscode/bin/install" }, "devDependencies": { - "typescript": "2.2.x", - "vscode": "1.x", - "mocha": "3.x", - "@types/node": "^6.0.40", - "@types/mocha": "^2.2.32" + "typescript": "^2.3.2", + "vscode": "^1.1.0", + "mocha": "^3.4.1", + "@types/node": "^7.0.21", + "@types/mocha": "^2.2.41" }, "dependencies": { - "vscode-languageclient": "~3.2.0" + "vscode-languageclient": "~3.2.2" } }