--- a/src/Pure/Admin/build_history.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/build_history.scala Sat Jun 17 17:41:02 2023 +0200
@@ -314,8 +314,7 @@
val properties =
if (database.is_file) {
- using(SQLite.open_database(database))(db =>
- store.read_ml_statistics(db, session_name))
+ using(SQLite.open_database(database))(store.read_ml_statistics(_, session_name))
}
else if (log_gz.is_file) {
Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
@@ -340,7 +339,7 @@
val errors =
if (database.is_file) {
try {
- using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
+ using(SQLite.open_database(database))(store.read_errors(_, session_name))
} // column "errors" could be missing
catch { case _: java.sql.SQLException => Nil }
}
--- a/src/Pure/Admin/build_log.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/build_log.scala Sat Jun 17 17:41:02 2023 +0200
@@ -686,7 +686,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 +
- SQL.where(SQL.and(version1.defined, version2.defined)))
+ SQL.where_and(version1.defined, version2.defined))
}
@@ -729,9 +729,9 @@
SQL.Table("recent_pull_date", table.columns,
table.select(table.columns, sql =
- SQL.where(
- SQL.or(pull_date(afp)(table).ident + " > " + recent_time(days),
- SQL.and(eq_rev, eq_rev2)))))
+ SQL.where_or(
+ pull_date(afp)(table).ident + " > " + recent_time(days),
+ SQL.and(eq_rev, eq_rev2))))
}
def select_recent_log_names(days: Int): PostgreSQL.Source = {
@@ -1102,11 +1102,10 @@
else (columns1, table1.ident)
val where =
- SQL.where(
- SQL.and(
- Data.log_name(table1).equal(log_name),
- Data.session_name(table1).ident + " <> ''",
- if_proper(session_names, Data.session_name(table1).member(session_names))))
+ SQL.where_and(
+ Data.log_name(table1).equal(log_name),
+ Data.session_name(table1).ident + " <> ''",
+ if_proper(session_names, Data.session_name(table1).member(session_names)))
val sessions =
db.execute_query_statement(
--- a/src/Pure/Admin/build_release.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/build_release.scala Sat Jun 17 17:41:02 2023 +0200
@@ -318,7 +318,7 @@
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
- File.set_executable(script_path, true)
+ File.set_executable(script_path)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
@@ -483,7 +483,7 @@
progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
- execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
+ execute(context.dist_dir, """chmod -R a+r,u+w,g=o .""")
execute(context.dist_dir,
"""find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
execute_tar(context.dist_dir, "-czf " +
@@ -744,7 +744,7 @@
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
- File.set_executable(isabelle_target + cygwin_bat, true)
+ File.set_executable(isabelle_target + cygwin_bat)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
@@ -784,7 +784,7 @@
Bytes.write(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
- File.set_executable(context.dist_dir + isabelle_exe, true)
+ File.set_executable(context.dist_dir + isabelle_exe)
}
other_isabelle.cleanup()
@@ -852,8 +852,7 @@
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
- execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
- execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
+ execute(tmp_dir, "chmod -R a+r,g=o " + Bash.string(context.dist_name))
execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
" " + Bash.string(context.dist_name + "/browser_info"))
}
--- a/src/Pure/Admin/build_status.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/build_status.scala Sat Jun 17 17:41:02 2023 +0200
@@ -61,15 +61,14 @@
(if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
Build_Log.Data.universal_table.select(columns, distinct = true, sql =
- SQL.where(
- SQL.and(
- Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
- Build_Log.Data.status.member(
- List(
- Build_Log.Session_Status.finished.toString,
- Build_Log.Session_Status.failed.toString)),
- if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
- if_proper(sql, SQL.enclose(sql)))))
+ SQL.where_and(
+ Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
+ Build_Log.Data.status.member(
+ List(
+ Build_Log.Session_Status.finished.toString,
+ Build_Log.Session_Status.failed.toString)),
+ if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
+ if_proper(sql, SQL.enclose(sql))))
}
}
--- a/src/Pure/Admin/component_cvc5.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/component_cvc5.scala Sat Jun 17 17:41:02 2023 +0200
@@ -53,7 +53,7 @@
Isabelle_System.make_directory(platform_dir)
Isabelle_System.download_file(url, platform_exe, progress = progress)
- File.set_executable(platform_exe, true)
+ File.set_executable(platform_exe)
}
--- a/src/Pure/Admin/component_cygwin.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/component_cygwin.scala Sat Jun 17 17:41:02 2023 +0200
@@ -33,7 +33,7 @@
File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
- File.set_executable(cygwin_exe, true)
+ File.set_executable(cygwin_exe)
Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
val res =
--- a/src/Pure/Admin/component_sqlite.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/component_sqlite.scala Sat Jun 17 17:41:02 2023 +0200
@@ -72,7 +72,7 @@
Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
}
- File.set_executable(component_dir.path + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
+ File.set_executable(component_dir.path + Path.explode("x86_64-windows/sqlitejdbc.dll"))
}
}
--- a/src/Pure/Admin/other_isabelle.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Admin/other_isabelle.scala Sat Jun 17 17:41:02 2023 +0200
@@ -112,7 +112,7 @@
if (!ssh.is_file(dummy_stty_remote)) {
ssh.make_directory(dummy_stty_remote.dir)
ssh.write_file(dummy_stty_remote, dummy_stty)
- ssh.set_executable(dummy_stty_remote, true)
+ ssh.set_executable(dummy_stty_remote)
}
try {
bash(
--- a/src/Pure/General/file.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/General/file.scala Sat Jun 17 17:41:02 2023 +0200
@@ -12,7 +12,7 @@
InputStreamReader, File => JFile, IOException}
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
FileVisitOption, FileVisitResult}
-import java.nio.file.attribute.BasicFileAttributes
+import java.nio.file.attribute.{BasicFileAttributes, PosixFilePermission}
import java.net.{URI, URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.EnumSet
@@ -362,12 +362,33 @@
/* permissions */
+ private val restrict_perms: List[PosixFilePermission] =
+ List(
+ PosixFilePermission.GROUP_READ,
+ PosixFilePermission.GROUP_WRITE,
+ PosixFilePermission.GROUP_EXECUTE,
+ PosixFilePermission.OTHERS_READ,
+ PosixFilePermission.OTHERS_WRITE,
+ PosixFilePermission.OTHERS_EXECUTE)
+
+ def restrict(path: Path): Unit =
+ if (Platform.is_windows) Isabelle_System.chmod("g-rwx,o-rwx", path)
+ else {
+ val perms = Files.getPosixFilePermissions(path.java_path)
+ var perms_changed = false
+ for (p <- restrict_perms if perms.contains(p)) {
+ perms.remove(p)
+ perms_changed = true
+ }
+ if (perms_changed) Files.setPosixFilePermissions(path.java_path, perms)
+ }
+
def is_executable(path: Path): Boolean = {
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
else path.file.canExecute
}
- def set_executable(path: Path, flag: Boolean): Unit = {
+ def set_executable(path: Path, flag: Boolean = false): Unit = {
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
else path.file.setExecutable(flag, false)
--- a/src/Pure/General/integer.ML Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/General/integer.ML Sat Jun 17 17:41:02 2023 +0200
@@ -7,6 +7,7 @@
signature INTEGER =
sig
val build: (int -> int) -> int
+ val build1: (int -> int) -> int
val min: int -> int -> int
val max: int -> int -> int
val add: int -> int -> int
@@ -31,6 +32,7 @@
struct
fun build (f: int -> int) = f 0;
+fun build1 (f: int -> int) = f 1;
fun min x y = Int.min (x, y);
fun max x y = Int.max (x, y);
@@ -38,8 +40,8 @@
fun add x y = x + y;
fun mult x y = x * y;
-fun sum xs = fold add xs 0;
-fun prod xs = fold mult xs 1;
+val sum = build o fold add;
+val prod = build1 o fold mult;
fun sign x = int_ord (x, 0);
--- a/src/Pure/General/sql.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/General/sql.scala Sat Jun 17 17:41:02 2023 +0200
@@ -72,13 +72,17 @@
val TRUE: Source = "TRUE"
val FALSE: Source = "FALSE"
- def equal(sql: Source, s: String): Source = sql + " = " + string(s)
+ def equal(sql: Source, x: Int): Source = sql + " = " + x
+ def equal(sql: Source, x: Long): Source = sql + " = " + x
+ def equal(sql: Source, x: String): Source = sql + " = " + string(x)
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)
+ def where_and(args: Source*): Source = where(and(args:_*))
+ def where_or(args: Source*): Source = where(or(args:_*))
/* types */
@@ -146,12 +150,19 @@
def defined: String = ident + " IS NOT NULL"
def undefined: String = ident + " IS NULL"
- def equal(s: String): Source = SQL.equal(ident, s)
- def member(set: Iterable[String]): Source = SQL.member(ident, set)
+ def equal(x: Int): Source = SQL.equal(ident, x)
+ def equal(x: Long): Source = SQL.equal(ident, x)
+ def equal(x: String): Source = SQL.equal(ident, x)
- def where_equal(s: String): Source = SQL.where(equal(s))
+ def where_equal(x: Int): Source = SQL.where(equal(x))
+ def where_equal(x: Long): Source = SQL.where(equal(x))
+ def where_equal(x: String): Source = SQL.where(equal(x))
+
+ def member(set: Iterable[String]): Source = SQL.member(ident, set)
def where_member(set: Iterable[String]): Source = SQL.where(member(set))
+ def max: Column = copy(expr = "MAX(" + ident + ")")
+
override def toString: Source = ident
}
@@ -229,13 +240,8 @@
def iterator: Iterator[Table] = list.iterator
// requires transaction
- def create_lock(db: Database): Unit = {
- foreach(db.create_table(_))
- lock(db)
- }
-
- // requires transaction
- def lock(db: Database): Unit = {
+ def lock(db: Database, create: Boolean = false): Unit = {
+ if (create) foreach(db.create_table(_))
val sql = db.lock_tables(list)
if (sql.nonEmpty) db.execute_statement(sql)
}
@@ -398,8 +404,8 @@
finally { connection.setAutoCommit(auto_commit) }
}
- def transaction_lock[A](tables: Tables)(body: => A): A =
- transaction { tables.lock(db); body }
+ def transaction_lock[A](tables: Tables, create: Boolean = false)(body: => A): A =
+ transaction { tables.lock(db, create = create); body }
def lock_tables(tables: List[Table]): Source = "" // PostgreSQL only
@@ -482,13 +488,18 @@
Class.forName("org.sqlite.JDBC")
}
- def open_database(path: Path): Database = {
+ def open_database(path: Path, restrict: Boolean = false): Database = {
init_jdbc
val path0 = path.expand
val s0 = File.platform_path(path0)
val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0
val connection = DriverManager.getConnection("jdbc:sqlite:" + s1)
- new Database(path0.toString, connection)
+ val db = new Database(path0.toString, connection)
+
+ try { if (restrict) File.restrict(path0) }
+ catch { case exn: Throwable => db.close(); throw exn }
+
+ db
}
class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
--- a/src/Pure/General/ssh.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/General/ssh.scala Sat Jun 17 17:41:02 2023 +0200
@@ -241,7 +241,12 @@
if (cmd.nonEmpty) run_sftp(cmd + " " + sftp_path(path))
}
- override def set_executable(path: Path, flag: Boolean): Unit =
+ override def restrict(path: Path): Unit =
+ if (!execute("chmod g-rwx,o-rwx " + bash_path(path)).ok) {
+ error("Failed to change permissions of " + quote(remote_path(path)))
+ }
+
+ override def set_executable(path: Path, flag: Boolean = false): Unit =
if (!execute("chmod a" + (if (flag) "+" else "-") + "x " + bash_path(path)).ok) {
error("Failed to change executable status of " + quote(remote_path(path)))
}
@@ -402,7 +407,9 @@
def is_dir(path: Path): Boolean = path.is_dir
def is_file(path: Path): Boolean = path.is_file
def delete(path: Path): Unit = path.file.delete
- def set_executable(path: Path, flag: Boolean): Unit = File.set_executable(path, flag)
+ def restrict(path: Path): Unit = File.restrict(path)
+ def set_executable(path: Path, flag: Boolean = false): Unit =
+ File.set_executable(path, flag = flag)
def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
def rm_tree(dir: Path): Unit = Isabelle_System.rm_tree(dir)
def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
--- a/src/Pure/ML/ml_process.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/ML/ml_process.scala Sat Jun 17 17:41:02 2023 +0200
@@ -77,13 +77,13 @@
// options
val eval_options = if (session_heaps.isEmpty) Nil else List("Options.load_default ()")
val isabelle_process_options = Isabelle_System.tmp_file("options")
- Isabelle_System.chmod("600", File.path(isabelle_process_options))
+ File.restrict(File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
// session resources
val eval_init_session = if (session_heaps.isEmpty) Nil else List("Resources.init_session_env ()")
val init_session = Isabelle_System.tmp_file("init_session")
- Isabelle_System.chmod("600", File.path(init_session))
+ File.restrict(File.path(init_session))
File.write(init_session, new Resources(session_background).init_session_yxml)
// process
--- a/src/Pure/System/host.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/System/host.scala Sat Jun 17 17:41:02 2023 +0200
@@ -96,6 +96,8 @@
/* SQL data model */
object Data {
+ val database: Path = Path.explode("$ISABELLE_HOME_USER/host.db")
+
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
SQL.Table("isabelle_host" + if_proper(name, "_" + name), columns, body = body)
@@ -106,6 +108,8 @@
val table = make_table("node_info", List(hostname, numa_next))
}
+ val all_tables: SQL.Tables = SQL.Tables(Node_Info.table)
+
def read_numa_next(db: SQL.Database, hostname: String): Int =
db.execute_query_statementO[Int](
Node_Info.table.select(List(Node_Info.numa_next),
@@ -113,16 +117,38 @@
res => res.int(Node_Info.numa_next)
).getOrElse(0)
- def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
- if (read_numa_next(db, hostname) != numa_next) {
- db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
- db.execute_statement(Node_Info.table.insert(), body =
- { stmt =>
- stmt.string(1) = hostname
- stmt.int(2) = numa_next
- })
- true
+ def write_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Unit = {
+ db.execute_statement(Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)))
+ db.execute_statement(Node_Info.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = hostname
+ stmt.int(2) = numa_next
+ })
+ }
+ }
+
+ def next_numa_node(
+ db: SQL.Database,
+ hostname: String,
+ available_nodes: List[Int],
+ used_nodes: => Set[Int]
+ ): Option[Int] =
+ if (available_nodes.isEmpty) None
+ else {
+ val available = available_nodes.zipWithIndex
+ val used = used_nodes
+ db.transaction_lock(Data.all_tables, create = true) {
+ val numa_next = Data.read_numa_next(db, hostname)
+ val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0)
+ val candidates = available.drop(numa_index) ::: available.take(numa_index)
+ val (n, i) =
+ candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
+ candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
+
+ val numa_next1 = available_nodes((i + 1) % available_nodes.length)
+ if (numa_next != numa_next1) Data.write_numa_next(db, hostname, numa_next1)
+
+ Some(n)
}
- else false
- }
+ }
}
--- a/src/Pure/System/progress.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/System/progress.scala Sat Jun 17 17:41:02 2023 +0200
@@ -10,8 +10,12 @@
import java.util.{Map => JMap}
import java.io.{File => JFile}
+import scala.collection.immutable.SortedMap
+
object Progress {
+ /* messages */
+
object Kind extends Enumeration { val writeln, warning, error_message = Value }
sealed case class Message(kind: Kind.Value, text: String, verbose: Boolean = false) {
def output_text: String =
@@ -33,6 +37,131 @@
def print_percentage: String =
percentage match { case None => "" case Some(p) => " " + p + "%" }
}
+
+
+ /* SQL data model */
+
+ object Data {
+ val database: Path = Path.explode("$ISABELLE_HOME_USER/progress.db")
+
+ def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
+ SQL.Table("isabelle_progress" + if_proper(name, "_" + name), columns, body = body)
+
+ object Base {
+ val context_uuid = SQL.Column.string("context_uuid").make_primary_key
+ val context = SQL.Column.long("context").make_primary_key
+ val stopped = SQL.Column.bool("stopped")
+
+ val table = make_table("", List(context_uuid, context, stopped))
+ }
+
+ object Agents {
+ val agent_uuid = SQL.Column.string("agent_uuid").make_primary_key
+ val context_uuid = SQL.Column.string("context_uuid").make_primary_key
+ val hostname = SQL.Column.string("hostname")
+ val java_pid = SQL.Column.long("java_pid")
+ val java_start = SQL.Column.date("java_start")
+ val start = SQL.Column.date("start")
+ val stamp = SQL.Column.date("stamp")
+ val stop = SQL.Column.date("stop")
+ val seen = SQL.Column.long("seen")
+
+ val table = make_table("agents",
+ List(agent_uuid, context_uuid, hostname, java_pid, java_start, start, stamp, stop, seen))
+ }
+
+ object Messages {
+ type T = SortedMap[Long, Message]
+ val empty: T = SortedMap.empty
+
+ val context = SQL.Column.long("context").make_primary_key
+ val serial = SQL.Column.long("serial").make_primary_key
+ val kind = SQL.Column.int("kind")
+ val text = SQL.Column.string("text")
+ val verbose = SQL.Column.bool("verbose")
+
+ val table = make_table("messages", List(context, serial, kind, text, verbose))
+ }
+
+ val all_tables: SQL.Tables = SQL.Tables(Base.table, Agents.table, Messages.table)
+
+ def read_progress_context(db: SQL.Database, context_uuid: String): Option[Long] =
+ db.execute_query_statementO(
+ Base.table.select(List(Base.context),
+ sql = Base.context_uuid.where_equal(context_uuid)), _.long(Base.context))
+
+ def next_progress_context(db: SQL.Database): Long =
+ db.execute_query_statementO(
+ Base.table.select(List(Base.context.max)), _.long(Base.context)).getOrElse(0L) + 1L
+
+ def read_progress_stopped(db: SQL.Database, context: Long): Boolean =
+ db.execute_query_statementO(
+ Base.table.select(List(Base.stopped), sql = Base.context.where_equal(context)),
+ _.bool(Base.stopped)
+ ).getOrElse(false)
+
+ def write_progress_stopped(db: SQL.Database, context: Long, stopped: Boolean): Unit =
+ db.execute_statement(
+ Base.table.update(List(Base.stopped), sql = Base.context.where_equal(context)),
+ body = { stmt => stmt.bool(1) = stopped })
+
+ def update_agent(
+ db: SQL.Database,
+ agent_uuid: String,
+ seen: Long,
+ stop: Boolean = false
+ ): Unit = {
+ val sql =
+ Agents.table.update(List(Agents.stamp, Agents.stop, Agents.seen),
+ sql = Agents.agent_uuid.where_equal(agent_uuid))
+ db.execute_statement(sql, body = { stmt =>
+ val now = db.now()
+ stmt.date(1) = now
+ stmt.date(2) = if (stop) Some(now) else None
+ stmt.long(3) = seen
+ })
+ }
+
+ def next_messages_serial(db: SQL.Database, context: Long): Long =
+ db.execute_query_statementO(
+ Messages.table.select(
+ List(Messages.serial.max), sql = Base.context.where_equal(context)),
+ _.long(Messages.serial)
+ ).getOrElse(0L) + 1L
+
+ def read_messages(db: SQL.Database, context: Long, seen: Long = 0): Messages.T =
+ db.execute_query_statement(
+ Messages.table.select(
+ List(Messages.serial, Messages.kind, Messages.text, Messages.verbose),
+ sql =
+ SQL.where_and(
+ Messages.context.ident + " = " + context,
+ if (seen <= 0) "" else Messages.serial.ident + " > " + seen)),
+ SortedMap.from[Long, Message],
+ { res =>
+ val serial = res.long(Messages.serial)
+ val kind = Kind(res.int(Messages.kind))
+ val text = res.string(Messages.text)
+ val verbose = res.bool(Messages.verbose)
+ serial -> Message(kind, text, verbose = verbose)
+ }
+ )
+
+ def write_messages(
+ db: SQL.Database,
+ context: Long,
+ serial: Long,
+ message: Message
+ ): Unit = {
+ db.execute_statement(Messages.table.insert(), body = { stmt =>
+ stmt.long(1) = context
+ stmt.long(2) = serial
+ stmt.int(3) = message.kind.id
+ stmt.string(4) = message.text
+ stmt.bool(5) = message.verbose
+ })
+ }
+ }
}
class Progress {
@@ -107,6 +236,123 @@
}
+/* database progress */
+
+class Database_Progress(
+ val db: SQL.Database,
+ val base_progress: Progress,
+ val hostname: String = Isabelle_System.hostname(),
+ val context_uuid: String = UUID.random().toString)
+extends Progress {
+ database_progress =>
+
+ private var _agent_uuid: String = ""
+ private var _context: Long = 0
+ private var _seen: Long = 0
+
+ def agent_uuid: String = synchronized { _agent_uuid }
+
+ private def transaction_lock[A](body: => A, create: Boolean = false): A =
+ db.transaction_lock(Progress.Data.all_tables, create = create)(body)
+
+ private def init(): Unit = synchronized {
+ transaction_lock(create = true, body = {
+ Progress.Data.read_progress_context(db, context_uuid) match {
+ case Some(context) =>
+ _context = context
+ _agent_uuid = UUID.random().toString
+ case None =>
+ _context = Progress.Data.next_progress_context(db)
+ _agent_uuid = context_uuid
+ db.execute_statement(Progress.Data.Base.table.insert(), { stmt =>
+ stmt.string(1) = context_uuid
+ stmt.long(2) = _context
+ stmt.bool(3) = false
+ })
+ }
+ db.execute_statement(Progress.Data.Agents.table.insert(), { stmt =>
+ val java = ProcessHandle.current()
+ val java_pid = java.pid
+ val java_start = Date.instant(java.info.startInstant.get)
+ val now = db.now()
+
+ stmt.string(1) = _agent_uuid
+ stmt.string(2) = context_uuid
+ stmt.string(3) = hostname
+ stmt.long(4) = java_pid
+ stmt.date(5) = java_start
+ stmt.date(6) = now
+ stmt.date(7) = now
+ stmt.date(8) = None
+ stmt.long(9) = 0L
+ })
+ })
+ if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.all_tables)
+ }
+
+ def exit(): Unit = synchronized {
+ if (_context > 0) {
+ transaction_lock {
+ Progress.Data.update_agent(db, _agent_uuid, _seen, stop = true)
+ }
+ _context = 0
+ }
+ }
+
+ private def sync_database[A](body: => A): A = synchronized {
+ require(_context > 0)
+ transaction_lock {
+ val stopped_db = Progress.Data.read_progress_stopped(db, _context)
+ val stopped = base_progress.stopped
+
+ if (stopped_db && !stopped) base_progress.stop()
+ if (stopped && !stopped_db) Progress.Data.write_progress_stopped(db, _context, true)
+
+ val messages = Progress.Data.read_messages(db, _context, seen = _seen)
+ for ((seen, message) <- messages) {
+ if (base_progress.do_output(message)) base_progress.output(message)
+ _seen = _seen max seen
+ }
+ if (messages.nonEmpty) Progress.Data.update_agent(db, _agent_uuid, _seen)
+
+ body
+ }
+ }
+
+ def sync(): Unit = sync_database {}
+
+ private def output_database(message: Progress.Message, body: => Unit): Unit =
+ sync_database {
+ val serial = Progress.Data.next_messages_serial(db, _context)
+ Progress.Data.write_messages(db, _context, serial, message)
+
+ body
+
+ _seen = _seen max serial
+ Progress.Data.update_agent(db, _agent_uuid, _seen)
+ }
+
+ override def output(message: Progress.Message): Unit =
+ output_database(message, if (do_output(message)) base_progress.output(message))
+
+ override def theory(theory: Progress.Theory): Unit =
+ output_database(theory.message, base_progress.theory(theory))
+
+ override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
+ base_progress.nodes_status(nodes_status)
+
+ override def verbose: Boolean = base_progress.verbose
+
+ override def stop(): Unit = synchronized { base_progress.stop(); sync() }
+ override def stopped: Boolean = sync_database { base_progress.stopped }
+
+ override def toString: String = super.toString + ": database " + db
+
+ init()
+ sync()
+}
+
+
/* structured program progress */
object Program_Progress {
--- a/src/Pure/Thy/document_build.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Thy/document_build.scala Sat Jun 17 17:41:02 2023 +0200
@@ -64,10 +64,9 @@
val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- SQL.where(
- SQL.and(
- Data.session_name.equal(session_name),
- if_proper(name, Data.name.equal(name))))
+ SQL.where_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] =
--- a/src/Pure/Thy/export.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Thy/export.scala Sat Jun 17 17:41:02 2023 +0200
@@ -44,11 +44,10 @@
val tables = SQL.Tables(table)
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
- 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))))
+ SQL.where_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 =
@@ -252,7 +251,7 @@
/* context for database access */
def open_database_context(store: Sessions.Store): Database_Context = {
- val database_server = if (store.database_server) Some(store.open_database_server()) else None
+ val database_server = if (store.build_database_server) Some(store.open_database_server()) else None
new Database_Context(store, database_server)
}
@@ -535,7 +534,7 @@
Isabelle_System.make_directory(path.dir)
val bytes = entry.bytes
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
- File.set_executable(path, entry.executable)
+ File.set_executable(path, flag = entry.executable)
}
}
}
--- a/src/Pure/Thy/sessions.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Thy/sessions.scala Sat Jun 17 17:41:02 2023 +0200
@@ -119,10 +119,9 @@
SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
def where_equal(session_name: String, name: String = ""): SQL.Source =
- SQL.where(
- SQL.and(
- Sources.session_name.equal(session_name),
- if_proper(name, Sources.name.equal(name))))
+ SQL.where_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(
@@ -1496,7 +1495,8 @@
def find_database(name: String): Option[Path] =
input_dirs.map(_ + database(name)).find(_.is_file)
- def database_server: Boolean = options.bool("build_database_server")
+ def build_database_server: Boolean = options.bool("build_database_server")
+ def build_database_test: Boolean = options.bool("build_database_test")
def open_database_server(): PostgreSQL.Database =
PostgreSQL.open_database(
@@ -1513,22 +1513,17 @@
port = options.int("build_database_ssh_port"))),
ssh_close = true)
- val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+ def open_build_database(path: Path): SQL.Database =
+ if (build_database_server) open_database_server()
+ else SQLite.open_database(path, restrict = true)
- def open_build_database(): Option[SQL.Database] =
- if (!options.bool("build_database_test")) None
- else if (database_server) Some(open_database_server())
- else {
- val db = SQLite.open_database(build_database)
- try { Isabelle_System.chmod("600", build_database) }
- catch { case exn: Throwable => db.close(); throw exn }
- Some(db)
- }
+ def maybe_open_build_database(path: Path): Option[SQL.Database] =
+ if (!build_database_test) None else Some(open_build_database(path))
def try_open_database(
name: String,
output: Boolean = false,
- server: Boolean = database_server
+ server: Boolean = build_database_server
): Option[SQL.Database] = {
def check(db: SQL.Database): Option[SQL.Database] =
if (output || session_info_exists(db)) Some(db) else { db.close(); None }
@@ -1554,7 +1549,7 @@
def clean_output(name: String): Option[Boolean] = {
val relevant_db =
- database_server &&
+ build_database_server &&
using_option(try_open_database(name))(init_session_info(_, name)).getOrElse(false)
val del =
@@ -1619,10 +1614,8 @@
val all_tables: SQL.Tables =
SQL.Tables(Session_Info.table, Sources.table, Export.Data.table, Document_Build.Data.table)
- def init_session_info(db: SQL.Database, name: String): Boolean = {
- db.transaction {
- all_tables.create_lock(db)
-
+ def init_session_info(db: SQL.Database, name: String): Boolean =
+ db.transaction_lock(all_tables, create = true) {
val already_defined = session_info_defined(db, name)
db.execute_statement(
@@ -1639,7 +1632,6 @@
already_defined
}
- }
def session_info_exists(db: SQL.Database): Boolean = {
val tables = db.tables
--- a/src/Pure/Tools/build_process.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Tools/build_process.scala Sat Jun 17 17:41:02 2023 +0200
@@ -122,12 +122,11 @@
}
def prepare_database(): Unit = {
- using_option(store.open_build_database()) { db =>
+ using_option(store.maybe_open_build_database(Data.database)) { db =>
val shared_db = db.is_postgresql
- db.transaction {
- Data.all_tables.create_lock(db)
+ db.transaction_lock(Data.all_tables, create = true) {
Data.clean_build(db)
- if (shared_db) store.all_tables.create_lock(db)
+ if (shared_db) store.all_tables.lock(db, create = true)
}
db.vacuum(Data.all_tables ::: (if (shared_db) store.all_tables else SQL.Tables.empty))
}
@@ -144,24 +143,17 @@
/** dynamic state **/
- type Progress_Messages = SortedMap[Long, Progress.Message]
- val progress_messages_empty: Progress_Messages = SortedMap.empty
-
case class Build(
- build_uuid: String,
+ build_uuid: String, // Database_Progress.context_uuid
ml_platform: String,
options: String,
start: Date,
- stop: Option[Date],
- progress_stopped: Boolean
+ stop: Option[Date]
)
case class Worker(
- worker_uuid: String,
+ worker_uuid: String, // Database_Progress.agent_uuid
build_uuid: String,
- hostname: String,
- java_pid: Long,
- java_start: Date,
start: Date,
stamp: Date,
stop: Option[Date],
@@ -202,7 +194,6 @@
}
sealed case class Snapshot(
- progress_messages: Progress_Messages,
builds: List[Build], // available build configurations
workers: List[Worker], // available worker processes
sessions: State.Sessions, // static build targets
@@ -224,8 +215,6 @@
sealed case class State(
serial: Long = 0,
- progress_seen: Long = 0,
- numa_next: Int = 0,
sessions: State.Sessions = Map.empty,
pending: State.Pending = Nil,
running: State.Running = Map.empty,
@@ -238,26 +227,6 @@
copy(serial = i)
}
- def progress_serial(message_serial: Long = serial): State =
- if (message_serial > progress_seen) copy(progress_seen = message_serial)
- else error("Bad serial " + message_serial + " for progress output (already seen)")
-
- def next_numa_node(numa_nodes: List[Int]): (Option[Int], State) =
- if (numa_nodes.isEmpty) (None, this)
- else {
- val available = numa_nodes.zipWithIndex
- val used =
- Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i)
-
- val numa_index = available.collectFirst({ case (n, i) if n == numa_next => i }).getOrElse(0)
- val candidates = available.drop(numa_index) ::: available.take(numa_index)
- val (n, i) =
- candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
- candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
-
- (Some(n), copy(numa_next = numa_nodes((i + 1) % numa_nodes.length)))
- }
-
def finished: Boolean = pending.isEmpty
def remove_pending(name: String): State =
@@ -299,6 +268,8 @@
/** SQL data model **/
object Data {
+ val database: Path = 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)
@@ -361,10 +332,8 @@
val options = SQL.Column.string("options")
val start = SQL.Column.date("start")
val stop = SQL.Column.date("stop")
- val progress_stopped = SQL.Column.bool("progress_stopped")
- val table =
- make_table("", List(build_uuid, ml_platform, options, start, stop, progress_stopped))
+ val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
}
def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] =
@@ -377,16 +346,14 @@
val options = res.string(Base.options)
val start = res.date(Base.start)
val stop = res.get_date(Base.stop)
- val progress_stopped = res.bool(Base.progress_stopped)
- Build(build_uuid, ml_platform, options, start, stop, progress_stopped)
+ Build(build_uuid, ml_platform, options, start, stop)
})
def start_build(
db: SQL.Database,
build_uuid: String,
ml_platform: String,
- options: String,
- progress_stopped: Boolean
+ options: String
): Unit = {
db.execute_statement(Base.table.insert(), body =
{ stmt =>
@@ -395,7 +362,6 @@
stmt.string(3) = options
stmt.date(4) = db.now()
stmt.date(5) = None
- stmt.bool(6) = progress_stopped
})
}
@@ -483,106 +449,22 @@
}
- /* progress */
-
- object Progress {
- val serial = SQL.Column.long("serial").make_primary_key
- val kind = SQL.Column.int("kind")
- val text = SQL.Column.string("text")
- val verbose = SQL.Column.bool("verbose")
- val build_uuid = Generic.build_uuid
-
- val table = make_table("progress", List(serial, kind, text, verbose, build_uuid))
- }
-
- def read_progress(db: SQL.Database, seen: Long = 0, build_uuid: String = ""): Progress_Messages =
- db.execute_query_statement(
- Progress.table.select(
- sql =
- SQL.where(
- SQL.and(
- if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
- Generic.sql(build_uuid = build_uuid)))),
- SortedMap.from[Long, isabelle.Progress.Message],
- { res =>
- val serial = res.long(Progress.serial)
- val kind = isabelle.Progress.Kind(res.int(Progress.kind))
- val text = res.string(Progress.text)
- val verbose = res.bool(Progress.verbose)
- serial -> isabelle.Progress.Message(kind, text, verbose = verbose)
- }
- )
-
- def write_progress(
- db: SQL.Database,
- message_serial: Long,
- message: isabelle.Progress.Message,
- build_uuid: String
- ): Unit = {
- db.execute_statement(Progress.table.insert(), body =
- { stmt =>
- stmt.long(1) = message_serial
- stmt.int(2) = message.kind.id
- stmt.string(3) = message.text
- stmt.bool(4) = message.verbose
- stmt.string(5) = build_uuid
- })
- }
-
- def sync_progress(
- db: SQL.Database,
- seen: Long,
- build_uuid: String,
- build_progress: Progress
- ): (Progress_Messages, Boolean) = {
- require(build_uuid.nonEmpty)
-
- val messages = read_progress(db, seen = seen, build_uuid = build_uuid)
-
- val stopped_db =
- db.execute_query_statementO[Boolean](
- Base.table.select(List(Base.progress_stopped),
- sql = SQL.where(Base.build_uuid.equal(build_uuid))),
- res => res.bool(Base.progress_stopped)
- ).getOrElse(false)
-
- def stop_db(): Unit =
- db.execute_statement(
- Base.table.update(
- List(Base.progress_stopped), sql = Base.build_uuid.where_equal(build_uuid)),
- body = { stmt => stmt.bool(1) = true })
-
- val stopped = build_progress.stopped
-
- if (stopped_db && !stopped) build_progress.stop()
- if (stopped && !stopped_db) stop_db()
-
- (messages, messages.isEmpty && stopped_db == stopped)
- }
-
-
/* workers */
object Workers {
val worker_uuid = Generic.worker_uuid.make_primary_key
val build_uuid = Generic.build_uuid
- val hostname = SQL.Column.string("hostname")
- val java_pid = SQL.Column.long("java_pid")
- val java_start = SQL.Column.date("java_start")
val start = SQL.Column.date("start")
val stamp = SQL.Column.date("stamp")
val stop = SQL.Column.date("stop")
val serial = SQL.Column.long("serial")
- val table = make_table("workers",
- List(worker_uuid, build_uuid, hostname, java_pid, java_start, start, stamp, stop, serial))
-
- val serial_max = serial.copy(expr = "MAX(" + serial.ident + ")")
+ val table = make_table("workers", List(worker_uuid, build_uuid, start, stamp, stop, serial))
}
def read_serial(db: SQL.Database): Long =
db.execute_query_statementO[Long](
- Workers.table.select(List(Workers.serial_max)), _.long(Workers.serial)).getOrElse(0L)
+ Workers.table.select(List(Workers.serial.max)), _.long(Workers.serial)).getOrElse(0L)
def read_workers(
db: SQL.Database,
@@ -597,9 +479,6 @@
Worker(
worker_uuid = res.string(Workers.worker_uuid),
build_uuid = res.string(Workers.build_uuid),
- hostname = res.string(Workers.hostname),
- java_pid = res.long(Workers.java_pid),
- java_start = res.date(Workers.java_start),
start = res.date(Workers.start),
stamp = res.date(Workers.stamp),
stop = res.get_date(Workers.stop),
@@ -611,9 +490,6 @@
db: SQL.Database,
worker_uuid: String,
build_uuid: String,
- hostname: String,
- java_pid: Long,
- java_start: Date,
serial: Long
): Unit = {
def err(msg: String): Nothing =
@@ -635,13 +511,10 @@
val now = db.now()
stmt.string(1) = worker_uuid
stmt.string(2) = build_uuid
- stmt.string(3) = hostname
- stmt.long(4) = java_pid
- stmt.date(5) = java_start
- stmt.date(6) = now
- stmt.date(7) = now
- stmt.date(8) = None
- stmt.long(9) = serial
+ stmt.date(3) = now
+ stmt.date(4) = now
+ stmt.date(5) = None
+ stmt.long(6) = serial
})
}
@@ -858,12 +731,10 @@
SQL.Tables(
Base.table,
Workers.table,
- Progress.table,
Sessions.table,
Pending.table,
Running.table,
- Results.table,
- Host.Data.Node_Info.table)
+ Results.table)
val build_uuid_tables =
all_tables.filter(table =>
@@ -881,14 +752,13 @@
val serial = serial_db max state.serial
stamp_worker(db, worker_uuid, serial)
- val numa_next = Host.Data.read_numa_next(db, hostname)
val sessions = pull1(read_sessions_domain(db), read_sessions(db, _), state.sessions)
val pending = read_pending(db)
val running = pull0(read_running(db), state.running)
val results = pull1(read_results_domain(db), read_results(db, _), state.results)
- state.copy(serial = serial, numa_next = numa_next, sessions = sessions,
- pending = pending, running = running, results = results)
+ state.copy(serial = serial, sessions = sessions, pending = pending,
+ running = running, results = results)
}
}
@@ -904,8 +774,7 @@
update_sessions(db, state.sessions),
update_pending(db, state.pending),
update_running(db, state.running),
- update_results(db, state.results),
- Host.Data.update_numa_next(db, hostname, state.numa_next))
+ update_results(db, state.results))
val serial0 = state.serial
val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0
@@ -932,90 +801,61 @@
protected final val build_deps: Sessions.Deps = build_context.build_deps
protected final val hostname: String = build_context.hostname
protected final val build_uuid: String = build_context.build_uuid
- protected final val worker_uuid: String = UUID.random().toString
+
+
+ /* progress backed by database */
+
+ private val _database: Option[SQL.Database] =
+ store.maybe_open_build_database(Build_Process.Data.database)
+
+ private val _host_database: Option[SQL.Database] =
+ store.maybe_open_build_database(Host.Data.database)
- override def toString: String =
- "Build_Process(worker_uuid = " + quote(worker_uuid) + ", build_uuid = " + quote(build_uuid) +
- if_proper(build_context.master, ", master = true") + ")"
+ protected val (progress, worker_uuid) = synchronized {
+ _database match {
+ case None => (build_progress, UUID.random().toString)
+ case Some(db) =>
+ val progress_db = store.open_build_database(Progress.Data.database)
+ val progress =
+ new Database_Progress(progress_db, build_progress,
+ hostname = hostname,
+ context_uuid = build_uuid)
+ (progress, progress.agent_uuid)
+ }
+ }
+ protected val log: Logger = Logger.make_system_log(progress, build_options)
+
+ def close(): Unit = synchronized {
+ _database.foreach(_.close())
+ _host_database.foreach(_.close())
+ progress match {
+ case db_progress: Database_Progress =>
+ db_progress.exit()
+ db_progress.db.close()
+ case _ =>
+ }
+ }
/* global state: internal var vs. external database */
private var _state: Build_Process.State = Build_Process.State()
- private val _database: Option[SQL.Database] = store.open_build_database()
-
- def close(): Unit = synchronized { _database.foreach(_.close()) }
-
- protected def synchronized_database[A](body: => A): A =
- synchronized {
- _database match {
- case None => body
- case Some(db) =>
- def pull_database(): Unit = {
- _state = Build_Process.Data.pull_database(db, worker_uuid, hostname, _state)
- }
-
- def sync_database(): Unit = {
- _state =
- Build_Process.Data.update_database(db, worker_uuid, build_uuid, hostname, _state)
- }
-
- def attempt(): Either[A, Build_Process.Progress_Messages] = {
- val (messages, sync) =
- Build_Process.Data.sync_progress(
- db, _state.progress_seen, build_uuid, build_progress)
- if (sync) Left { pull_database(); val res = body; sync_database(); res }
- else Right(messages)
- }
-
- @tailrec def attempts(): A = {
- db.transaction_lock(Build_Process.Data.all_tables) { attempt() } match {
- case Left(res) => res
- case Right(messages) =>
- for ((message_serial, message) <- messages) {
- _state = _state.progress_serial(message_serial = message_serial)
- if (build_progress.do_output(message)) build_progress.output(message)
- }
- attempts()
- }
- }
- attempts()
- }
- }
-
-
- /* progress backed by database */
-
- private def progress_output(message: Progress.Message, build_progress_output: => Unit): Unit = {
- synchronized_database {
- _state = _state.inc_serial.progress_serial()
- for (db <- _database) {
- Build_Process.Data.write_progress(db, _state.serial, message, build_uuid)
- Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial)
- }
- build_progress_output
+ protected def synchronized_database[A](body: => A): A = synchronized {
+ _database match {
+ case None => body
+ case Some(db) =>
+ db.transaction_lock(Build_Process.Data.all_tables) {
+ progress.asInstanceOf[Database_Progress].sync()
+ _state = Build_Process.Data.pull_database(db, worker_uuid, hostname, _state)
+ val res = body
+ _state =
+ Build_Process.Data.update_database(db, worker_uuid, build_uuid, hostname, _state)
+ res
+ }
}
}
- protected object progress extends Progress {
- override def verbose: Boolean = build_progress.verbose
-
- override def output(message: Progress.Message): Unit =
- progress_output(message, if (do_output(message)) build_progress.output(message))
-
- override def theory(theory: Progress.Theory): Unit =
- progress_output(theory.message, build_progress.theory(theory))
-
- override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
- build_progress.nodes_status(nodes_status)
-
- override def stop(): Unit = build_progress.stop()
- override def stopped: Boolean = build_progress.stopped
- }
-
- protected val log: Logger = Logger.make_system_log(progress, build_options)
-
/* policy operations */
@@ -1086,7 +926,13 @@
.make_result(result_name, Process_Result.undefined, output_shasum)
}
else {
- val (numa_node, state1) = state.next_numa_node(build_context.numa_nodes)
+ def used_nodes: Set[Int] =
+ Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
+ val numa_node =
+ for {
+ db <- _host_database
+ n <- Host.next_numa_node(db, hostname, build_context.numa_nodes, used_nodes)
+ } yield n
val node_info = Host.Node_Info(hostname, numa_node)
progress.echo(
@@ -1101,7 +947,7 @@
val job = Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Some(build))
- state1.add_running(job)
+ state.add_running(job)
}
}
@@ -1114,7 +960,7 @@
protected final def start_build(): Unit = synchronized_database {
for (db <- _database) {
Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
- build_context.sessions_structure.session_prefs, progress.stopped)
+ build_context.sessions_structure.session_prefs)
}
}
@@ -1126,12 +972,8 @@
protected final def start_worker(): Unit = synchronized_database {
for (db <- _database) {
- val java = ProcessHandle.current()
- val java_pid = java.pid
- val java_start = Date.instant(java.info.startInstant.get)
_state = _state.inc_serial
- Build_Process.Data.start_worker(
- db, worker_uuid, build_uuid, hostname, java_pid, java_start, _state.serial)
+ Build_Process.Data.start_worker(db, worker_uuid, build_uuid, _state.serial)
}
}
@@ -1211,16 +1053,14 @@
/* snapshot */
def snapshot(): Build_Process.Snapshot = synchronized_database {
- val (progress_messages, builds, workers) =
+ val (builds, workers) =
_database match {
- case None => (Build_Process.progress_messages_empty, Nil, Nil)
+ case None => (Nil, Nil)
case Some(db) =>
- (Build_Process.Data.read_progress(db),
- Build_Process.Data.read_builds(db),
+ (Build_Process.Data.read_builds(db),
Build_Process.Data.read_workers(db))
}
Build_Process.Snapshot(
- progress_messages = progress_messages,
builds = builds,
workers = workers,
sessions = _state.sessions,
@@ -1228,4 +1068,11 @@
running = _state.running,
results = _state.results)
}
+
+
+ /* toString */
+
+ override def toString: String =
+ "Build_Process(worker_uuid = " + quote(worker_uuid) + ", build_uuid = " + quote(build_uuid) +
+ if_proper(build_context.master, ", master = true") + ")"
}
--- a/src/Pure/Tools/dotnet_setup.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Tools/dotnet_setup.scala Sat Jun 17 17:41:02 2023 +0200
@@ -136,7 +136,7 @@
progress.bash(script, echo = progress.verbose,
cwd = if (dry_run) null else component_dir.path.file).check
for (exe <- File.find_files(platform_dir.file, pred = _.getName.endsWith(".exe"))) {
- File.set_executable(File.path(exe), true)
+ File.set_executable(File.path(exe))
}
}
}
--- a/src/Pure/Tools/server.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Pure/Tools/server.scala Sat Jun 17 17:41:02 2023 +0200
@@ -397,10 +397,8 @@
existing_server: Boolean = false,
log: Logger = No_Logger
): (Info, Option[Server]) = {
- using(SQLite.open_database(Data.database)) { db =>
- db.transaction {
- Isabelle_System.chmod("600", Data.database)
- Data.tables.create_lock(db)
+ using(SQLite.open_database(Data.database, restrict = true)) { db =>
+ db.transaction_lock(Data.tables, create = true) {
list(db).filterNot(_.active).foreach(server_info =>
db.execute_statement(Data.table.delete(sql = Data.name.where_equal(server_info.name))))
}
@@ -429,7 +427,7 @@
}
def exit(name: String = default_name): Boolean = {
- using(SQLite.open_database(Data.database))(db =>
+ using(SQLite.open_database(Data.database)) { db =>
db.transaction_lock(Data.tables) {
find(db, name) match {
case Some(server_info) =>
@@ -438,7 +436,8 @@
true
case None => false
}
- })
+ }
+ }
}
--- a/src/Tools/VSCode/src/component_vscodium.scala Thu Jun 15 17:20:09 2023 +1000
+++ b/src/Tools/VSCode/src/component_vscodium.scala Sat Jun 17 17:41:02 2023 +0200
@@ -217,7 +217,7 @@
val name = file.getName
File.is_dll(name) || File.is_exe(name) || File.is_node(name)
})
- files.foreach(file => File.set_executable(File.path(file), true))
+ files.foreach(file => File.set_executable(File.path(file)))
Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check
}
}