tuned doc: display build manager SSH options;
authorFabian Huch <huch@in.tum.de>
Wed, 06 Aug 2025 16:51:58 +0200
changeset 82915 b7422567c507
parent 82914 cbf3703f92ea
child 82961 6a69754cf371
tuned doc: display build manager SSH options;
etc/options
src/Pure/Build/build_manager.scala
--- 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),