build_manager: terminate processes if cancelling does not work;

--- a/etc/options	Tue Aug 06 13:54:10 2024 +0200
+++ b/etc/options	Tue Aug 06 15:00:37 2024 +0200
@@ -252,6 +252,9 @@
 option build_manager_timeout : real = 28800
   -- "timeout for user-submitted tasks (seconds > 0)"
 
+option build_manager_cancel_timeout : real = 180.0
+  -- "timeout for graceful cancelling (seconds > 0)"
+
 option build_manager_delay : real = 1.0
   -- "delay build manager loop"
 

--- a/src/Pure/Build/build_manager.scala	Tue Aug 06 13:54:10 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Aug 06 15:00:37 2024 +0200
@@ -753,13 +753,22 @@
 
   object Runner {
     object State {
-      def empty: State = new State(Map.empty, Map.empty)
+      def init(options: Options): State =
+        new State(Map.empty, Map.empty, Map.empty, options.seconds("build_manager_cancel_timeout"))
     }
 
     class State private(
       process_futures: Map[String, Future[Build_Process]],
-      result_futures: Map[String, Future[Process_Result]]
+      result_futures: Map[String, Future[Process_Result]],
+      cancelling_until: Map[String, Time],
+      cancel_timeout: Time
     ) {
+      private def copy(
+        process_futures: Map[String, Future[Build_Process]] = process_futures,
+        result_futures: Map[String, Future[Process_Result]] = result_futures,
+        cancelling_until: Map[String, Time] = cancelling_until,
+      ): State = new State(process_futures, result_futures, cancelling_until, cancel_timeout)
+
       def is_empty = process_futures.isEmpty && result_futures.isEmpty
 
       def init(context: Context): State = {
@@ -770,13 +779,21 @@
               case Exn.Res(process) => process.run()
               case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
-        new State(
+
+        copy(
           process_futures + (context.name -> process_future),
           result_futures + (context.name -> result_future))
       }
 
       def running: List[String] = process_futures.keys.toList
 
+      private def do_terminate(name: String): Boolean =
+        if (cancelling_until(name) <= Time.now()) true
+        else {
+          process_futures(name).join.terminate()
+          false
+        }
+
       def update: (State, Map[String, Process_Result]) = {
         val finished =
           for ((name, future) <- result_futures if future.is_finished)
@@ -786,21 +803,32 @@
               case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
 
-        val process_futures1 = process_futures.filterNot((name, _) => finished.contains(name))
-        val result_futures1 = result_futures.filterNot((name, _) => finished.contains(name))
-
-        (new State(process_futures1, result_futures1), finished)
+        val state1 =
+          copy(
+            process_futures.filterNot((name, _) => finished.contains(name)),
+            result_futures.filterNot((name, _) => finished.contains(name)),
+            cancelling_until.filterNot((name, _) => finished.contains(name) && !do_terminate(name)))
+        (state1, finished)
       }
 
-      def cancel(cancelled: List[String]): State = {
-        for (name <- cancelled) {
-          val process_future = process_futures(name)
-          if (process_future.is_finished) process_future.join.cancel()
-          else process_future.cancel()
+      private def do_cancel(name: String): Boolean = 
+        process_futures.get(name) match {
+          case Some(process_future) =>
+            if (process_future.is_finished) {
+              process_future.join.cancel()
+              true
+            } else {
+              process_future.cancel()
+              false
+            }
+          case None => false
         }
 
-        new State(process_futures.filterNot((name, _) => cancelled.contains(name)), result_futures)
-      }
+      def cancel(cancelled: List[String]): State =
+        copy(
+          process_futures.filterNot((name, _) => cancelled.contains(name)),
+          cancelling_until = cancelling_until ++
+            cancelled.filter(do_cancel).map(_ -> (Time.now() + cancel_timeout)))
     }
   }
 
@@ -966,7 +994,7 @@
 
     override def stopped(state: Runner.State): Boolean = progress.stopped && state.is_empty
 
-    def init: Runner.State = Runner.State.empty
+    def init: Runner.State = Runner.State.init(store.options)
     def loop_body(state: Runner.State): Runner.State = {
       val state1 =
         if (progress.stopped) state
@@ -1472,6 +1500,7 @@
       catch { case exn: Throwable => close(); throw exn }
 
     def cancel(): Unit = Option(_process).foreach(_.interrupt())
+    def terminate(): Unit = Option(_process).foreach(_.terminate())
 
     def close(): Unit = {
       Option(_dir).foreach(ssh.rm_tree)