more robust: first register job, then start job;

--- a/src/Pure/Tools/build_job.scala	Mon Feb 13 11:53:35 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Mon Feb 13 12:00:21 2023 +0100
@@ -251,7 +251,7 @@
   val session_sources: Sessions.Sources =
     Sessions.Sources.load(session_background.base, cache = store.cache.compress)
 
-  private val future_result: Future[Process_Result] =
+  private lazy val future_result: Future[Process_Result] =
     Future.thread("build", uninterruptible = true) {
       val parent = info.parent.getOrElse("")
 
@@ -559,6 +559,7 @@
       }
     }
 
+  def start(): Unit = future_result
   def terminate(): Unit = future_result.cancel()
   def is_finished: Boolean = future_result.is_finished
 

--- a/src/Pure/Tools/build_process.scala	Mon Feb 13 11:53:35 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 12:00:21 2023 +0100
@@ -317,13 +317,16 @@
         new Resources(session_background, log = log,
           command_timings = build_context(session_name).old_command_timings)
 
-      synchronized {
-        val numa_node = next_numa_node()
-        val job =
-          new Build_Job(progress, session_background, store, do_store,
-            resources, session_setup, input_heaps, numa_node)
-        _running += (session_name -> job)
-      }
+      val job =
+        synchronized {
+          val numa_node = next_numa_node()
+          val job =
+            new Build_Job(progress, session_background, store, do_store,
+              resources, session_setup, input_heaps, numa_node)
+          _running += (session_name -> job)
+          job
+        }
+      job.start()
     }
     else {
       progress.echo(session_name + " CANCELLED")