src/Pure/System/bash.scala
author wenzelm
Thu, 22 Apr 2021 23:40:22 +0200
changeset 73858 37243ad3ecb6
parent 73857 19c558ea903c
child 73859 342362c9496c
permissions -rw-r--r--
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62584
6cd36a0d2a28 clarified files;
wenzelm
parents: 62574
diff changeset
     1
/*  Title:      Pure/System/bash.scala
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     3
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     4
GNU bash processes, with propagation of interrupts.
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     5
*/
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     6
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     7
package isabelle
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     8
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     9
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile, BufferedReader, InputStreamReader,
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    11
  BufferedWriter, OutputStreamWriter}
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    12
71922
wenzelm
parents: 71921
diff changeset
    13
import scala.annotation.tailrec
73858
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
    14
import scala.jdk.OptionConverters._
71922
wenzelm
parents: 71921
diff changeset
    15
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    16
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    17
object Bash
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    18
{
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    19
  /* concrete syntax */
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    20
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    21
  private def bash_chr(c: Byte): String =
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    22
  {
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    23
    val ch = c.toChar
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    24
    ch match {
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    25
      case '\t' => "$'\\t'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    26
      case '\n' => "$'\\n'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    27
      case '\f' => "$'\\f'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    28
      case '\r' => "$'\\r'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    29
      case _ =>
67200
wenzelm
parents: 65317
diff changeset
    30
        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    31
          Symbol.ascii(ch)
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    32
        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    33
        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    34
        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    35
        else  "\\" + ch
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    36
    }
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    37
  }
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    38
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    39
  def string(s: String): String =
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    40
    if (s == "") "\"\""
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 67200
diff changeset
    41
    else UTF8.bytes(s).iterator.map(bash_chr).mkString
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    42
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    43
  def strings(ss: List[String]): String =
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 67200
diff changeset
    44
    ss.iterator.map(Bash.string).mkString(" ")
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    45
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    46
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    47
  /* process and result */
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    48
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
    49
  type Watchdog = (Time, Process => Boolean)
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
    50
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    51
  def process(script: String,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62569
diff changeset
    52
      cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    53
      env: Map[String, String] = Isabelle_System.settings(),
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    54
      redirect: Boolean = false,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    55
      cleanup: () => Unit = () => ()): Process =
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    56
    new Process(script, cwd, env, redirect, cleanup)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    57
63996
3f47fec9edfc tuned whitespace;
wenzelm
parents: 63805
diff changeset
    58
  class Process private[Bash](
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    59
      script: String,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    60
      cwd: JFile,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    61
      env: Map[String, String],
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    62
      redirect: Boolean,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    63
      cleanup: () => Unit)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    64
  {
62604
wenzelm
parents: 62602
diff changeset
    65
    private val timing_file = Isabelle_System.tmp_file("bash_timing")
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    66
    private val timing = Synchronized[Option[Timing]](None)
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
    67
    def get_timing: Timing = timing.value getOrElse Timing.zero
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    68
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    69
    private val script_file = Isabelle_System.tmp_file("bash_script")
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    70
    File.write(script_file, script)
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    71
62296
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 61025
diff changeset
    72
    private val proc =
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    73
      Isabelle_System.process(
73855
981df2e1f646 clarified command-line;
wenzelm
parents: 73821
diff changeset
    74
        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    75
          File.standard_path(timing_file), "bash", File.standard_path(script_file)),
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    76
        cwd = cwd, env = env, redirect = redirect)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    77
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    78
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    79
    // channels
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    80
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    81
    val stdin: BufferedWriter =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    82
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    83
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    84
    val stdout: BufferedReader =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    85
      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    86
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    87
    val stderr: BufferedReader =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    88
      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    89
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    90
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    91
    // signals
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    92
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
    93
    private val group_pid = stdout.readLine
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    94
73858
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
    95
    private val initial_process: Option[ProcessHandle] =
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
    96
      if (Platform.is_unix) ProcessHandle.of(Value.Long.parse(group_pid)).toScala
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
    97
      else None
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
    98
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
    99
    @tailrec private def signal(s: String, count: Int = 1): Boolean =
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   100
    {
71922
wenzelm
parents: 71921
diff changeset
   101
      count <= 0 ||
wenzelm
parents: 71921
diff changeset
   102
      {
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
   103
        Isabelle_System.process_signal(group_pid, signal = s)
73858
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
   104
        val running =
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
   105
          (initial_process.isDefined && initial_process.get.isAlive) ||
37243ad3ecb6 fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents: 73857
diff changeset
   106
          Isabelle_System.process_signal(group_pid)
71923
wenzelm
parents: 71922
diff changeset
   107
        if (running) {
71921
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71899
diff changeset
   108
          Time.seconds(0.1).sleep
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
   109
          signal(s, count - 1)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   110
        }
71922
wenzelm
parents: 71921
diff changeset
   111
        else false
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   112
      }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   113
    }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   114
71928
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71924
diff changeset
   115
    def terminate(): Unit = Isabelle_Thread.try_uninterruptible
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   116
    {
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
   117
      signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   118
      proc.destroy()
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   119
      do_cleanup()
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   120
    }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   121
71928
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71924
diff changeset
   122
    def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
71921
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71899
diff changeset
   123
    {
73857
19c558ea903c clarified signature;
wenzelm
parents: 73855
diff changeset
   124
      Isabelle_System.process_signal(group_pid, "INT")
71921
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71899
diff changeset
   125
    }
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71899
diff changeset
   126
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   127
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   128
    // JVM shutdown hook
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   129
71928
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71924
diff changeset
   130
    private val shutdown_hook = Isabelle_Thread.create(() => terminate())
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   131
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   132
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   133
    catch { case _: IllegalStateException => }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   134
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   135
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   136
    // cleanup
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   137
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73583
diff changeset
   138
    private def do_cleanup(): Unit =
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   139
    {
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   140
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   141
      catch { case _: IllegalStateException => }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   142
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   143
      script_file.delete
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   144
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   145
      timing.change {
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   146
        case None =>
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   147
          if (timing_file.isFile) {
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   148
            val t =
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   149
              Word.explode(File.read(timing_file)) match {
63805
c272680df665 clarified modules;
wenzelm
parents: 62610
diff changeset
   150
                case List(Value.Long(elapsed), Value.Long(cpu)) =>
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   151
                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   152
                case _ => Timing.zero
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   153
              }
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   154
            timing_file.delete
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   155
            Some(t)
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   156
          }
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   157
          else Some(Timing.zero)
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   158
        case some => some
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   159
      }
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   160
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   161
      cleanup()
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   162
    }
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   163
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   164
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   165
    // join
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   166
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   167
    def join: Int =
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   168
    {
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   169
      val rc = proc.waitFor
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   170
      do_cleanup()
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   171
      rc
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   172
    }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   173
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   174
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   175
    // result
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   176
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   177
    def result(
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   178
      progress_stdout: String => Unit = (_: String) => (),
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   179
      progress_stderr: String => Unit = (_: String) => (),
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   180
      watchdog: Option[Watchdog] = None,
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   181
      strict: Boolean = true): Process_Result =
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   182
    {
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   183
      stdin.close()
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   184
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   185
      val out_lines =
72335
a1fb4d28e609 unused --- superseded by PIDE messages;
wenzelm
parents: 71928
diff changeset
   186
        Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   187
      val err_lines =
72335
a1fb4d28e609 unused --- superseded by PIDE messages;
wenzelm
parents: 71928
diff changeset
   188
        Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   189
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   190
      val watchdog_thread =
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   191
        for ((time, check) <- watchdog)
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   192
        yield {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   193
          Future.thread("bash_watchdog") {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   194
            while (proc.isAlive) {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   195
              time.sleep
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   196
              if (check(this)) interrupt()
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   197
            }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   198
          }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   199
        }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   200
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   201
      val rc =
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   202
        try { join }
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   203
        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   204
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   205
      watchdog_thread.foreach(_.cancel())
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72335
diff changeset
   206
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   207
      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   208
73379
8a8ffe78eee7 clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents: 72834
diff changeset
   209
      Process_Result(rc, out_lines.join, err_lines.join, get_timing)
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   210
    }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   211
  }
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   212
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   213
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   214
  /* Scala function */
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   215
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   216
  object Process extends Scala.Fun_Strings("bash_process", thread = true)
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   217
  {
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   218
    val here = Scala_Project.here
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   219
    def apply(args: List[String]): List[String] =
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   220
    {
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   221
      val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) }
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   222
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   223
      val is_interrupt =
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   224
        result match {
73510
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73476
diff changeset
   225
          case Exn.Res(res) => res.rc == Exn.Interrupt.return_code
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   226
          case Exn.Exn(exn) => Exn.is_interrupt(exn)
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   227
        }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   228
73515
c8abfe393c16 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents: 73512
diff changeset
   229
      result match {
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   230
        case _ if is_interrupt => Nil
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   231
        case Exn.Exn(exn) => List(Exn.message(exn))
73515
c8abfe393c16 more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents: 73512
diff changeset
   232
        case Exn.Res(res) =>
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   233
          res.rc.toString ::
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   234
          res.timing.elapsed.ms.toString ::
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   235
          res.timing.cpu.ms.toString ::
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   236
          res.out_lines.length.toString ::
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73671
diff changeset
   237
          res.out_lines ::: res.err_lines
73474
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   238
      }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   239
    }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73379
diff changeset
   240
  }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   241
}