1/* Title: Pure/System/bash.scala 2 Author: Makarius 3 4GNU bash processes, with propagation of interrupts. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile, BufferedReader, InputStreamReader, 11 BufferedWriter, OutputStreamWriter} 12 13 14object Bash 15{ 16 /* concrete syntax */ 17 18 private def bash_chr(c: Byte): String = 19 { 20 val ch = c.toChar 21 ch match { 22 case '\t' => "$'\\t'" 23 case '\n' => "$'\\n'" 24 case '\f' => "$'\\f'" 25 case '\r' => "$'\\r'" 26 case _ => 27 if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) 28 Symbol.ascii(ch) 29 else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" 30 else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" 31 else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" 32 else "\\" + ch 33 } 34 } 35 36 def string(s: String): String = 37 if (s == "") "\"\"" 38 else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString 39 40 def strings(ss: List[String]): String = 41 ss.iterator.map(Bash.string(_)).mkString(" ") 42 43 44 /* process and result */ 45 46 private class Limited_Progress(proc: Process, progress_limit: Option[Long]) 47 { 48 private var count = 0L 49 def apply(progress: String => Unit)(line: String): Unit = synchronized { 50 progress(line) 51 count = count + line.length + 1 52 progress_limit match { 53 case Some(limit) if count > limit => proc.terminate 54 case _ => 55 } 56 } 57 } 58 59 def process(script: String, 60 cwd: JFile = null, 61 env: Map[String, String] = Isabelle_System.settings(), 62 redirect: Boolean = false, 63 cleanup: () => Unit = () => ()): Process = 64 new Process(script, cwd, env, redirect, cleanup) 65 66 class Process private[Bash]( 67 script: String, 68 cwd: JFile, 69 env: Map[String, String], 70 redirect: Boolean, 71 cleanup: () => Unit) 72 { 73 private val timing_file = Isabelle_System.tmp_file("bash_timing") 74 private val timing = Synchronized[Option[Timing]](None) 75 def get_timing: Timing = timing.value getOrElse Timing.zero 76 77 private val script_file = Isabelle_System.tmp_file("bash_script") 78 File.write(script_file, script) 79 80 private val proc = 81 Isabelle_System.process( 82 List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", 83 File.standard_path(timing_file), "bash", File.standard_path(script_file)), 84 cwd = cwd, env = env, redirect = redirect) 85 86 87 // channels 88 89 val stdin: BufferedWriter = 90 new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) 91 92 val stdout: BufferedReader = 93 new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) 94 95 val stderr: BufferedReader = 96 new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) 97 98 99 // signals 100 101 private val pid = stdout.readLine 102 103 def interrupt() 104 { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } } 105 106 private def kill(signal: String): Boolean = 107 Exn.Interrupt.postpone { 108 Isabelle_System.kill(signal, pid) 109 Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true 110 111 private def multi_kill(signal: String): Boolean = 112 { 113 var running = true 114 var count = 10 115 while (running && count > 0) { 116 if (kill(signal)) { 117 Exn.Interrupt.postpone { 118 Thread.sleep(100) 119 count -= 1 120 } 121 } 122 else running = false 123 } 124 running 125 } 126 127 def terminate() 128 { 129 multi_kill("INT") && multi_kill("TERM") && kill("KILL") 130 proc.destroy 131 do_cleanup() 132 } 133 134 135 // JVM shutdown hook 136 137 private val shutdown_hook = new Thread { override def run = terminate() } 138 139 try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } 140 catch { case _: IllegalStateException => } 141 142 143 // cleanup 144 145 private def do_cleanup() 146 { 147 try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } 148 catch { case _: IllegalStateException => } 149 150 script_file.delete 151 152 timing.change { 153 case None => 154 if (timing_file.isFile) { 155 val t = 156 Word.explode(File.read(timing_file)) match { 157 case List(Value.Long(elapsed), Value.Long(cpu)) => 158 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) 159 case _ => Timing.zero 160 } 161 timing_file.delete 162 Some(t) 163 } 164 else Some(Timing.zero) 165 case some => some 166 } 167 168 cleanup() 169 } 170 171 172 // join 173 174 def join: Int = 175 { 176 val rc = proc.waitFor 177 do_cleanup() 178 rc 179 } 180 181 182 // result 183 184 def result( 185 progress_stdout: String => Unit = (_: String) => (), 186 progress_stderr: String => Unit = (_: String) => (), 187 progress_limit: Option[Long] = None, 188 strict: Boolean = true): Process_Result = 189 { 190 stdin.close 191 192 val limited = new Limited_Progress(this, progress_limit) 193 val out_lines = 194 Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) } 195 val err_lines = 196 Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) } 197 198 val rc = 199 try { join } 200 catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } 201 if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() 202 203 Process_Result(rc, out_lines.join, err_lines.join, false, get_timing) 204 } 205 } 206} 207