src/Pure/PIDE/prover.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 70048 3fd9298dd200
child 70486 9f2a6856b912
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     1 /*  Title:      Pure/PIDE/prover.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:
     4 
     5 Prover process wrapping.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
    12 
    13 
    14 object Prover
    15 {
    16   /* messages */
    17 
    18   sealed abstract class Message
    19   type Receiver = Message => Unit
    20 
    21   class Input(val name: String, val args: List[String]) extends Message
    22   {
    23     override def toString: String =
    24       XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    25         args.map(s =>
    26           List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    27   }
    28 
    29   class Output(val message: XML.Elem) extends Message
    30   {
    31     def kind: String = message.markup.name
    32     def properties: Properties.T = message.markup.properties
    33     def body: XML.Body = message.body
    34 
    35     def is_init = kind == Markup.INIT
    36     def is_exit = kind == Markup.EXIT
    37     def is_stdout = kind == Markup.STDOUT
    38     def is_stderr = kind == Markup.STDERR
    39     def is_system = kind == Markup.SYSTEM
    40     def is_status = kind == Markup.STATUS
    41     def is_report = kind == Markup.REPORT
    42     def is_syslog = is_init || is_exit || is_system || is_stderr
    43 
    44     override def toString: String =
    45     {
    46       val res =
    47         if (is_status || is_report) message.body.map(_.toString).mkString
    48         else Pretty.string_of(message.body)
    49       if (properties.isEmpty)
    50         kind.toString + " [[" + res + "]]"
    51       else
    52         kind.toString + " " +
    53           (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
    54     }
    55   }
    56 
    57   class Protocol_Output(props: Properties.T, val bytes: Bytes)
    58     extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
    59   {
    60     lazy val text: String = bytes.text
    61   }
    62 }
    63 
    64 
    65 class Prover(
    66   receiver: Prover.Receiver,
    67   xml_cache: XML.Cache,
    68   channel: System_Channel,
    69   process: Bash.Process) extends Protocol
    70 {
    71   /** receiver output **/
    72 
    73   private def system_output(text: String)
    74   {
    75     receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
    76   }
    77 
    78   private def protocol_output(props: Properties.T, bytes: Bytes)
    79   {
    80     receiver(new Prover.Protocol_Output(props, bytes))
    81   }
    82 
    83   private def output(kind: String, props: Properties.T, body: XML.Body)
    84   {
    85     val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
    86     val reports = Protocol_Message.reports(props, body)
    87     for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
    88   }
    89 
    90   private def exit_message(result: Process_Result)
    91   {
    92     output(Markup.EXIT, Markup.Process_Result(result),
    93       List(XML.Text("Return code: " + result.rc.toString)))
    94   }
    95 
    96 
    97 
    98   /** process manager **/
    99 
   100   private val process_result: Future[Process_Result] =
   101     Future.thread("process_result") {
   102       val rc = process.join
   103       val timing = process.get_timing
   104       Process_Result(rc, timing = timing)
   105     }
   106 
   107   private def terminate_process()
   108   {
   109     try { process.terminate }
   110     catch {
   111       case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
   112     }
   113   }
   114 
   115   private val process_manager = Standard_Thread.fork("process_manager")
   116   {
   117     val (startup_failed, startup_errors) =
   118     {
   119       var finished: Option[Boolean] = None
   120       val result = new StringBuilder(100)
   121       while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
   122         while (finished.isEmpty && process.stderr.ready) {
   123           try {
   124             val c = process.stderr.read
   125             if (c == 2) finished = Some(true)
   126             else result += c.toChar
   127           }
   128           catch { case _: IOException => finished = Some(false) }
   129         }
   130         Thread.sleep(10)
   131       }
   132       (finished.isEmpty || !finished.get, result.toString.trim)
   133     }
   134     if (startup_errors != "") system_output(startup_errors)
   135 
   136     if (startup_failed) {
   137       terminate_process()
   138       process_result.join
   139       exit_message(Process_Result(127))
   140     }
   141     else {
   142       val (command_stream, message_stream) = channel.rendezvous()
   143 
   144       command_input_init(command_stream)
   145       val stdout = physical_output(false)
   146       val stderr = physical_output(true)
   147       val message = message_output(message_stream)
   148 
   149       val result = process_result.join
   150       system_output("process terminated")
   151       command_input_close()
   152       for (thread <- List(stdout, stderr, message)) thread.join
   153       system_output("process_manager terminated")
   154       exit_message(result)
   155     }
   156     channel.shutdown()
   157   }
   158 
   159 
   160   /* management methods */
   161 
   162   def join() { process_manager.join() }
   163 
   164   def terminate()
   165   {
   166     system_output("Terminating prover process")
   167     command_input_close()
   168 
   169     var count = 10
   170     while (!process_result.is_finished && count > 0) {
   171       Thread.sleep(100)
   172       count -= 1
   173     }
   174     if (!process_result.is_finished) terminate_process()
   175   }
   176 
   177 
   178 
   179   /** process streams **/
   180 
   181   /* command input */
   182 
   183   private var command_input: Option[Consumer_Thread[List[Bytes]]] = None
   184 
   185   private def command_input_close(): Unit = command_input.foreach(_.shutdown)
   186 
   187   private def command_input_init(raw_stream: OutputStream)
   188   {
   189     val name = "command_input"
   190     val stream = new BufferedOutputStream(raw_stream)
   191     command_input =
   192       Some(
   193         Consumer_Thread.fork(name)(
   194           consume =
   195             {
   196               case chunks =>
   197                 try {
   198                   Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream)
   199                   chunks.foreach(_.write_stream(stream))
   200                   stream.flush
   201                   true
   202                 }
   203                 catch { case e: IOException => system_output(name + ": " + e.getMessage); false }
   204             },
   205           finish = { case () => stream.close; system_output(name + " terminated") }
   206         )
   207       )
   208   }
   209 
   210 
   211   /* physical output */
   212 
   213   private def physical_output(err: Boolean): Thread =
   214   {
   215     val (name, reader, markup) =
   216       if (err) ("standard_error", process.stderr, Markup.STDERR)
   217       else ("standard_output", process.stdout, Markup.STDOUT)
   218 
   219     Standard_Thread.fork(name) {
   220       try {
   221         var result = new StringBuilder(100)
   222         var finished = false
   223         while (!finished) {
   224           //{{{
   225           var c = -1
   226           var done = false
   227           while (!done && (result.length == 0 || reader.ready)) {
   228             c = reader.read
   229             if (c >= 0) result.append(c.asInstanceOf[Char])
   230             else done = true
   231           }
   232           if (result.length > 0) {
   233             output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
   234             result.length = 0
   235           }
   236           else {
   237             reader.close
   238             finished = true
   239           }
   240           //}}}
   241         }
   242       }
   243       catch { case e: IOException => system_output(name + ": " + e.getMessage) }
   244       system_output(name + " terminated")
   245     }
   246   }
   247 
   248 
   249   /* message output */
   250 
   251   private def message_output(stream: InputStream): Thread =
   252   {
   253     class EOF extends Exception
   254     class Protocol_Error(msg: String) extends Exception(msg)
   255 
   256     val name = "message_output"
   257     Standard_Thread.fork(name) {
   258       val default_buffer = new Array[Byte](65536)
   259       var c = -1
   260 
   261       def read_int(): Int =
   262       //{{{
   263       {
   264         var n = 0
   265         c = stream.read
   266         if (c == -1) throw new EOF
   267         while (48 <= c && c <= 57) {
   268           n = 10 * n + (c - 48)
   269           c = stream.read
   270         }
   271         if (c != 10)
   272           throw new Protocol_Error("malformed header: expected integer followed by newline")
   273         else n
   274       }
   275       //}}}
   276 
   277       def read_chunk_bytes(): (Array[Byte], Int) =
   278       //{{{
   279       {
   280         val n = read_int()
   281         val buf =
   282           if (n <= default_buffer.length) default_buffer
   283           else new Array[Byte](n)
   284 
   285         var i = 0
   286         var m = 0
   287         do {
   288           m = stream.read(buf, i, n - i)
   289           if (m != -1) i += m
   290         }
   291         while (m != -1 && n > i)
   292 
   293         if (i != n)
   294           throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)")
   295 
   296         (buf, n)
   297       }
   298       //}}}
   299 
   300       def read_chunk(): XML.Body =
   301       {
   302         val (buf, n) = read_chunk_bytes()
   303         YXML.parse_body_failsafe(UTF8.decode_chars(Symbol.decode, buf, 0, n))
   304       }
   305 
   306       try {
   307         do {
   308           try {
   309             val header = read_chunk()
   310             header match {
   311               case List(XML.Elem(Markup(name, props), Nil)) =>
   312                 val kind = name.intern
   313                 if (kind == Markup.PROTOCOL) {
   314                   val (buf, n) = read_chunk_bytes()
   315                   protocol_output(props, Bytes(buf, 0, n))
   316                 }
   317                 else {
   318                   val body = read_chunk()
   319                   output(kind, props, body)
   320                 }
   321               case _ =>
   322                 read_chunk()
   323                 throw new Protocol_Error("bad header: " + header.toString)
   324             }
   325           }
   326           catch { case _: EOF => }
   327         }
   328         while (c != -1)
   329       }
   330       catch {
   331         case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
   332         case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
   333       }
   334       stream.close
   335 
   336       system_output(name + " terminated")
   337     }
   338   }
   339 
   340 
   341 
   342   /** protocol commands **/
   343 
   344   def protocol_command_bytes(name: String, args: Bytes*): Unit =
   345     command_input match {
   346       case Some(thread) if thread.is_active => thread.send(Bytes(name) :: args.toList)
   347       case _ => error("Inactive prover input thread for command " + quote(name))
   348     }
   349 
   350   def protocol_command(name: String, args: String*)
   351   {
   352     receiver(new Prover.Input(name, args.toList))
   353     protocol_command_bytes(name, args.map(Bytes(_)): _*)
   354   }
   355 }