--- a/etc/options Wed Aug 06 10:01:05 2025 +0100
+++ b/etc/options Wed Aug 06 16:51:58 2025 +0200
@@ -494,9 +494,11 @@
section "Build Manager SSH"
option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection
+ -- "SSH host name for build manager"
option build_manager_ssh_port : int = 0 for connection
+ -- "explicit SSH port"
option build_manager_ssh_user : string = "" for connection
- -- "ssh user to access build manager system"
+ -- "explicit SSH user"
option build_manager_cluster_ssh_host : string = "localhost" for connection
option build_manager_cluster_ssh_user : string = "" for connection
--- a/src/Pure/Build/build_manager.scala Wed Aug 06 10:01:05 2025 +0100
+++ b/src/Pure/Build/build_manager.scala Wed Aug 06 16:51:58 2025 +0200
@@ -1942,6 +1942,9 @@
/* Isabelle tool wrapper */
+ private val build_manager_ssh_options =
+ List("build_manager_ssh_user", "build_manager_ssh_host", "build_manager_ssh_port")
+
val isabelle_tool2 = Isabelle_Tool("build_task", "submit build task for build manager",
Scala_Project.here,
{ args =>
@@ -1962,6 +1965,9 @@
var rev = ""
val exclude_sessions = new mutable.ListBuffer[String]
+ def show_options: String =
+ cat_lines(build_manager_ssh_options.flatMap(options.get).map(_.print))
+
val getopts = Getopts("""
Usage: isabelle build_task [OPTIONS] [SESSIONS ...]
@@ -1978,14 +1984,16 @@
-f fresh build
-g NAME select session group NAME
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -p OPTION override Isabelle system OPTION for build process (via NAME=VAL or NAME)
+ -p OPTION override Isabelle system OPTION for build process
+ (via NAME=VAL or NAME)
-r REV explicit revision (default: state of working directory)
-v verbose
-x NAME exclude session NAME and all descendants
- Submit build task on SSH server. Notable system options:
+ Submit build task on managed server.
-""" + Library.indent_lines(2, options.get("build_manager_ssh_user").get.print) + "\n",
+ Requires SSH access to known host according to system options:
+""" + Library.indent_lines(4, show_options) + "\n",
"A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
"B:" -> (arg => base_sessions += arg),
"P" -> (_ => presentation = true),