support local build_heaps;
authorwenzelm
Thu, 06 May 2021 20:43:12 +0200
changeset 73890 c88faa1e09e1
parent 73889 7e465e166bb2
child 73891 3531d20cf2fd
support local build_heaps; more robust build_release;
src/Pure/Admin/build_release.scala
src/Pure/General/ssh.scala
--- a/src/Pure/Admin/build_release.scala	Wed May 05 21:14:38 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu May 06 20:43:12 2021 +0200
@@ -223,39 +223,45 @@
 
   /** build release **/
 
-  /* build heaps on remote server */
+  /* build heaps */
 
-  private def remote_build_heaps(
+  private def build_heaps(
     options: Options,
     platform: Platform.Family.Value,
     build_sessions: List[String],
     local_dir: Path): Unit =
   {
     val server_option = "build_host_" + platform.toString
-    options.string(server_option) match {
-      case SSH.Target(user, host) =>
-        using(SSH.open_session(options, host = host, user = user))(ssh =>
-          Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
-          {
-            execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
-            ssh.with_tmp_dir(remote_dir =>
-            {
-              val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
-              ssh.write_file(remote_tmp_tar, local_tmp_tar)
-              val remote_commands =
-                List(
-                  "cd " + File.bash_path(remote_dir),
-                  "tar -xf tmp.tar",
-                  "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
-                  "tar -cf tmp.tar heaps")
-              ssh.execute(remote_commands.mkString(" && ")).check
-              ssh.read_file(remote_tmp_tar, local_tmp_tar)
-            })
-            execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
-          })
-        )
-      case s => error("Bad " + server_option + ": " + quote(s))
+    val ssh =
+      options.string(server_option) match {
+        case "" =>
+          if (Platform.family == platform) SSH.Local
+          else error("Undefined option " + server_option + ": cannot build heaps")
+        case SSH.Target(user, host) =>
+          SSH.open_session(options, host = host, user = user)
+        case s => error("Malformed option " + server_option + ": " + quote(s))
+      }
+    try {
+      Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
+      {
+        execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
+        ssh.with_tmp_dir(remote_dir =>
+        {
+          val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
+          ssh.write_file(remote_tmp_tar, local_tmp_tar)
+          val remote_commands =
+            List(
+              "cd " + File.bash_path(remote_dir),
+              "tar -xf tmp.tar",
+              "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
+              "tar -cf tmp.tar heaps")
+          ssh.execute(remote_commands.mkString(" && "), settings = false).check
+          ssh.read_file(remote_tmp_tar, local_tmp_tar)
+        })
+        execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
+      })
     }
+    finally { ssh.close() }
   }
 
 
@@ -594,8 +600,8 @@
         // build heaps
 
         if (build_sessions.nonEmpty) {
-          progress.echo("Building heaps ...")
-          remote_build_heaps(options, platform, build_sessions, isabelle_target)
+          progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
+          build_heaps(options, platform, build_sessions, isabelle_target)
         }
 
 
@@ -901,11 +907,12 @@
       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
         error("Building for windows requires 7z")
 
+      val progress = new Console_Progress()
       def make_context(name: String): Release_Context =
         Release_Context(target_dir,
           release_name = name,
           components_base = components_base,
-          progress = new Console_Progress())
+          progress = progress)
 
       val context =
         if (source_archive.isEmpty) {
@@ -915,9 +922,10 @@
           context
         }
         else {
-          val archive = Release_Archive.get(source_archive, rename = release_name)
+          val archive =
+            Release_Archive.get(source_archive, rename = release_name, progress = progress)
           val context = make_context(archive.identifier)
-          Isabelle_System.new_directory(context.dist_dir)
+          Isabelle_System.make_directory(context.dist_dir)
           use_release_archive(context, archive, id = rev)
           context
         }
--- a/src/Pure/General/ssh.scala	Wed May 05 21:14:38 2021 +0200
+++ b/src/Pure/General/ssh.scala	Thu May 06 20:43:12 2021 +0200
@@ -318,7 +318,7 @@
     val session: JSch_Session,
     on_close: () => Unit,
     val nominal_host: String,
-    val nominal_user: String) extends System with AutoCloseable
+    val nominal_user: String) extends System
   {
     def update_options(new_options: Options): Session =
       new Session(new_options, session, on_close, nominal_host, nominal_user)
@@ -347,7 +347,7 @@
     val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp]
     sftp.connect(connect_timeout(options))
 
-    def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
+    override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() }
 
     val settings: Map[String, String] =
     {
@@ -438,12 +438,12 @@
     def open_input(path: Path): InputStream = sftp.get(remote_path(path))
     def open_output(path: Path): OutputStream = sftp.put(remote_path(path))
 
-    def read_file(path: Path, local_path: Path): Unit =
+    override def read_file(path: Path, local_path: Path): Unit =
       sftp.get(remote_path(path), File.platform_path(local_path))
     def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_))
     def read(path: Path): String = using(open_input(path))(File.read_stream)
 
-    def write_file(path: Path, local_path: Path): Unit =
+    override def write_file(path: Path, local_path: Path): Unit =
       sftp.put(File.platform_path(local_path), remote_path(path))
     def write_bytes(path: Path, bytes: Bytes): Unit =
       using(open_output(path))(bytes.write_stream)
@@ -463,6 +463,7 @@
     override def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
+        settings: Boolean = true,
         strict: Boolean = true): Process_Result =
       exec(command).result(progress_stdout, progress_stderr, strict)
 
@@ -479,7 +480,7 @@
     def tmp_dir(): String =
       execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
 
-    def with_tmp_dir[A](body: Path => A): A =
+    override def with_tmp_dir[A](body: Path => A): A =
     {
       val remote_dir = tmp_dir()
       try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) }
@@ -489,8 +490,10 @@
 
   /* system operations */
 
-  trait System
+  trait System extends AutoCloseable
   {
+    def close(): Unit = ()
+
     def hg_url: String = ""
 
     def expand_path(path: Path): Path = path.expand
@@ -498,13 +501,20 @@
     def is_dir(path: Path): Boolean = path.is_dir
     def is_file(path: Path): Boolean = path.is_file
     def make_directory(path: Path): Path = Isabelle_System.make_directory(path)
+    def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body)
+    def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2)
+    def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1)
 
     def execute(command: String,
         progress_stdout: String => Unit = (_: String) => (),
         progress_stderr: String => Unit = (_: String) => (),
+        settings: Boolean = true,
         strict: Boolean = true): Process_Result =
-      Isabelle_System.bash(command, progress_stdout = progress_stdout,
-        progress_stderr = progress_stderr, strict = strict)
+      Isabelle_System.bash(command,
+        progress_stdout = progress_stdout,
+        progress_stderr = progress_stderr,
+        env = if (settings) Isabelle_System.settings() else null,
+        strict = strict)
 
     def isabelle_platform: Isabelle_Platform = Isabelle_Platform()
   }