--- a/src/Pure/Admin/component_e.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Admin/component_e.scala Fri Feb 16 15:55:06 2024 +0000
@@ -100,6 +100,7 @@
}
}
+
/* Isabelle tool wrapper */
val isabelle_tool =
--- a/src/Pure/Admin/component_hugo.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Admin/component_hugo.scala Fri Feb 16 15:55:06 2024 +0000
@@ -91,6 +91,9 @@
""" + Date.Format.date(Date.now()) + "\n")
}
+
+ /* Isabelle tool wrapper */
+
val isabelle_tool =
Isabelle_Tool("component_hugo", "build hugo component", Scala_Project.here,
{ args =>
--- a/src/Pure/Admin/component_spass.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Admin/component_spass.scala Fri Feb 16 15:55:06 2024 +0000
@@ -138,6 +138,7 @@
}
}
+
/* Isabelle tool wrapper */
val isabelle_tool =
--- a/src/Pure/Build/build.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Build/build.scala Fri Feb 16 15:55:06 2024 +0000
@@ -308,7 +308,7 @@
}
- /* command-line wrapper */
+ /* Isabelle tool wrappers */
val isabelle_tool1 = Isabelle_Tool("build", "build and manage Isabelle sessions",
Scala_Project.here,
@@ -585,7 +585,7 @@
verbose: Boolean = false
): String = {
val options = build_options ::: Options.Spec.eq("build_hostname", host.name) :: host.options
- ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_worker" +
+ ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_worker" +
if_proper(build_id, " -B " + Bash.string(build_id)) +
if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
@@ -861,7 +861,7 @@
}
- /* command-line wrapper */
+ /* Isabelle tool wrapper */
val isabelle_tool4 = Isabelle_Tool("build_log", "print messages from session build database",
Scala_Project.here,
--- a/src/Pure/Build/build_benchmark.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Build/build_benchmark.scala Fri Feb 16 15:55:06 2024 +0000
@@ -8,8 +8,10 @@
object Build_Benchmark {
- /* ZF-Constructible as representative benchmark session with short build time and requirements */
+ /* benchmark */
+ // ZF-Constructible as representative benchmark session with
+ // short build time and requirements
val benchmark_session = "ZF-Constructible"
def benchmark_command(
@@ -18,7 +20,7 @@
isabelle_home: Path = Path.current,
): String = {
val options = Options.Spec.eq("build_hostname", host.name) :: host.options
- ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_benchmark" +
+ ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_benchmark" +
Options.Spec.bash_strings(options, bg = true)
}
@@ -103,6 +105,9 @@
}
}
+
+ /* Isabelle tool wrapper */
+
val isabelle_tool = Isabelle_Tool("build_benchmark", "run benchmark for build process",
Scala_Project.here,
{ args =>
--- a/src/Pure/Build/build_cluster.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Build/build_cluster.scala Fri Feb 16 15:55:06 2024 +0000
@@ -101,7 +101,7 @@
}
def parse_single(registry: Registry, str: String): Host =
- Library.the_single(parse(registry, str), "Single host expected: " + quote(str))
+ Library.the_single(parse(registry, str), message = "Single host expected: " + quote(str))
}
class Host(
@@ -238,10 +238,10 @@
def return_code(rc: Int): Unit = ()
def return_code(res: Process_Result): Unit = return_code(res.rc)
def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn))
- def open(): Unit = ()
- def init(): Unit = ()
- def benchmark(): Unit = ()
- def start(): Unit = ()
+ def open(): Build_Cluster = this
+ def init(): Build_Cluster = this
+ def benchmark(): Build_Cluster = this
+ def start(): Build_Cluster = this
def active(): Boolean = false
def join: List[Build_Cluster.Result] = Nil
def stop(): Unit = { join; close() }
@@ -284,7 +284,7 @@
private var _sessions = List.empty[Build_Cluster.Session]
- override def open(): Unit = synchronized {
+ override def open(): Build_Cluster = synchronized {
require(_sessions.isEmpty, "build cluster already open")
val attempts =
@@ -300,6 +300,8 @@
for (case Exn.Res(session) <- attempts) session.close()
error("Failed to connect build cluster")
}
+
+ this
}
@@ -307,7 +309,7 @@
private var _init = List.empty[Future[Unit]]
- override def init(): Unit = synchronized {
+ override def init(): Build_Cluster = synchronized {
require(_sessions.nonEmpty, "build cluster not yet open")
if (_init.isEmpty) {
@@ -319,9 +321,11 @@
}
}
}
+
+ this
}
- override def benchmark(): Unit = synchronized {
+ override def benchmark(): Build_Cluster = synchronized {
_init.foreach(_.join)
_init =
for (session <- _sessions if !session.host.shared) yield {
@@ -330,6 +334,8 @@
}
}
_init.foreach(_.join)
+
+ this
}
@@ -339,7 +345,7 @@
override def active(): Boolean = synchronized { _workers.nonEmpty }
- override def start(): Unit = synchronized {
+ override def start(): Build_Cluster = synchronized {
require(_sessions.nonEmpty, "build cluster not yet open")
require(_workers.isEmpty, "build cluster already active")
@@ -352,6 +358,8 @@
Exn.release(capture(session.host, "work") { session.start() })
}
}
+
+ this
}
override def join: List[Build_Cluster.Result] = synchronized {
--- a/src/Pure/Build/build_process.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Build/build_process.scala Fri Feb 16 15:55:06 2024 +0000
@@ -914,11 +914,8 @@
protected val log: Logger = Logger.make_system_log(progress, build_options)
- protected def open_build_cluster(): Build_Cluster = {
- val build_cluster = Build_Cluster.make(build_context, progress = build_progress)
- build_cluster.open()
- build_cluster
- }
+ protected def open_build_cluster(): Build_Cluster =
+ Build_Cluster.make(build_context, progress = build_progress).open()
protected val _build_cluster =
try {
--- a/src/Pure/Build/build_schedule.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/Build/build_schedule.scala Fri Feb 16 15:55:06 2024 +0000
@@ -1314,11 +1314,7 @@
val hosts_current =
cluster_hosts.forall(host => isabelle.Host.read_info(host_database, host.name).isDefined)
if (!hosts_current) {
- val build_cluster = Build_Cluster.make(build_context, progress = progress)
- build_cluster.open()
- build_cluster.init()
- build_cluster.benchmark()
- build_cluster.close()
+ using(Build_Cluster.make(build_context, progress = progress).open())(_.init().benchmark())
}
val host_infos = Host_Infos.load(cluster_hosts, host_database)
@@ -1509,7 +1505,7 @@
}
- /* command-line wrapper */
+ /* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("build_schedule", "generate build schedule", Scala_Project.here,
{ args =>
--- a/src/Pure/System/isabelle_tool.scala Fri Feb 16 11:22:29 2024 +0000
+++ b/src/Pure/System/isabelle_tool.scala Fri Feb 16 15:55:06 2024 +0000
@@ -87,6 +87,8 @@
/* command line entry point */
+ def exe(isabelle_home: Path): Path = isabelle_home + Path.explode("bin/isabelle")
+
def main(args: Array[String]): Unit = {
Command_Line.tool {
args.toList match {