# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717761659 -7200
# Node ID 02424b81472a08923d1243d560753ce745873102
# Parent  21b30f1fa3315485f5bf984703078cc5e67fd947
clarified: add explicit build process;

diff -r 21b30f1fa331 -r 02424b81472a src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 07 13:54:00 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 07 14:00:59 2024 +0200
@@ -567,17 +567,17 @@
     }
 
     class State private(
-      process_futures: Map[String, Future[Bash.Process]],
+      process_futures: Map[String, Future[Build_Process]],
       result_futures: Map[String, Future[Process_Result]]
     ) {
       def is_empty = process_futures.isEmpty && result_futures.isEmpty
 
       def init(build_config: Build_Config, job: Job, context: Context): State = {
-        val process_future = Future.fork(context.process(build_config))
+        val process_future = Future.fork(Build_Process.open(build_config, context))
         val result_future =
           Future.fork(
             process_future.join_result match {
-              case Exn.Res(process) => context.run(process)
+              case Exn.Res(process) => process.run()
               case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt)
             })
         new State(
@@ -600,7 +600,7 @@
       def cancel(cancelled: List[String]): State = {
         for (name <- cancelled) {
           val process_future = process_futures(name)
-          if (process_future.is_finished) process_future.join.interrupt()
+          if (process_future.is_finished) process_future.join.cancel()
           else process_future.cancel()
         }
 
@@ -1074,6 +1074,8 @@
   }
 
   class Context private(store: Store, val dir: Path, val build_hosts: List[Build_Cluster.Host]) {
+    def isabelle_identifier: String = store.identifier
+
     private val log_file = dir + Path.basic("log")
     val progress = new File_Progress(log_file, verbose = true)
     def log: String =
@@ -1096,33 +1098,65 @@
 
     def remove(): Unit = Isabelle_System.rm_tree(dir)
 
-    lazy val ssh = store.open_ssh()
+    def ssh = store.open_ssh()
+  }
+
+
+  /* build process */
+
+  object Build_Process {
+    def open(build_config: Build_Config, context: Context): Build_Process =
+      new Build_Process(context.ssh, build_config, context)
+  }
 
-    def process(build_config: Build_Config): Bash.Process = {
-      val isabelle = Other_Isabelle(dir, store.identifier, ssh, progress)
+  class Build_Process(ssh: SSH.Session, build_config: Build_Config, context: Context) {
+    private val _dir = ssh.tmp_dir()
+    private val _progress = context.progress
+
+    private val _isabelle =
+      try {
+        val rsync_context = Rsync.Context(ssh = ssh)
+        val source = File.standard_path(context.dir)
+        Rsync.exec(rsync_context, clean = true, args = List("--", Url.direct_path(source),
+          rsync_context.target(_dir))).check
+
+        Other_Isabelle(_dir, context.isabelle_identifier, ssh, _progress)
+      }
+      catch { case exn: Throwable => close(); throw exn }
 
-      val init_components =
-        for {
-          component <- build_config.components
-          target = dir + Sync.DIRS + Path.basic(component.name)
-          if Components.is_component_dir(target)
-        } yield "init_component " + quote(target.absolute.implode)
+    private val _process =
+      try {
+        val init_components =
+          for {
+            component <- build_config.components
+            target = _dir + Sync.DIRS + Path.basic(component.name)
+            if Components.is_component_dir(target)
+          } yield "init_component " + quote(target.absolute.implode)
+
+        _isabelle.init(
+          other_settings = _isabelle.init_components() ::: init_components,
+          fresh = build_config.fresh_build, echo = true)
 
-      isabelle.init(other_settings = isabelle.init_components() ::: init_components,
-        fresh = build_config.fresh_build, echo = true)
+        val cmd = build_config.command(context.build_hosts)
+        _progress.echo("isabelle" + cmd)
 
-      val cmd = build_config.command(build_hosts)
-      progress.echo("isabelle" + cmd)
+        val script = File.bash_path(Isabelle_Tool.exe(_isabelle.isabelle_home)) + cmd
+        ssh.bash_process(_isabelle.bash_context(script), settings = false)
+      }
+      catch { case exn: Throwable => close(); throw exn }
 
-      val script = File.bash_path(Isabelle_Tool.exe(isabelle.isabelle_home)) + cmd
-      ssh.bash_process(isabelle.bash_context(script), settings = false)
+    def run(): Process_Result = {
+      val process_result =
+        _process.result(progress_stdout = _progress.echo(_), progress_stderr = _progress.echo(_))
+      close()
+      process_result
     }
 
-    def run(process: Bash.Process): Process_Result = {
-      val process_result =
-        process.result(progress_stdout = progress.echo(_), progress_stderr = progress.echo(_))
+    def cancel(): Unit = Option(_process).foreach(_.interrupt())
+
+    def close(): Unit = {
+      Option(_dir).foreach(ssh.rm_tree)
       ssh.close()
-      process_result
     }
   }