src/Pure/Tools/isabelle_process.scala
author wenzelm
Sat Oct 04 14:29:45 2008 +0200 (2008-10-04 ago)
changeset 28497 40e1cc165b05
parent 28344 f4a17868bde5
child 28498 cb1b43edb5ed
permissions -rw-r--r--
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm@27963
     1
/*  Title:      Pure/Tools/isabelle_process.ML
wenzelm@27949
     2
    ID:         $Id$
wenzelm@27949
     3
    Author:     Makarius
wenzelm@27963
     4
    Options:    :folding=explicit:collapseFolds=1:
wenzelm@27949
     5
wenzelm@27949
     6
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm@27949
     7
*/
wenzelm@27949
     8
wenzelm@27949
     9
package isabelle
wenzelm@27949
    10
wenzelm@27949
    11
import java.util.Properties
wenzelm@27955
    12
import java.util.concurrent.LinkedBlockingQueue
wenzelm@28045
    13
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
wenzelm@28056
    14
  InputStream, OutputStream, IOException}
wenzelm@27949
    15
wenzelm@27963
    16
import isabelle.{Symbol, XML}
wenzelm@27949
    17
wenzelm@27949
    18
wenzelm@27973
    19
object IsabelleProcess {
wenzelm@27973
    20
wenzelm@27949
    21
  /* results */
wenzelm@27949
    22
wenzelm@27949
    23
  object Kind extends Enumeration {
wenzelm@28344
    24
    //{{{ values and codes
wenzelm@28344
    25
    // internal system notification
wenzelm@28344
    26
    val SYSTEM = Value("SYSTEM")
wenzelm@27949
    27
    // Posix channels/events
wenzelm@27949
    28
    val STDIN = Value("STDIN")
wenzelm@27949
    29
    val STDOUT = Value("STDOUT")
wenzelm@27949
    30
    val SIGNAL = Value("SIGNAL")
wenzelm@27949
    31
    val EXIT = Value("EXIT")
wenzelm@27949
    32
    // Isabelle messages
wenzelm@28344
    33
    val INIT = Value("INIT")
wenzelm@28344
    34
    val STATUS = Value("STATUS")
wenzelm@27949
    35
    val WRITELN = Value("WRITELN")
wenzelm@27949
    36
    val PRIORITY = Value("PRIORITY")
wenzelm@27949
    37
    val TRACING = Value("TRACING")
wenzelm@27949
    38
    val WARNING = Value("WARNING")
wenzelm@27949
    39
    val ERROR = Value("ERROR")
wenzelm@27949
    40
    val DEBUG = Value("DEBUG")
wenzelm@27949
    41
    val PROMPT = Value("PROMPT")
wenzelm@28344
    42
    // messages codes
wenzelm@28344
    43
    val code = Map(
wenzelm@28344
    44
      ('A' : Int) -> Kind.INIT,
wenzelm@28344
    45
      ('B' : Int) -> Kind.STATUS,
wenzelm@28344
    46
      ('C' : Int) -> Kind.WRITELN,
wenzelm@28344
    47
      ('D' : Int) -> Kind.PRIORITY,
wenzelm@28344
    48
      ('E' : Int) -> Kind.TRACING,
wenzelm@28344
    49
      ('F' : Int) -> Kind.WARNING,
wenzelm@28344
    50
      ('G' : Int) -> Kind.ERROR,
wenzelm@28344
    51
      ('H' : Int) -> Kind.DEBUG,
wenzelm@28344
    52
      ('I' : Int) -> Kind.PROMPT,
wenzelm@28344
    53
      ('0' : Int) -> Kind.SYSTEM,
wenzelm@28344
    54
      ('1' : Int) -> Kind.STDIN,
wenzelm@28344
    55
      ('2' : Int) -> Kind.STDOUT,
wenzelm@28344
    56
      ('3' : Int) -> Kind.SIGNAL,
wenzelm@28344
    57
      ('4' : Int) -> Kind.EXIT)
wenzelm@27949
    58
    //}}}
wenzelm@27949
    59
    def is_raw(kind: Value) =
wenzelm@28045
    60
      kind == STDOUT
wenzelm@27990
    61
    def is_control(kind: Value) =
wenzelm@28344
    62
      kind == SYSTEM ||
wenzelm@27990
    63
      kind == SIGNAL ||
wenzelm@28344
    64
      kind == EXIT
wenzelm@27949
    65
    def is_system(kind: Value) =
wenzelm@28344
    66
      kind == SYSTEM ||
wenzelm@27949
    67
      kind == STDIN ||
wenzelm@27949
    68
      kind == SIGNAL ||
wenzelm@27949
    69
      kind == EXIT ||
wenzelm@27949
    70
      kind == STATUS ||
wenzelm@28344
    71
      kind == PROMPT
wenzelm@27949
    72
  }
wenzelm@27949
    73
wenzelm@27973
    74
  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
wenzelm@27949
    75
    override def toString = {
wenzelm@27963
    76
      val res = XML.content(YXML.parse_failsafe(result)).mkString("")
wenzelm@27955
    77
      if (props == null) kind.toString + " [[" + res + "]]"
wenzelm@27955
    78
      else kind.toString + " " + props.toString + " [[" + res + "]]"
wenzelm@27949
    79
    }
wenzelm@27973
    80
    def is_raw() = Kind.is_raw(kind)
wenzelm@27990
    81
    def is_control() = Kind.is_control(kind)
wenzelm@27973
    82
    def is_system() = Kind.is_system(kind)
wenzelm@27973
    83
  }
wenzelm@27949
    84
wenzelm@27973
    85
}
wenzelm@27973
    86
wenzelm@27973
    87
wenzelm@27973
    88
class IsabelleProcess(args: String*) {
wenzelm@27973
    89
wenzelm@27973
    90
  import IsabelleProcess._
wenzelm@27973
    91
wenzelm@27973
    92
wenzelm@27973
    93
  /* process information */
wenzelm@27973
    94
wenzelm@27973
    95
  private var proc: Process = null
wenzelm@27973
    96
  private var closing = false
wenzelm@27973
    97
  private var pid: String = null
wenzelm@27973
    98
  private var the_session: String = null
wenzelm@27973
    99
  def session() = the_session
wenzelm@27973
   100
wenzelm@27973
   101
wenzelm@27973
   102
  /* results */
wenzelm@27949
   103
wenzelm@27990
   104
  private val results = new LinkedBlockingQueue[Result]
wenzelm@27949
   105
wenzelm@27949
   106
  private def put_result(kind: Kind.Value, props: Properties, result: String) {
wenzelm@27963
   107
    if (kind == Kind.INIT && props != null) {
wenzelm@27973
   108
      pid = props.getProperty(Markup.PID)
wenzelm@27973
   109
      the_session = props.getProperty(Markup.SESSION)
wenzelm@27963
   110
    }
wenzelm@27955
   111
    results.put(new Result(kind, props, result))
wenzelm@27949
   112
  }
wenzelm@27949
   113
wenzelm@27990
   114
  def get_result() = results.take
wenzelm@27973
   115
wenzelm@27992
   116
  def try_result() = {
wenzelm@27992
   117
    val res = results.poll
wenzelm@27992
   118
    if (res != null) Some(res) else None
wenzelm@27992
   119
  }
wenzelm@27992
   120
wenzelm@27973
   121
wenzelm@27973
   122
  /* signals */
wenzelm@27973
   123
wenzelm@27973
   124
  def interrupt() = synchronized {
wenzelm@27993
   125
    if (proc == null) error("Cannot interrupt Isabelle: no process")
wenzelm@27973
   126
    if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
wenzelm@27973
   127
    else {
wenzelm@27973
   128
      try {
wenzelm@28063
   129
        if (IsabelleSystem.exec("kill", "-INT", pid).waitFor == 0)
wenzelm@27990
   130
          put_result(Kind.SIGNAL, null, "INT")
wenzelm@27990
   131
        else
wenzelm@27973
   132
          put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
wenzelm@27973
   133
      }
wenzelm@27993
   134
      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
wenzelm@27973
   135
    }
wenzelm@27973
   136
  }
wenzelm@27973
   137
wenzelm@27973
   138
  def kill() = synchronized {
wenzelm@27993
   139
    if (proc == 0) error("Cannot kill Isabelle: no process")
wenzelm@27973
   140
    else {
wenzelm@27973
   141
      try_close()
wenzelm@27990
   142
      Thread.sleep(500)
wenzelm@27973
   143
      put_result(Kind.SIGNAL, null, "KILL")
wenzelm@27973
   144
      proc.destroy
wenzelm@27973
   145
      proc = null
wenzelm@27990
   146
      pid = null
wenzelm@27973
   147
    }
wenzelm@27973
   148
  }
wenzelm@27973
   149
wenzelm@27949
   150
wenzelm@27949
   151
  /* output being piped into the process */
wenzelm@27949
   152
wenzelm@27990
   153
  private val output = new LinkedBlockingQueue[String]
wenzelm@27949
   154
wenzelm@28045
   155
  private def output_raw(text: String) = synchronized {
wenzelm@27993
   156
    if (proc == null) error("Cannot output to Isabelle: no process")
wenzelm@27993
   157
    if (closing) error("Cannot output to Isabelle: already closing")
wenzelm@27955
   158
    output.put(text)
wenzelm@27949
   159
  }
wenzelm@27949
   160
wenzelm@28303
   161
  def output_sync(text: String) =
wenzelm@28045
   162
    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
wenzelm@27949
   163
wenzelm@27963
   164
wenzelm@27963
   165
  def command(text: String) =
wenzelm@27949
   166
    output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   167
wenzelm@27963
   168
  def command(props: Properties, text: String) =
wenzelm@27949
   169
    output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
wenzelm@27949
   170
      IsabelleSyntax.encode_string(text))
wenzelm@27949
   171
wenzelm@27963
   172
  def ML(text: String) =
wenzelm@27949
   173
    output_sync("ML_val " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   174
wenzelm@27949
   175
  def close() = synchronized {    // FIXME watchdog/timeout
wenzelm@27949
   176
    output_raw("\u0000")
wenzelm@27949
   177
    closing = true
wenzelm@27949
   178
  }
wenzelm@27949
   179
wenzelm@27949
   180
  def try_close() = synchronized {
wenzelm@27949
   181
    if (proc != null && !closing) {
wenzelm@27949
   182
      try { close() }
wenzelm@27993
   183
      catch { case _: RuntimeException => }
wenzelm@27949
   184
    }
wenzelm@27949
   185
  }
wenzelm@27949
   186
wenzelm@27949
   187
wenzelm@27949
   188
  /* stdin */
wenzelm@27949
   189
wenzelm@28045
   190
  private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
wenzelm@27949
   191
    override def run() = {
wenzelm@28056
   192
      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
wenzelm@27949
   193
      var finished = false
wenzelm@27949
   194
      while (!finished) {
wenzelm@27949
   195
        try {
wenzelm@27949
   196
          //{{{
wenzelm@27955
   197
          val s = output.take
wenzelm@27949
   198
          if (s == "\u0000") {
wenzelm@27949
   199
            writer.close
wenzelm@27949
   200
            finished = true
wenzelm@27949
   201
          }
wenzelm@27949
   202
          else {
wenzelm@27949
   203
            put_result(Kind.STDIN, null, s)
wenzelm@27949
   204
            writer.write(s)
wenzelm@27949
   205
            writer.flush
wenzelm@27949
   206
          }
wenzelm@27949
   207
          //}}}
wenzelm@27949
   208
        }
wenzelm@27949
   209
        catch {
wenzelm@27949
   210
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage)
wenzelm@27949
   211
        }
wenzelm@27949
   212
      }
wenzelm@27949
   213
      put_result(Kind.SYSTEM, null, "Stdin thread terminated")
wenzelm@27949
   214
    }
wenzelm@27949
   215
  }
wenzelm@27949
   216
wenzelm@27949
   217
wenzelm@27949
   218
  /* stdout */
wenzelm@27949
   219
wenzelm@28045
   220
  private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
wenzelm@27949
   221
    override def run() = {
wenzelm@28056
   222
      val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
wenzelm@28045
   223
      var result = new StringBuilder(100)
wenzelm@27949
   224
wenzelm@27949
   225
      var finished = false
wenzelm@27949
   226
      while (!finished) {
wenzelm@27949
   227
        try {
wenzelm@28045
   228
          //{{{
wenzelm@28045
   229
          var c = -1
wenzelm@28045
   230
          var done = false
wenzelm@28045
   231
          while (!done && (result.length == 0 || reader.ready)) {
wenzelm@28045
   232
            c = reader.read
wenzelm@28045
   233
            if (c >= 0) result.append(c.asInstanceOf[Char])
wenzelm@28045
   234
            else done = true
wenzelm@28045
   235
          }
wenzelm@28045
   236
          if (result.length > 0) {
wenzelm@28045
   237
            put_result(Kind.STDOUT, null, result.toString)
wenzelm@28045
   238
            result.length = 0
wenzelm@27949
   239
          }
wenzelm@27949
   240
          else {
wenzelm@28045
   241
            reader.close
wenzelm@28045
   242
            finished = true
wenzelm@28045
   243
            try_close()
wenzelm@27949
   244
          }
wenzelm@28045
   245
          //}}}
wenzelm@27963
   246
        }
wenzelm@27963
   247
        catch {
wenzelm@27949
   248
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage)
wenzelm@27949
   249
        }
wenzelm@27949
   250
      }
wenzelm@27949
   251
      put_result(Kind.SYSTEM, null, "Stdout thread terminated")
wenzelm@27949
   252
    }
wenzelm@27949
   253
  }
wenzelm@27949
   254
wenzelm@27949
   255
wenzelm@28045
   256
  /* messages */
wenzelm@27949
   257
wenzelm@28045
   258
  private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
wenzelm@27949
   259
    override def run() = {
wenzelm@28056
   260
      val reader = IsabelleSystem.fifo_reader(fifo)
wenzelm@28045
   261
      var kind: Kind.Value = null
wenzelm@28045
   262
      var props: Properties = null
wenzelm@28045
   263
      var result = new StringBuilder
wenzelm@27949
   264
wenzelm@27949
   265
      var finished = false
wenzelm@27949
   266
      while (!finished) {
wenzelm@27949
   267
        try {
wenzelm@28063
   268
          if (kind == null) {
wenzelm@28063
   269
            //{{{ Char mode -- resync
wenzelm@28063
   270
            var c = -1
wenzelm@28063
   271
            do {
wenzelm@28063
   272
              c = reader.read
wenzelm@28063
   273
              if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
wenzelm@28063
   274
            } while (c >= 0 && c != 2)
wenzelm@28063
   275
wenzelm@28063
   276
            if (result.length > 0) {
wenzelm@28063
   277
              put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString)
wenzelm@28063
   278
              result.length = 0
wenzelm@28063
   279
            }
wenzelm@28063
   280
            if (c < 0) {
wenzelm@28063
   281
              reader.close
wenzelm@28063
   282
              finished = true
wenzelm@28063
   283
              try_close()
wenzelm@28045
   284
            }
wenzelm@28045
   285
            else {
wenzelm@28344
   286
              c = reader.read
wenzelm@28344
   287
              if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
wenzelm@28344
   288
              else kind = null
wenzelm@28063
   289
              props = null
wenzelm@28063
   290
            }
wenzelm@28063
   291
            //}}}
wenzelm@28063
   292
          }
wenzelm@28063
   293
          else {
wenzelm@28063
   294
            //{{{ Line mode
wenzelm@28063
   295
            val line = reader.readLine
wenzelm@28063
   296
            if (line == null) {
wenzelm@28063
   297
              reader.close
wenzelm@28063
   298
              finished = true
wenzelm@28063
   299
              try_close()
wenzelm@28063
   300
            }
wenzelm@28063
   301
            else {
wenzelm@28063
   302
              val len = line.length
wenzelm@28063
   303
              // property
wenzelm@28063
   304
              if (line.endsWith("\u0002,")) {
wenzelm@28063
   305
                val i = line.indexOf('=')
wenzelm@28063
   306
                if (i > 0) {
wenzelm@28063
   307
                  val name = line.substring(0, i)
wenzelm@28063
   308
                  val value = line.substring(i + 1, len - 2)
wenzelm@28063
   309
                  if (props == null) props = new Properties
wenzelm@28063
   310
                  if (!props.containsKey(name)) props.setProperty(name, value)
wenzelm@28045
   311
                }
wenzelm@28045
   312
              }
wenzelm@28063
   313
              // last text line
wenzelm@28063
   314
              else if (line.endsWith("\u0002.")) {
wenzelm@28063
   315
                result.append(line.substring(0, len - 2))
wenzelm@28063
   316
                put_result(kind, props, result.toString)
wenzelm@28063
   317
                result.length = 0
wenzelm@28063
   318
                kind = null
wenzelm@28063
   319
              }
wenzelm@28063
   320
              // text line
wenzelm@28063
   321
              else {
wenzelm@28063
   322
                result.append(line)
wenzelm@28063
   323
                result.append('\n')
wenzelm@28063
   324
              }
wenzelm@28045
   325
            }
wenzelm@28063
   326
            //}}}
wenzelm@27949
   327
          }
wenzelm@27963
   328
        }
wenzelm@28063
   329
        catch {
wenzelm@28063
   330
          case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage)
wenzelm@28063
   331
        }
wenzelm@27949
   332
      }
wenzelm@28063
   333
      put_result(Kind.SYSTEM, null, "Message thread terminated")
wenzelm@27949
   334
    }
wenzelm@27949
   335
  }
wenzelm@27949
   336
wenzelm@27949
   337
wenzelm@27949
   338
  /** main **/
wenzelm@27949
   339
wenzelm@27949
   340
  {
wenzelm@28497
   341
    /* isabelle version */
wenzelm@28497
   342
wenzelm@28497
   343
    {
wenzelm@28497
   344
      val (msg, rc) = IsabelleSystem.isabelle_tool("version")
wenzelm@28497
   345
      if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
wenzelm@28497
   346
      put_result(Kind.SYSTEM, null, msg)
wenzelm@28497
   347
    }
wenzelm@28497
   348
wenzelm@28045
   349
wenzelm@28045
   350
    /* message fifo */
wenzelm@28045
   351
wenzelm@28063
   352
    val message_fifo = IsabelleSystem.mk_fifo()
wenzelm@28063
   353
    def rm_fifo() = IsabelleSystem.rm_fifo(message_fifo)
wenzelm@28045
   354
wenzelm@28063
   355
    val message_thread = new MessageThread(message_fifo)
wenzelm@28063
   356
    message_thread.start
wenzelm@28045
   357
wenzelm@28045
   358
wenzelm@27973
   359
    /* exec process */
wenzelm@27963
   360
wenzelm@27973
   361
    try {
wenzelm@28063
   362
      val cmdline = List(IsabelleSystem.getenv_strict("ISABELLE_HOME") +
wenzelm@28063
   363
          "/bin/isabelle-process", "-W", message_fifo) ++ args
wenzelm@28063
   364
      proc = IsabelleSystem.exec2(cmdline: _*)
wenzelm@27949
   365
    }
wenzelm@27993
   366
    catch {
wenzelm@28063
   367
      case e: IOException =>
wenzelm@28063
   368
        rm_fifo()
wenzelm@28063
   369
        error("Failed to execute Isabelle process: " + e.getMessage)
wenzelm@27993
   370
    }
wenzelm@27949
   371
wenzelm@27949
   372
wenzelm@28045
   373
    /* stdin/stdout */
wenzelm@28045
   374
wenzelm@28045
   375
    new StdinThread(proc.getOutputStream).start
wenzelm@28045
   376
    new StdoutThread(proc.getInputStream).start
wenzelm@28045
   377
wenzelm@28045
   378
wenzelm@28045
   379
    /* exit */
wenzelm@27949
   380
wenzelm@28063
   381
    new Thread("isabelle: exit") {
wenzelm@28045
   382
      override def run() = {
wenzelm@28045
   383
        val rc = proc.waitFor()
wenzelm@28045
   384
        Thread.sleep(300)
wenzelm@28045
   385
        put_result(Kind.SYSTEM, null, "Exit thread terminated")
wenzelm@28045
   386
        put_result(Kind.EXIT, null, Integer.toString(rc))
wenzelm@28063
   387
        rm_fifo()
wenzelm@28045
   388
      }
wenzelm@28063
   389
    }.start
wenzelm@28063
   390
wenzelm@27949
   391
  }
wenzelm@27949
   392
wenzelm@27949
   393
}