--- a/etc/options Sat Feb 25 17:35:48 2023 +0000
+++ b/etc/options Sun Feb 26 21:17:10 2023 +0100
@@ -132,9 +132,6 @@
option timeout_build : bool = true
-- "observe timeout for session build"
-option process_output_limit : int = 100
- -- "build process output limit (in million characters, 0 = unlimited)"
-
option process_output_tail : int = 40
-- "build process output tail shown to user (in lines, 0 = unlimited)"
@@ -180,9 +177,15 @@
option build_pide_reports : bool = true
-- "report PIDE markup (in batch build)"
+option build_hostname : string = ""
+ -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"
+
option build_engine : string = ""
-- "alternative session build engine"
+option build_database : bool = false
+ -- "expose state of build process via central database"
+
section "Editor Session"
--- a/lib/scripts/getsettings Sat Feb 25 17:35:48 2023 +0000
+++ b/lib/scripts/getsettings Sun Feb 26 21:17:10 2023 +0100
@@ -78,6 +78,8 @@
ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
+ISABELLE_HOSTNAME="$(hostname -s)"
+
# components
--- a/src/Pure/Admin/build_history.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Admin/build_history.scala Sun Feb 26 21:17:10 2023 +0100
@@ -582,7 +582,7 @@
else {
ssh.with_tmp_dir { tmp_dir =>
val output_file = tmp_dir + Path.explode("output")
- val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
+ val build_options = if_proper(afp_repos, " -A") + " " + options
try {
val script =
ssh.bash_path(Path.explode("Admin/build_other")) +
--- a/src/Pure/Admin/build_log.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Admin/build_log.scala Sun Feb 26 21:17:10 2023 +0100
@@ -681,7 +681,7 @@
val version2 = Prop.afp_version
build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
SQL.select(List(version1, version2), distinct = true) + meta_info_table +
- " WHERE " + version1.defined + " AND " + version2.defined)
+ SQL.where(SQL.and(version1.defined, version2.defined)))
}
@@ -700,7 +700,7 @@
"SELECT " + versions.mkString(", ") +
", min(" + Prop.build_start + ") AS " + pull_date(afp) +
" FROM " + meta_info_table +
- " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") +
+ " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
" GROUP BY " + versions.mkString(", "))
}
@@ -719,25 +719,22 @@
val rev2 = afp_rev.getOrElse("")
val table = pull_date_table(afp)
- val version1 = Prop.isabelle_version
- val version2 = Prop.afp_version
- val eq1 = version1(table).toString + " = " + SQL.string(rev)
- val eq2 = version2(table).toString + " = " + SQL.string(rev2)
+ val eq_rev = if_proper(rev, Prop.isabelle_version(table).equal(rev))
+ val eq_rev2 = if_proper(rev2, Prop.afp_version(table).equal(rev2))
SQL.Table("recent_pull_date", table.columns,
- table.select(table.columns,
- "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) +
- (if (rev != "" && rev2 == "") " OR " + eq1
- else if (rev == "" && rev2 != "") " OR " + eq2
- else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
- else "")))
+ table.select(table.columns, sql =
+ SQL.where(
+ SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days),
+ SQL.and(eq_rev, eq_rev2)))))
}
def select_recent_log_names(days: Int): PostgreSQL.Source = {
val table1 = meta_info_table
val table2 = recent_pull_date_table(days)
- table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
- " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
+ table1.select(List(log_name), distinct = true, sql =
+ SQL.join_inner + table2.query_named +
+ " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
}
def select_recent_versions(
@@ -776,9 +773,10 @@
val a_table =
SQL.Table("a", a_columns,
SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) +
- table1 + SQL.join_outer + table2 +
- " ON " + version1(table1) + " = " + version1(table2) +
- " AND " + version2(table1) + " = " + version2(table2))
+ table1 + SQL.join_outer + table2 + " ON " +
+ SQL.and(
+ version1(table1).ident + " = " + version1(table2).ident,
+ version2(table1).ident + " = " + version2(table2).ident))
val b_columns = log_name :: pull_date() :: a_columns.tail
val b_table =
@@ -798,9 +796,10 @@
SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
{
SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
- c_table.query_named + SQL.join_outer + ml_statistics_table +
- " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) +
- " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table)
+ c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " +
+ SQL.and(
+ log_name(c_table).ident + " = " + log_name(ml_statistics_table).ident,
+ session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident)
})
}
}
@@ -1037,7 +1036,7 @@
def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
val table = Data.meta_info_table
val columns = table.columns.tail
- db.using_statement(table.select(columns, Data.log_name.where_equal(log_name))) { stmt =>
+ db.using_statement(table.select(columns, sql = Data.log_name.where_equal(log_name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) None
else {
@@ -1063,12 +1062,12 @@
val table1 = Data.sessions_table
val table2 = Data.ml_statistics_table
- val where_log_name =
- Data.log_name(table1).where_equal(log_name) + " AND " +
- Data.session_name(table1) + " <> ''"
val where =
- if (session_names.isEmpty) where_log_name
- else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
+ SQL.where(
+ SQL.and(
+ Data.log_name(table1).where_equal(log_name),
+ Data.session_name(table1).ident + " <> ''",
+ if_proper(session_names, Data.session_name(table1).member(session_names))))
val columns1 = table1.columns.tail.map(_.apply(table1))
val (columns, from) =
@@ -1076,14 +1075,15 @@
val columns = columns1 ::: List(Data.ml_statistics(table2))
val join =
table1.toString + SQL.join_outer + table2 + " ON " +
- Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
- Data.session_name(table1) + " = " + Data.session_name(table2)
+ SQL.and(
+ Data.log_name(table1).ident + " = " + Data.log_name(table2).ident,
+ Data.session_name(table1).ident + " = " + Data.session_name(table2).ident)
(columns, SQL.enclose(join))
}
else (columns1, table1.ident)
val sessions =
- db.using_statement(SQL.select(columns) + from + " " + where) { stmt =>
+ db.using_statement(SQL.select(columns) + from + where) { stmt =>
stmt.execute_query().iterator({ res =>
val session_name = res.string(Data.session_name)
val session_entry =
--- a/src/Pure/Admin/build_scala.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Admin/build_scala.scala Sun Feb 26 21:17:10 2023 +0100
@@ -29,8 +29,7 @@
Isabelle_System.download_file(proper_url, path, progress = progress)
def print: String =
- " * " + name + " " + version +
- (if (base_version.nonEmpty) " for Scala " + base_version else "") +
+ " * " + name + " " + version + if_proper(base_version, " for Scala " + base_version) +
":\n " + make_url(url)
}
--- a/src/Pure/Admin/build_status.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Admin/build_status.scala Sun Feb 26 21:17:10 2023 +0100
@@ -36,16 +36,15 @@
columns: List[SQL.Column],
only_sessions: Set[String]
): PostgreSQL.Source = {
- Build_Log.Data.universal_table.select(columns, distinct = true,
- sql = "WHERE " +
+ Build_Log.Data.universal_table.select(columns, distinct = true, sql =
+ "WHERE " +
Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
" AND " +
- SQL.member(Build_Log.Data.status.ident,
+ Build_Log.Data.status.member(
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)) +
+ if_proper(only_sessions, " AND " + Build_Log.Data.session_name.member(only_sessions)) +
" AND " + SQL.enclose(sql))
}
}
@@ -206,7 +205,7 @@
val body =
proper_string(isabelle_version).map("Isabelle/" + _).toList :::
(if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList
- if (body.isEmpty) "" else body.mkString(" (", ", ", ")")
+ if_proper(body, body.mkString(" (", ", ", ")"))
}
def read_data(options: Options,
--- a/src/Pure/Admin/isabelle_cronjob.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Feb 26 21:17:10 2023 +0100
@@ -155,9 +155,10 @@
SSH.open_session(options, host = host, user = user, port = port)
def sql: PostgreSQL.Source =
- 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))
+ SQL.and(
+ Build_Log.Prop.build_engine.equal(Build_History.engine),
+ Build_Log.Prop.build_host.member(host :: more_hosts),
+ if_proper(detect, SQL.enclose(detect)))
def profile: Build_Status.Profile =
Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
--- a/src/Pure/General/completion.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/completion.scala Sun Feb 26 21:17:10 2023 +0100
@@ -60,7 +60,7 @@
def load(): History = {
def ignore_error(msg: String): Unit =
Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
- (if (msg == "") "" else "\n" + msg))
+ if_proper(msg, "\n" + msg))
val content =
if (COMPLETION_HISTORY.is_file) {
@@ -139,9 +139,8 @@
YXML.string_of_tree(Semantic.Info(pos, No_Completion))
def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
- if (names.isEmpty) ""
- else
- YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
+ if_proper(names,
+ YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names))))
def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
report_names(pos, thys.map(name => (name, (Markup.THEORY, name))), total)
--- a/src/Pure/General/json_api.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/json_api.scala Sun Feb 26 21:17:10 2023 +0100
@@ -22,7 +22,7 @@
HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
def get_root(route: String = ""): Root =
- Root(get(if (route.isEmpty) "" else "/" + route).json)
+ Root(get(if_proper(route, "/" + route)).json)
}
sealed case class Root(json: JSON.T) {
--- a/src/Pure/General/mailman.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/mailman.scala Sun Feb 26 21:17:10 2023 +0100
@@ -453,9 +453,7 @@
def get(lines: List[String]): List[String] =
unapply(lines) getOrElse
- error("Missing delimiters:" +
- (if (bg.nonEmpty) " " else "") + bg +
- (if (en.nonEmpty) " " else "") + en)
+ error("Missing delimiters:" + if_proper(bg, " ") + bg + if_proper(en, " ") + en)
}
@@ -541,7 +539,7 @@
override def message_content(name: String, lines: List[String]): Message = {
def err(msg: String = ""): Nothing =
- error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
+ error("Malformed message: " + name + if_proper(msg, "\n" + msg))
val (head, body) =
try { (Head.get(lines), make_body(Body.get(lines))) }
@@ -596,7 +594,7 @@
override def message_content(name: String, lines: List[String]): Message = {
def err(msg: String = ""): Nothing =
- error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
+ error("Malformed message: " + name + if_proper(msg, "\n" + msg))
val (head, body) =
try { (Head.get(lines), make_body(Body.get(lines))) }
--- a/src/Pure/General/mercurial.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/mercurial.scala Sun Feb 26 21:17:10 2023 +0100
@@ -86,7 +86,7 @@
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
- if (s == "") "" else " " + prefix + " " + Bash.string(s)
+ if_proper(s, " " + prefix + " " + Bash.string(s))
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
--- a/src/Pure/General/position.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/position.scala Sun Feb 26 21:17:10 2023 +0100
@@ -116,18 +116,18 @@
def here(props: T, delimited: Boolean = true): String = {
val pos = props.filter(Markup.position_property)
- if (pos.isEmpty) ""
- else {
- val s0 =
- (Line.unapply(pos), File.unapply(pos)) match {
- case (Some(i), None) => "line " + i.toString
- case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
- case (None, Some(name)) => "file " + quote(name)
- case _ => ""
- }
- val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
- Markup(Markup.POSITION, pos).markup(s)
- }
+ if_proper(pos,
+ {
+ val s0 =
+ (Line.unapply(pos), File.unapply(pos)) match {
+ case (Some(i), None) => "line " + i.toString
+ case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name)
+ case (None, Some(name)) => "file " + quote(name)
+ case _ => ""
+ }
+ val s = if (s0 == "") s0 else if (delimited) " (" + s0 + ")" else s0
+ Markup(Markup.POSITION, pos).markup(s)
+ })
}
--- a/src/Pure/General/rsync.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/rsync.scala Sun Feb 26 21:17:10 2023 +0100
@@ -42,7 +42,7 @@
(if (clean) " --delete-excluded" else "") +
(if (list) " --list-only --no-human-readable" else "") +
filter.map(s => " --filter=" + Bash.string(s)).mkString +
- (if (args.nonEmpty) " " + Bash.strings(args) else "")
+ if_proper(args, " " + Bash.strings(args))
context.progress.bash(script, echo = true)
}
--- a/src/Pure/General/sql.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/sql.scala Sun Feb 26 21:17:10 2023 +0100
@@ -47,6 +47,9 @@
def enclose(s: Source): Source = "(" + s + ")"
def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
+ def separate(sql: Source): Source =
+ (if (sql.isEmpty || sql.startsWith(" ")) "" else " ") + sql
+
def select(columns: List[Column] = Nil, distinct: Boolean = false): Source =
"SELECT " + (if (distinct) "DISTINCT " else "") +
(if (columns.isEmpty) "*" else commas(columns.map(_.ident))) + " FROM "
@@ -55,12 +58,27 @@
val join_inner: Source = " INNER JOIN "
def join(outer: Boolean): Source = if (outer) join_outer else join_inner
- def member(x: Source, set: Iterable[String]): Source = {
- require(set.nonEmpty)
- set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+ def infix(op: Source, args: Iterable[Source]): Source = {
+ val body = args.iterator.filter(_.nonEmpty).mkString(" " + op + " ")
+ if_proper(body, enclose(body))
}
- def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
+ def AND(args: Iterable[Source]): Source = infix("AND", args)
+ def OR(args: Iterable[Source]): Source = infix("OR", args)
+
+ def and(args: Source*): Source = AND(args)
+ def or(args: Source*): Source = OR(args)
+
+ val TRUE: Source = "TRUE"
+ val FALSE: Source = "FALSE"
+
+ def equal(sql: Source, s: String): Source = sql + " = " + string(s)
+
+ def member(sql: Source, set: Iterable[String]): Source =
+ if (set.isEmpty) FALSE
+ else OR(set.iterator.map(equal(sql, _)).toList)
+
+ def where(sql: Source): Source = if_proper(sql, " WHERE " + sql)
/* types */
@@ -128,8 +146,11 @@
def defined: String = ident + " IS NOT NULL"
def undefined: String = ident + " IS NULL"
- def equal(s: String): Source = ident + " = " + string(s)
- def where_equal(s: String): Source = "WHERE " + equal(s)
+ def equal(s: String): Source = SQL.equal(ident, s)
+ def member(set: Iterable[String]): Source = SQL.member(ident, set)
+
+ def where_equal(s: String): Source = SQL.where(equal(s))
+ def where_member(set: Iterable[String]): Source = SQL.where(member(set))
override def toString: Source = ident
}
@@ -170,20 +191,19 @@
(if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
ident + " " + enclosure(index_columns.map(_.name))
- def insert_cmd(cmd: Source, sql: Source = ""): Source =
- cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
- (if (sql == "") "" else " " + sql)
+ def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
+ cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql)
- def insert(sql: Source = ""): Source = insert_cmd("INSERT", sql)
+ def insert(sql: Source = ""): Source = insert_cmd(sql = sql)
def delete(sql: Source = ""): Source =
- "DELETE FROM " + ident +
- (if (sql == "") "" else " " + sql)
+ "DELETE FROM " + ident + SQL.separate(sql)
def select(
- select_columns: List[Column] = Nil, sql: Source = "", distinct: Boolean = false): Source =
- SQL.select(select_columns, distinct = distinct) + ident +
- (if (sql == "") "" else " " + sql)
+ select_columns: List[Column] = Nil,
+ distinct: Boolean = false,
+ sql: Source = ""
+ ): Source = SQL.select(select_columns, distinct = distinct) + ident + SQL.separate(sql)
override def toString: Source = ident
}
@@ -367,8 +387,7 @@
}
def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
- using_statement(
- table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
+ using_statement(table.create(strict, sql_type) + SQL.separate(sql))(_.execute())
def create_index(table: Table, name: String, columns: List[Column],
strict: Boolean = false, unique: Boolean = false): Unit =
@@ -425,7 +444,7 @@
date_format.parse(res.string(column))
def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
- table.insert_cmd("INSERT OR IGNORE", sql = sql)
+ table.insert_cmd(cmd = "INSERT OR IGNORE", sql = sql)
}
}
@@ -501,8 +520,7 @@
}
def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
- table.insert_cmd("INSERT",
- sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
+ table.insert_cmd(sql = if_proper(sql, sql + " ") + "ON CONFLICT DO NOTHING")
/* notifications: IPC via database server */
@@ -516,8 +534,7 @@
def notify(name: String, payload: String = ""): Unit =
using_statement(
- "NOTIFY " + SQL.ident(name) +
- (if (payload.isEmpty) "" else ", " + SQL.string(payload)))(_.execute())
+ "NOTIFY " + SQL.ident(name) + if_proper(payload, ", " + SQL.string(payload)))(_.execute())
def get_notifications(): List[PGNotification] =
the_postgresql_connection.getNotifications() match {
--- a/src/Pure/General/ssh.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/ssh.scala Sun Feb 26 21:17:10 2023 +0100
@@ -19,7 +19,7 @@
if (control_path.isEmpty || control_path == Bash.string(control_path)) {
"ssh" +
(if (port > 0) " -p " + port else "") +
- (if (control_path.nonEmpty) " -o ControlPath=" + control_path else "")
+ if_proper(control_path, " -o ControlPath=" + control_path)
}
else error ("Malformed SSH control socket: " + quote(control_path))
@@ -130,8 +130,8 @@
control_master = master, control_path = control_path)
val cmd =
Config.command(command, config) +
- (if (opts.nonEmpty) " " + opts else "") +
- (if (args.nonEmpty) " -- " + args else "")
+ if_proper(opts, " " + opts) +
+ if_proper(args, " -- " + args)
Isabelle_System.bash(cmd, cwd = cwd,
redirect = redirect,
progress_stdout = progress_stdout,
@@ -155,7 +155,7 @@
}
def run_ssh(master: Boolean = false, opts: String = "", args: String = ""): Process_Result = {
- val args1 = Bash.string(host) + (if (args.nonEmpty) " " + args else "")
+ val args1 = Bash.string(host) + if_proper(args, " " + args)
run_command("ssh", master = master, opts = opts, args = args1)
}
--- a/src/Pure/General/timing.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/General/timing.scala Sun Feb 26 21:17:10 2023 +0100
@@ -26,7 +26,7 @@
val timing = stop - start
if (timing.is_relevant) {
val msg = if (message == null) null else message(result)
- output((if (msg == null || msg == "") "" else msg + ": ") + timing.message + " elapsed time")
+ output(if_proper(msg, msg + ": ") + timing.message + " elapsed time")
}
Exn.release(result)
--- a/src/Pure/Isar/keyword.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Isar/keyword.scala Sun Feb 26 21:17:10 2023 +0100
@@ -114,8 +114,8 @@
) {
override def toString: String =
kind +
- (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") +
- (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
+ if_proper(load_command, " (" + quote(load_command) + ")") +
+ if_proper(tags, tags.map(quote).mkString(" % ", " % ", ""))
def map(f: String => String): Spec =
copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f))
@@ -137,9 +137,7 @@
case Some(load_command) => " (" + quote(load_command) + ")"
case None => ""
}
- val kind_decl =
- if (kind == "") ""
- else " :: " + quote(kind) + load_decl
+ val kind_decl = if_proper(kind, " :: " + quote(kind) + load_decl)
quote(name) + kind_decl
}
entries.mkString("keywords\n ", " and\n ", "")
--- a/src/Pure/ML/ml_statistics.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/ML/ml_statistics.scala Sun Feb 26 21:17:10 2023 +0100
@@ -59,7 +59,7 @@
}
val env_prefix =
- if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
+ if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n")
Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
--- a/src/Pure/PIDE/resources.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/PIDE/resources.scala Sun Feb 26 21:17:10 2023 +0100
@@ -308,8 +308,7 @@
"Cyclic dependency of " + show_path(names)
private def required_by(initiators: List[Document.Node.Name]): String =
- if (initiators.isEmpty) ""
- else "\n(required by " + show_path(initiators.reverse) + ")"
+ if_proper(initiators, "\n(required by " + show_path(initiators.reverse) + ")")
}
final class Dependencies[A] private(
--- a/src/Pure/ROOT.ML Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/ROOT.ML Sun Feb 26 21:17:10 2023 +0100
@@ -366,4 +366,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
--- a/src/Pure/ROOT.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/ROOT.scala Sun Feb 26 21:17:10 2023 +0100
@@ -20,5 +20,6 @@
val proper_bool = Library.proper_bool _
val proper_string = Library.proper_string _
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
+ def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
}
--- a/src/Pure/System/isabelle_process.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/System/isabelle_process.scala Sun Feb 26 21:17:10 2023 +0100
@@ -58,7 +58,7 @@
case Session.Terminated(result) =>
if (!result.ok && !startup.is_finished) {
val syslog = session.syslog.content()
- val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog)
+ val err = "Session startup failed" + if_proper(syslog, ":\n" + syslog)
startup.fulfill(err)
}
terminated.fulfill(result)
--- a/src/Pure/System/isabelle_system.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/System/isabelle_system.scala Sun Feb 26 21:17:10 2023 +0100
@@ -47,6 +47,9 @@
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
+ def hostname(default: String = ""): String =
+ proper_string(default) getOrElse getenv_strict("ISABELLE_HOSTNAME")
+
/* services */
@@ -499,8 +502,6 @@
}
}
- def hostname(): String = bash("hostname -s").check.out
-
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
--- a/src/Pure/System/options.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/System/options.scala Sun Feb 26 21:17:10 2023 +0100
@@ -406,21 +406,30 @@
}
+ /* changed options */
+
+ def changed(defaults: Options = Options.init(prefs = "")): List[String] =
+ (for {
+ (name, opt2) <- options.iterator
+ opt1 = defaults.get(name)
+ if opt1.isEmpty || opt1.get.value != opt2.value
+ } yield (name, opt2.value)).toList.sortBy(_._1).map({ case (x, y) => Properties.Eq(x, y) })
+
+
/* save preferences */
- def save_prefs(file: Path = Options.PREFS): Unit = {
- val defaults: Options = Options.init(prefs = "")
- val changed =
- (for {
- (name, opt2) <- options.iterator
- opt1 = defaults.get(name)
- if opt1.isEmpty || opt1.get.value != opt2.value
- } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList
+ def make_prefs(defaults: Options = Options.init(prefs = "")): String = {
+ (for {
+ (name, opt2) <- options.iterator
+ opt1 = defaults.get(name)
+ if opt1.isEmpty || opt1.get.value != opt2.value
+ } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else ""))
+ .toList.sortBy(_._1)
+ .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
+ }
- val prefs =
- changed.sortBy(_._1)
- .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
-
+ def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init(prefs = "")): Unit = {
+ val prefs = make_prefs(defaults = defaults)
Isabelle_System.make_directory(file.dir)
File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
}
--- a/src/Pure/Thy/bibtex.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Thy/bibtex.scala Sun Feb 26 21:17:10 2023 +0100
@@ -680,7 +680,7 @@
"\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
" -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
(if (chronological) " -c" else "") +
- (if (title != "") " -h " + Bash.string(title) + " " else "") +
+ if_proper(title, " -h " + Bash.string(title) + " ") +
" " + File.bash_path(in_file) + " " + File.bash_path(out_file),
cwd = tmp_dir.file).check
@@ -813,7 +813,7 @@
def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
val body =
- (if (location.isEmpty) "" else Symbol.cartouche(location) + " in ") +
+ if_proper(location, Symbol.cartouche(location) + " in ") +
citations.map(quote).mkString(" and ")
cite_antiquotation(name, body)
}
--- a/src/Pure/Thy/document_build.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Thy/document_build.scala Sun Feb 26 21:17:10 2023 +0100
@@ -64,27 +64,29 @@
val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- "WHERE " + Data.session_name.equal(session_name) +
- (if (name == "") "" else " AND " + Data.name.equal(name))
+ SQL.where(
+ SQL.and(
+ Data.session_name.equal(session_name),
+ if_proper(name, Data.name.equal(name))))
}
- def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = {
- val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
- db.using_statement(select)(stmt =>
- stmt.execute_query().iterator({ res =>
- val name = res.string(Data.name)
- val sources = res.string(Data.sources)
- Document_Input(name, SHA1.fake_shasum(sources))
- }).toList)
- }
+ def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
+ db.using_statement(
+ Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name))
+ ) { stmt =>
+ (stmt.execute_query().iterator { res =>
+ val name = res.string(Data.name)
+ val sources = res.string(Data.sources)
+ Document_Input(name, SHA1.fake_shasum(sources))
+ }).toList
+ }
def read_document(
db: SQL.Database,
session_name: String,
name: String
): Option[Document_Output] = {
- val select = Data.table.select(sql = Data.where_equal(session_name, name))
- db.using_statement(select)({ stmt =>
+ db.using_statement(Data.table.select(sql = Data.where_equal(session_name, name))) { stmt =>
val res = stmt.execute_query()
if (res.next()) {
val name = res.string(Data.name)
@@ -94,7 +96,7 @@
Some(Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf))
}
else None
- })
+ }
}
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = {
@@ -357,7 +359,7 @@
"then\n" +
" " + (if (title.nonEmpty) program_running_script(title) else "") +
exe + " " + root_name_script() + "\n" +
- (if (after.isEmpty) "" else " " + after) +
+ if_proper(after, " " + after) +
"fi\n"
}
--- a/src/Pure/Thy/export.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Thy/export.scala Sun Feb 26 21:17:10 2023 +0100
@@ -42,9 +42,11 @@
List(session_name, theory_name, name, executable, compressed, body))
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
- "WHERE " + Data.session_name.equal(session_name) +
- (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
- (if (name == "") "" else " AND " + Data.name.equal(name))
+ SQL.where(
+ SQL.and(
+ Data.session_name.equal(session_name),
+ if_proper(theory_name, Data.theory_name.equal(theory_name)),
+ if_proper(name, Data.name.equal(name))))
}
def compound_name(a: String, b: String): String =
@@ -62,15 +64,15 @@
}
def readable(db: SQL.Database): Boolean = {
- val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
- db.using_statement(select)(stmt => stmt.execute_query().next())
+ db.using_statement(
+ Data.table.select(List(Data.name),
+ sql = Data.where_equal(session, theory, name)))(_.execute_query().next())
}
- def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = {
- val select =
+ def read(db: SQL.Database, cache: XML.Cache): Option[Entry] =
+ db.using_statement(
Data.table.select(List(Data.executable, Data.compressed, Data.body),
- Data.where_equal(session, theory, name))
- db.using_statement(select) { stmt =>
+ sql = Data.where_equal(session, theory, name))) { stmt =>
val res = stmt.execute_query()
if (res.next()) {
val executable = res.bool(Data.executable)
@@ -81,27 +83,24 @@
}
else None
}
- }
- }
-
- def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
- val select =
- Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
- SQL.order_by(List(Data.theory_name))
- db.using_statement(select)(stmt =>
- stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
}
- def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
- val select =
- Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
- SQL.order_by(List(Data.theory_name, Data.name))
- db.using_statement(select)(stmt =>
- stmt.execute_query().iterator(res =>
- Entry_Name(session = session_name,
- theory = res.string(Data.theory_name),
- name = res.string(Data.name))).toList)
- }
+ def read_theory_names(db: SQL.Database, session_name: String): List[String] =
+ db.using_statement(
+ Data.table.select(List(Data.theory_name), distinct = true,
+ sql = Data.where_equal(session_name) + SQL.order_by(List(Data.theory_name)))
+ ) { stmt => stmt.execute_query().iterator(_.string(Data.theory_name)).toList }
+
+ def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] =
+ db.using_statement(
+ Data.table.select(List(Data.theory_name, Data.name),
+ sql = Data.where_equal(session_name)) + SQL.order_by(List(Data.theory_name, Data.name))
+ ) { stmt =>
+ stmt.execute_query().iterator(res =>
+ Entry_Name(session = session_name,
+ theory = res.string(Data.theory_name),
+ name = res.string(Data.name))).toList
+ }
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
--- a/src/Pure/Thy/latex.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Thy/latex.scala Sun Feb 26 21:17:10 2023 +0100
@@ -231,14 +231,14 @@
}
def index_item(item: Index_Item.Value): String = {
- val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
+ val like = if_proper(item.like, index_escape(item.like) + "@")
val text = index_escape(latex_output(item.text))
like + text
}
def index_entry(entry: Index_Entry.Value): Text = {
val items = entry.items.map(index_item).mkString("!")
- val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind)
+ val kind = if_proper(entry.kind, "|" + index_escape(entry.kind))
latex_macro("index", XML.string(items + kind))
}
--- a/src/Pure/Thy/sessions.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Thy/sessions.scala Sun Feb 26 21:17:10 2023 +0100
@@ -77,8 +77,10 @@
SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- "WHERE " + Sources.session_name.equal(session_name) +
- (if (name == "") "" else " AND " + Sources.name.equal(name))
+ SQL.where(
+ SQL.and(
+ Sources.session_name.equal(session_name),
+ if_proper(name, Sources.name.equal(name))))
def load(session_base: Base, cache: Compress.Cache = Compress.Cache.none): Sources =
new Sources(
@@ -339,9 +341,7 @@
val resources = new Resources(session_background)
if (verbose || list_files) {
- val groups =
- if (info.groups.isEmpty) ""
- else info.groups.mkString(" (", " ", ")")
+ val groups = if_proper(info.groups, info.groups.mkString(" (", " ", ")"))
progress.echo("Session " + info.chapter + "/" + session_name + groups)
}
@@ -1512,8 +1512,9 @@
/* SQL database content */
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
- db.using_statement(Session_Info.table.select(List(column),
- Session_Info.session_name.where_equal(name))) { stmt =>
+ db.using_statement(
+ Session_Info.table.select(List(column),
+ sql = Session_Info.session_name.where_equal(name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) Bytes.empty else res.bytes(column)
}
@@ -1528,22 +1529,22 @@
db.transaction {
db.create_table(Session_Info.table)
db.using_statement(
- Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute())
+ Session_Info.table.delete(sql = Session_Info.session_name.where_equal(name)))(_.execute())
if (db.isInstanceOf[PostgreSQL.Database]) {
db.using_statement(Session_Info.augment_table)(_.execute())
}
db.create_table(Sources.table)
- db.using_statement(Sources.table.delete(Sources.where_equal(name)))(_.execute())
+ db.using_statement(Sources.table.delete(sql = Sources.where_equal(name)))(_.execute())
db.create_table(Export.Data.table)
db.using_statement(
- Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
+ Export.Data.table.delete(sql = Export.Data.session_name.where_equal(name)))(_.execute())
db.create_table(Document_Build.Data.table)
db.using_statement(
Document_Build.Data.table.delete(
- Document_Build.Data.session_name.where_equal(name)))(_.execute())
+ sql = Document_Build.Data.session_name.where_equal(name)))(_.execute())
}
}
@@ -1557,7 +1558,7 @@
session_info_exists(db) && {
db.using_statement(
Session_Info.table.select(List(Session_Info.session_name),
- Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
+ sql = Session_Info.session_name.where_equal(name)))(_.execute_query().next())
}
def write_session_info(
@@ -1610,8 +1611,8 @@
def read_build(db: SQL.Database, name: String): Option[Build_Info] = {
if (db.tables.contains(Session_Info.table.name)) {
- db.using_statement(Session_Info.table.select(Nil,
- Session_Info.session_name.where_equal(name))) { stmt =>
+ db.using_statement(
+ Session_Info.table.select(sql = Session_Info.session_name.where_equal(name))) { stmt =>
val res = stmt.execute_query()
if (!res.next()) None
else {
@@ -1652,18 +1653,18 @@
session_name: String,
name: String = ""
): List[Source_File] = {
- val select =
- Sources.table.select(Nil,
+ db.using_statement(
+ Sources.table.select(sql =
Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name)))
- db.using_statement(select) { stmt =>
- (stmt.execute_query().iterator { res =>
- val res_name = res.string(Sources.name)
- val digest = SHA1.fake_digest(res.string(Sources.digest))
- val compressed = res.bool(Sources.compressed)
- val body = res.bytes(Sources.body)
- Source_File(res_name, digest, compressed, body, cache.compress)
- }).toList
- }
+ ) { stmt =>
+ (stmt.execute_query().iterator { res =>
+ val res_name = res.string(Sources.name)
+ val digest = SHA1.fake_digest(res.string(Sources.digest))
+ val compressed = res.bool(Sources.compressed)
+ val body = res.bytes(Sources.body)
+ Source_File(res_name, digest, compressed, body, cache.compress)
+ }).toList
+ }
}
}
}
--- a/src/Pure/Tools/build.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/build.scala Sun Feb 26 21:17:10 2023 +0100
@@ -152,6 +152,7 @@
val build_context =
Build_Process.Context(store, build_deps, progress = progress,
+ hostname = Isabelle_System.hostname(build_options.string("build_hostname")),
build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
fresh_build = fresh_build, no_build = no_build, verbose = verbose,
session_setup = session_setup)
@@ -171,9 +172,10 @@
val results =
Isabelle_Thread.uninterruptible {
val engine = get_engine(build_options.string("build_engine"))
- val build_process = engine.init(build_context)
- val res = build_process.run()
- Results(build_context, res)
+ using(engine.init(build_context)) { build_process =>
+ val res = build_process.run()
+ Results(build_context, res)
+ }
}
if (export_files) {
@@ -293,9 +295,10 @@
val start_date = Date.now()
if (verbose) {
+ val hostname = Isabelle_System.hostname(options.string("build_hostname"))
progress.echo(
"Started at " + Build_Log.print_date(start_date) +
- " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
+ " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname +")")
progress.echo(Build_Log.Settings.show() + "\n")
}
--- a/src/Pure/Tools/build_job.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/build_job.scala Sun Feb 26 21:17:10 2023 +0100
@@ -13,18 +13,25 @@
trait Build_Job {
def job_name: String
- def numa_node: Option[Int] = None
+ def node_info: Build_Job.Node_Info
def start(): Unit = ()
def terminate(): Unit = ()
def is_finished: Boolean = false
def join: Process_Result = Process_Result.undefined
- def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, numa_node)
+ def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info)
}
object Build_Job {
- case class Abstract(
+ object Node_Info { def none: Node_Info = Node_Info("", None) }
+ sealed case class Node_Info(hostname: String, numa_node: Option[Int])
+
+ sealed case class Result(node_info: Node_Info, process_result: Process_Result) {
+ def ok: Boolean = process_result.ok
+ }
+
+ sealed case class Abstract(
override val job_name: String,
- override val numa_node: Option[Int]
+ override val node_info: Node_Info
) extends Build_Job {
override def make_abstract: Abstract = this
}
@@ -36,13 +43,13 @@
resources: Resources,
session_setup: (String, Session) => Unit,
val input_heaps: SHA1.Shasum,
- override val numa_node: Option[Int]
+ override val node_info: Node_Info
) extends Build_Job {
def session_name: String = session_background.session_name
def job_name: String = session_name
val info: Sessions.Info = session_background.sessions_structure(session_name)
- val options: Options = NUMA.policy_options(info.options, numa_node)
+ val options: Options = NUMA.policy_options(info.options, node_info.numa_node)
val session_sources: Sessions.Sources =
Sessions.Sources.load(session_background.base, cache = store.cache.compress)
--- a/src/Pure/Tools/build_process.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/build_process.scala Sun Feb 26 21:17:10 2023 +0100
@@ -68,13 +68,15 @@
store: Sessions.Store,
deps: Sessions.Deps,
progress: Progress = new Progress,
+ hostname: String = Isabelle_System.hostname(),
+ numa_shuffling: Boolean = false,
build_heap: Boolean = false,
- numa_shuffling: Boolean = false,
max_jobs: Int = 1,
fresh_build: Boolean = false,
no_build: Boolean = false,
verbose: Boolean = false,
- session_setup: (String, Session) => Unit = (_, _) => ()
+ session_setup: (String, Session) => Unit = (_, _) => (),
+ instance: String = UUID.random().toString
): Context = {
val sessions_structure = deps.sessions_structure
val build_graph = sessions_structure.build_graph
@@ -120,25 +122,27 @@
}
val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
- new Context(store, deps, sessions, ordering, progress, numa_nodes,
+ new Context(instance, store, deps, sessions, ordering, progress, hostname, numa_nodes,
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
no_build = no_build, verbose = verbose, session_setup)
}
}
final class Context private(
+ val instance: String,
val store: Sessions.Store,
val deps: Sessions.Deps,
sessions: Map[String, Session_Context],
val ordering: Ordering[String],
val progress: Progress,
+ val hostname: String,
val numa_nodes: List[Int],
val build_heap: Boolean,
val max_jobs: Int,
val fresh_build: Boolean,
val no_build: Boolean,
val verbose: Boolean,
- val session_setup: (String, Session) => Unit
+ val session_setup: (String, Session) => Unit,
) {
def sessions_structure: Sessions.Structure = deps.sessions_structure
@@ -161,12 +165,14 @@
case class Result(
current: Boolean,
output_heap: SHA1.Shasum,
+ node_info: Build_Job.Node_Info,
process_result: Process_Result
) {
def ok: Boolean = process_result.ok
}
sealed case class State(
+ serial: Long = 0,
numa_index: Int = 0,
pending: List[Entry] = Nil,
running: Map[String, Build_Job] = Map.empty,
@@ -176,7 +182,8 @@
if (numa_nodes.isEmpty) (None, this)
else {
val available = numa_nodes.zipWithIndex
- val used = Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
+ val used =
+ Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i)
val candidates = available.drop(numa_index) ::: available.take(numa_index)
val (n, i) =
candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
@@ -211,9 +218,10 @@
name: String,
current: Boolean,
output_heap: SHA1.Shasum,
- process_result: Process_Result
+ process_result: Process_Result,
+ node_info: Build_Job.Node_Info = Build_Job.Node_Info.none
): State = {
- val result = Build_Process.Result(current, output_heap, process_result)
+ val result = Build_Process.Result(current, output_heap, node_info, process_result)
copy(results = results + (name -> result))
}
@@ -222,6 +230,263 @@
}
+ /* SQL data model */
+
+ object Data {
+ val database = Path.explode("$ISABELLE_HOME_USER/build.db")
+
+ def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
+ SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
+
+ object Generic {
+ val instance = SQL.Column.string("instance")
+ val name = SQL.Column.string("name")
+
+ def sql_equal(instance: String = "", name: String = ""): SQL.Source =
+ SQL.and(
+ if_proper(instance, Generic.instance.equal(instance)),
+ if_proper(name, Generic.name.equal(name)))
+
+ def sql_member(instance: String = "", names: Iterable[String] = Nil): SQL.Source =
+ SQL.and(
+ if_proper(instance, Generic.instance.equal(instance)),
+ if_proper(names, Generic.name.member(names)))
+ }
+
+ object Config {
+ val instance = Generic.instance.make_primary_key
+ val ml_identifier = SQL.Column.string("ml_identifier")
+ val options = SQL.Column.string("options")
+
+ val table = make_table("", List(instance, ml_identifier, options))
+ }
+
+ object State {
+ val instance = Generic.instance.make_primary_key
+ val serial = SQL.Column.long("serial")
+ val numa_index = SQL.Column.int("numa_index")
+
+ val table = make_table("state", List(instance, serial, numa_index))
+ }
+
+ object Pending {
+ val name = Generic.name.make_primary_key
+ val deps = SQL.Column.string("deps")
+ val info = SQL.Column.string("info")
+
+ val table = make_table("pending", List(name, deps, info))
+ }
+
+ object Running {
+ val name = Generic.name.make_primary_key
+ val hostname = SQL.Column.string("hostname")
+ val numa_node = SQL.Column.int("numa_node")
+
+ val table = make_table("running", List(name, hostname, numa_node))
+ }
+
+ object Results {
+ val name = Generic.name.make_primary_key
+ val hostname = SQL.Column.string("hostname")
+ val numa_node = SQL.Column.string("numa_node")
+ val rc = SQL.Column.int("rc")
+ val out = SQL.Column.string("out")
+ val err = SQL.Column.string("err")
+ val timing_elapsed = SQL.Column.long("timing_elapsed")
+ val timing_cpu = SQL.Column.long("timing_cpu")
+ val timing_gc = SQL.Column.long("timing_gc")
+
+ val table =
+ make_table("results",
+ List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc))
+ }
+
+ def read_pending(db: SQL.Database): List[Entry] =
+ db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt =>
+ List.from(
+ stmt.execute_query().iterator { res =>
+ val name = res.string(Pending.name)
+ val deps = res.string(Pending.deps)
+ val info = res.string(Pending.info)
+ Entry(name, split_lines(deps), info = JSON.Object.parse(info))
+ })
+ }
+
+ def update_pending(db: SQL.Database, pending: List[Entry]): Boolean = {
+ val old_pending = read_pending(db)
+ val (delete, insert) = Library.symmetric_difference(old_pending, pending)
+
+ if (delete.nonEmpty) {
+ db.using_statement(
+ Pending.table.delete(
+ sql = SQL.where(Generic.sql_member(names = delete.map(_.name)))))(_.execute())
+ }
+
+ for (entry <- insert) {
+ db.using_statement(Pending.table.insert()) { stmt =>
+ stmt.string(1) = entry.name
+ stmt.string(2) = cat_lines(entry.deps)
+ stmt.string(3) = JSON.Format(entry.info)
+ stmt.execute()
+ }
+ }
+
+ delete.nonEmpty || insert.nonEmpty
+ }
+
+ def read_running(db: SQL.Database): List[Build_Job.Abstract] =
+ db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt =>
+ List.from(
+ stmt.execute_query().iterator { res =>
+ val name = res.string(Running.name)
+ val hostname = res.string(Running.hostname)
+ val numa_node = res.get_int(Running.numa_node)
+ Build_Job.Abstract(name, Build_Job.Node_Info(hostname, numa_node))
+ })
+ }
+
+ def update_running(db: SQL.Database, running: Map[String, Build_Job]): Boolean = {
+ val old_running = read_running(db)
+ val abs_running = running.valuesIterator.map(_.make_abstract).toList
+
+ val (delete, insert) = Library.symmetric_difference(old_running, abs_running)
+
+ if (delete.nonEmpty) {
+ db.using_statement(
+ Running.table.delete(
+ sql = SQL.where(Generic.sql_member(names = delete.map(_.job_name)))))(_.execute())
+ }
+
+ for (job <- insert) {
+ db.using_statement(Running.table.insert()) { stmt =>
+ stmt.string(1) = job.job_name
+ stmt.string(2) = job.node_info.hostname
+ stmt.int(3) = job.node_info.numa_node
+ stmt.execute()
+ }
+ }
+
+ delete.nonEmpty || insert.nonEmpty
+ }
+
+ def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] =
+ db.using_statement(
+ Results.table.select(sql = if_proper(names, Results.name.where_member(names)))) { stmt =>
+ Map.from(
+ stmt.execute_query().iterator { res =>
+ val name = res.string(Results.name)
+ val hostname = res.string(Results.hostname)
+ val numa_node = res.get_int(Results.numa_node)
+ val rc = res.int(Results.rc)
+ val out = res.string(Results.out)
+ val err = res.string(Results.err)
+ val timing_elapsed = res.long(Results.timing_elapsed)
+ val timing_cpu = res.long(Results.timing_cpu)
+ val timing_gc = res.long(Results.timing_gc)
+ val node_info = Build_Job.Node_Info(hostname, numa_node)
+ val process_result =
+ Process_Result(rc,
+ out_lines = split_lines(out),
+ err_lines = split_lines(err),
+ timing = Timing(Time.ms(timing_elapsed), Time.ms(timing_cpu), Time.ms(timing_gc)))
+ name -> Build_Job.Result(node_info, process_result)
+ })
+ }
+
+ def read_results_name(db: SQL.Database): Set[String] =
+ db.using_statement(Results.table.select(List(Results.name)))(stmt =>
+ Set.from(stmt.execute_query().iterator(_.string(Results.name))))
+
+ def update_results(db: SQL.Database, results: Map[String, Build_Process.Result]): Boolean = {
+ val old_results = read_results_name(db)
+ val insert = results.iterator.filterNot(p => old_results.contains(p._1)).toList
+
+ for ((name, result) <- insert) {
+ val node_info = result.node_info
+ val process_result = result.process_result
+ db.using_statement(Results.table.insert()) { stmt =>
+ stmt.string(1) = name
+ stmt.string(2) = node_info.hostname
+ stmt.int(3) = node_info.numa_node
+ stmt.int(4) = process_result.rc
+ stmt.string(5) = cat_lines(process_result.out_lines)
+ stmt.string(6) = cat_lines(process_result.err_lines)
+ stmt.long(7) = process_result.timing.elapsed.ms
+ stmt.long(8) = process_result.timing.cpu.ms
+ stmt.long(9) = process_result.timing.gc.ms
+ stmt.execute()
+ }
+ }
+
+ insert.nonEmpty
+ }
+
+ def write_config(db: SQL.Database, instance: String, hostname: String, options: Options): Unit =
+ db.using_statement(Config.table.insert()) { stmt =>
+ stmt.string(1) = instance
+ stmt.string(2) = Isabelle_System.getenv("ML_IDENTIFIER")
+ stmt.string(3) = options.make_prefs(Options.init(prefs = ""))
+ stmt.execute()
+ }
+
+ def read_state(db: SQL.Database, instance: String): (Long, Int) =
+ db.using_statement(
+ State.table.select(sql = SQL.where(Generic.sql_equal(instance = instance)))
+ ) { stmt =>
+ (stmt.execute_query().iterator { res =>
+ val serial = res.long(State.serial)
+ val numa_index = res.int(State.numa_index)
+ (serial, numa_index)
+ }).nextOption.getOrElse(error("No build state instance " + instance + " in database " + db))
+ }
+
+ def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit =
+ db.using_statement(State.table.insert()) { stmt =>
+ stmt.string(1) = instance
+ stmt.long(2) = serial
+ stmt.int(3) = numa_index
+ stmt.execute()
+ }
+
+ def reset_state(db: SQL.Database, instance: String): Unit =
+ db.using_statement(
+ State.table.delete(sql = SQL.where(Generic.sql_equal(instance = instance))))(_.execute())
+
+ def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
+ val tables =
+ List(Config.table, State.table, Pending.table, Running.table, Results.table)
+
+ for (table <- tables) db.create_table(table)
+
+ val old_pending = Data.read_pending(db)
+ if (old_pending.nonEmpty) {
+ error("Cannot init build process, because of unfinished " +
+ commas_quote(old_pending.map(_.name)))
+ }
+
+ for (table <- tables) db.using_statement(table.delete())(_.execute())
+
+ write_config(db, build_context.instance, build_context.hostname, build_context.store.options)
+ write_state(db, build_context.instance, 0, 0)
+ }
+
+ def update_database(db: SQL.Database, instance: String, state: State): State = {
+ val ch1 = update_pending(db, state.pending)
+ val ch2 = update_running(db, state.running)
+ val ch3 = update_results(db, state.results)
+
+ val (serial0, _) = read_state(db, instance)
+ val serial = if (ch1 || ch2 || ch3) serial0 + 1 else serial0
+ if (serial != serial0) {
+ reset_state(db, instance)
+ write_state(db, instance, serial, state.numa_index)
+ }
+
+ state.copy(serial = serial)
+ }
+ }
+
+
/* main process */
def session_finished(session_name: String, process_result: Process_Result): String =
@@ -235,7 +500,7 @@
}
}
-class Build_Process(protected val build_context: Build_Process.Context) {
+class Build_Process(protected val build_context: Build_Process.Context) extends AutoCloseable {
protected val store: Sessions.Store = build_context.store
protected val build_options: Options = store.options
protected val build_deps: Sessions.Deps = build_context.deps
@@ -249,6 +514,18 @@
case log_file => Logger.make(Some(Path.explode(log_file)))
}
+ protected val database: Option[SQL.Database] =
+ if (!build_options.bool("build_database") || true /*FIXME*/) None
+ else if (store.database_server) Some(store.open_database_server())
+ else {
+ val db = SQLite.open_database(Build_Process.Data.database)
+ try { Isabelle_System.chmod("600", Build_Process.Data.database) }
+ catch { case exn: Throwable => db.close(); throw exn }
+ Some(db)
+ }
+
+ def close(): Unit = database.foreach(_.close())
+
// global state
protected var _state: Build_Process.State = init_state()
@@ -327,7 +604,7 @@
_state = _state.
remove_pending(session_name).
remove_running(session_name).
- make_result(session_name, false, output_heap, process_result_tail)
+ make_result(session_name, false, output_heap, process_result_tail, node_info = job.node_info)
}
}
@@ -395,9 +672,10 @@
val job =
synchronized {
val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
+ val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
new Build_Job.Build_Session(progress, session_background, store, do_store,
- resources, build_context.session_setup, input_heaps, numa_node)
+ resources, build_context.session_setup, input_heaps, node_info)
_state = state1.add_running(session_name, job)
job
}
@@ -413,6 +691,24 @@
}
}
+ protected def setup_database(): Unit =
+ for (db <- database) {
+ synchronized {
+ db.transaction {
+ Build_Process.Data.init_database(db, build_context)
+ }
+ }
+ db.rebuild()
+ }
+ protected def sync_database(): Unit =
+ for (db <- database) {
+ synchronized {
+ db.transaction {
+ _state = Build_Process.Data.update_database(db, build_context.instance, _state)
+ }
+ }
+ }
+
protected def sleep(): Unit =
Isabelle_Thread.interrupt_handler(_ => progress.stop()) {
build_options.seconds("editor_input_delay").sleep()
@@ -424,14 +720,18 @@
Map.empty[String, Process_Result]
}
else {
+ setup_database()
while (!finished()) {
if (progress.stopped) stop_running()
for (job <- finished_running()) finish_job(job)
next_pending() match {
- case Some(name) => start_job(name)
- case None => sleep()
+ case Some(name) =>
+ start_job(name)
+ case None =>
+ sync_database()
+ sleep()
}
}
synchronized {
--- a/src/Pure/Tools/dotnet_setup.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/dotnet_setup.scala Sun Feb 26 21:17:10 2023 +0100
@@ -128,9 +128,9 @@
if (platform_dir.is_dir && force) Isabelle_System.rm_tree(platform_dir)
val script =
platform.exec + " " + File.bash_platform_path(install) +
- (if (version.nonEmpty) " -Version " + Bash.string(version) else "") +
+ if_proper(version, " -Version " + Bash.string(version)) +
" -Architecture " + Bash.string(platform.arch) +
- (if (platform.os.nonEmpty) " -OS " + Bash.string(platform.os) else "") +
+ if_proper(platform.os, " -OS " + Bash.string(platform.os)) +
" -InstallDir " + Bash.string(platform.name) +
(if (dry_run) " -DryRun" else "") +
" -NoPath"
--- a/src/Pure/Tools/dump.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/dump.scala Sun Feb 26 21:17:10 2023 +0100
@@ -353,7 +353,7 @@
Output.clean_yxml(
"FAILED theory " + bad.name +
(if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") +
- (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", ""))))
+ if_proper(bad.errors, bad.errors.mkString("\n", "\n", ""))))
val pending_msgs =
use_theories_result.nodes_pending match {
--- a/src/Pure/Tools/phabricator.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/phabricator.scala Sun Feb 26 21:17:10 2023 +0100
@@ -52,7 +52,7 @@
val default_name = "vcs"
def phabricator_name(name: String = "", ext: String = ""): String =
- "phabricator" + (if (name.isEmpty) "" else "-" + name) + (if (ext.isEmpty) "" else "." + ext)
+ "phabricator" + if_proper(name, "-" + name) + if_proper(ext, "." + ext)
def isabelle_phabricator_name(name: String = "", ext: String = ""): String =
"isabelle-" + phabricator_name(name = name, ext = ext)
@@ -81,7 +81,7 @@
body: String = "",
exit: String = ""): String = {
"""#!/bin/bash
-""" + (if (init.nonEmpty) "\n" + init else "") + """
+""" + if_proper(init, "\n" + init) + """
{
while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
do
@@ -92,7 +92,7 @@
} < /dev/null
done
} < """ + File.bash_path(global_config) + "\n" +
- (if (exit.nonEmpty) "\n" + exit + "\n" else "")
+ if_proper(exit, "\n" + exit + "\n")
}
sealed case class Config(name: String, root: Path) {
--- a/src/Pure/Tools/server.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/Tools/server.scala Sun Feb 26 21:17:10 2023 +0100
@@ -367,12 +367,13 @@
def list(db: SQLite.Database): List[Info] =
if (db.tables.contains(Data.table.name)) {
- db.using_statement(Data.table.select())(stmt =>
+ db.using_statement(Data.table.select()) { stmt =>
stmt.execute_query().iterator(res =>
Info(
res.string(Data.name),
res.int(Data.port),
- res.string(Data.password))).toList.sortBy(_.name))
+ res.string(Data.password))).toList.sortBy(_.name)
+ }
}
else Nil
@@ -390,8 +391,8 @@
Isabelle_System.chmod("600", Data.database)
db.create_table(Data.table)
list(db).filterNot(_.active).foreach(server_info =>
- db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
- _.execute()))
+ db.using_statement(
+ Data.table.delete(sql = Data.name.where_equal(server_info.name)))(_.execute()))
}
db.transaction {
find(db, name) match {
@@ -402,7 +403,7 @@
val server = new Server(port, log)
val server_info = Info(name, server.port, server.password)
- db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute())
+ db.using_statement(Data.table.delete(sql = Data.name.where_equal(name)))(_.execute())
db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = server_info.name
stmt.int(2) = server_info.port
--- a/src/Pure/library.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/library.scala Sun Feb 26 21:17:10 2023 +0100
@@ -271,6 +271,9 @@
case _ => error("Single argument expected")
}
+ def symmetric_difference[A](xs: List[A], ys: List[A]): (List[A], List[A]) =
+ (xs.filterNot(ys.toSet), ys.filterNot(xs.toSet))
+
/* proper values */
@@ -283,6 +286,9 @@
def proper_list[A](list: List[A]): Option[List[A]] =
if (list == null || list.isEmpty) None else Some(list)
+ def if_proper[A](x: Iterable[A], body: => String): String =
+ if (x == null || x.isEmpty) "" else body
+
/* reflection */
--- a/src/Pure/term.scala Sat Feb 25 17:35:48 2023 +0000
+++ b/src/Pure/term.scala Sun Feb 26 21:17:10 2023 +0100
@@ -41,21 +41,21 @@
override def toString: String =
if (this == dummyT) "_"
- else "Type(" + name + (if (args.isEmpty) "" else "," + args) + ")"
+ else "Type(" + name + if_proper(args, "," + args) + ")"
}
case class TFree(name: String, sort: Sort = Nil) extends Typ {
private lazy val hash: Int = ("TFree", name, sort).hashCode()
override def hashCode(): Int = hash
override def toString: String =
- "TFree(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
+ "TFree(" + name + if_proper(sort, "," + sort) + ")"
}
case class TVar(name: Indexname, sort: Sort = Nil) extends Typ {
private lazy val hash: Int = ("TVar", name, sort).hashCode()
override def hashCode(): Int = hash
override def toString: String =
- "TVar(" + name + (if (sort.isEmpty) "" else "," + sort) + ")"
+ "TVar(" + name + if_proper(sort, "," + sort) + ")"
}
val dummyT: Type = Type("dummy")
@@ -72,7 +72,7 @@
override def toString: String =
if (this == dummy) "_"
- else "Const(" + name + (if (typargs.isEmpty) "" else "," + typargs) + ")"
+ else "Const(" + name + if_proper(typargs, "," + typargs) + ")"
}
case class Free(name: String, typ: Typ = dummyT) extends Term {
private lazy val hash: Int = ("Free", name, typ).hashCode()