--- 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
--- 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
--- 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; }
--- 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)
--- 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).
--- 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",
--- 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 =
{
--- 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)
+ }
+}
--- 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 =
--- 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"
}
}