src/Pure/System/isabelle_system.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 37132 10ef4da1c314
child 37367 8680677265c9
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
wenzelm@30175
     1
/*  Title:      Pure/System/isabelle_system.scala
wenzelm@27919
     2
    Author:     Makarius
wenzelm@27919
     3
wenzelm@34201
     4
Isabelle system support (settings environment etc.).
wenzelm@27919
     5
*/
wenzelm@27919
     6
wenzelm@27919
     7
package isabelle
wenzelm@27919
     8
wenzelm@31520
     9
import java.util.regex.Pattern
wenzelm@31820
    10
import java.util.Locale
wenzelm@34198
    11
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
wenzelm@34198
    12
  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
wenzelm@34162
    13
  File, IOException}
wenzelm@34024
    14
import java.awt.{GraphicsEnvironment, Font}
wenzelm@28063
    15
wenzelm@28063
    16
import scala.io.Source
wenzelm@31520
    17
import scala.util.matching.Regex
wenzelm@34163
    18
import scala.collection.mutable
wenzelm@27936
    19
wenzelm@27919
    20
wenzelm@37013
    21
class Isabelle_System(this_isabelle_home: String) extends Standard_System
wenzelm@31498
    22
{
wenzelm@37013
    23
  def this() = this(null)
wenzelm@37013
    24
wenzelm@37013
    25
wenzelm@31796
    26
  /** Isabelle environment **/
wenzelm@31796
    27
wenzelm@37013
    28
  /*
wenzelm@37013
    29
    isabelle_home precedence:
wenzelm@37013
    30
      (1) this_isabelle_home as explicit argument
wenzelm@37013
    31
      (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
wenzelm@37013
    32
      (3) isabelle.home system property (e.g. via JVM application boot process)
wenzelm@37013
    33
  */
wenzelm@37013
    34
wenzelm@31498
    35
  private val environment: Map[String, String] =
wenzelm@31498
    36
  {
wenzelm@36011
    37
    import scala.collection.JavaConversions._
wenzelm@31498
    38
wenzelm@36193
    39
    val env0 = Map(java.lang.System.getenv.toList: _*) +
wenzelm@36193
    40
      ("THIS_JAVA" -> this_java())
wenzelm@27919
    41
wenzelm@31927
    42
    val isabelle_home =
wenzelm@37013
    43
      if (this_isabelle_home != null) this_isabelle_home
wenzelm@37013
    44
      else
wenzelm@37013
    45
        env0.get("ISABELLE_HOME") match {
wenzelm@37013
    46
          case None | Some("") =>
wenzelm@37013
    47
            val path = java.lang.System.getProperty("isabelle.home")
wenzelm@37013
    48
            if (path == null || path == "") error("Unknown Isabelle home directory")
wenzelm@37013
    49
            else path
wenzelm@37013
    50
          case Some(path) => path
wenzelm@37013
    51
        }
wenzelm@29177
    52
wenzelm@34201
    53
    Standard_System.with_tmp_file("settings") { dump =>
wenzelm@34201
    54
        val shell_prefix =
wenzelm@34201
    55
          if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
wenzelm@34201
    56
        val cmdline =
wenzelm@34201
    57
          shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
wenzelm@34258
    58
        val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
wenzelm@34201
    59
        if (rc != 0) error(output)
wenzelm@31498
    60
wenzelm@34201
    61
        val entries =
wenzelm@34201
    62
          for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
wenzelm@34201
    63
            val i = entry.indexOf('=')
wenzelm@34201
    64
            if (i <= 0) (entry -> "")
wenzelm@34201
    65
            else (entry.substring(0, i) -> entry.substring(i + 1))
wenzelm@34201
    66
          }
wenzelm@34201
    67
        Map(entries: _*) +
wenzelm@34201
    68
          ("HOME" -> java.lang.System.getenv("HOME")) +
wenzelm@34201
    69
          ("PATH" -> java.lang.System.getenv("PATH"))
wenzelm@34201
    70
      }
wenzelm@27953
    71
  }
wenzelm@27919
    72
wenzelm@31796
    73
wenzelm@34204
    74
  /* external processes */
wenzelm@34204
    75
wenzelm@34204
    76
  def execute(redirect: Boolean, args: String*): Process =
wenzelm@34204
    77
  {
wenzelm@34204
    78
    val cmdline =
wenzelm@34204
    79
      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
wenzelm@34204
    80
      else args
wenzelm@34219
    81
    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
wenzelm@34204
    82
  }
wenzelm@34204
    83
wenzelm@34204
    84
wenzelm@31796
    85
  /* getenv */
wenzelm@31796
    86
wenzelm@31498
    87
  def getenv(name: String): String =
wenzelm@31498
    88
    environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
wenzelm@31498
    89
wenzelm@31498
    90
  def getenv_strict(name: String): String =
wenzelm@31498
    91
  {
wenzelm@31234
    92
    val value = getenv(name)
wenzelm@27993
    93
    if (value != "") value else error("Undefined environment variable: " + name)
wenzelm@27919
    94
  }
wenzelm@27919
    95
wenzelm@37058
    96
  override def toString = getenv_strict("ISABELLE_HOME")
wenzelm@31703
    97
wenzelm@27936
    98
wenzelm@31796
    99
wenzelm@31796
   100
  /** file path specifications **/
wenzelm@31796
   101
wenzelm@31820
   102
  /* expand_path */
wenzelm@31796
   103
wenzelm@36136
   104
  private val Root = new Regex("(//+[^/]*|/)(.*)")
wenzelm@36136
   105
  private val Only_Root = new Regex("//+[^/]*|/")
wenzelm@36136
   106
wenzelm@31820
   107
  def expand_path(isabelle_path: String): String =
wenzelm@31796
   108
  {
wenzelm@31796
   109
    val result_path = new StringBuilder
wenzelm@36136
   110
    def init(path: String): String =
wenzelm@31796
   111
    {
wenzelm@36136
   112
      path match {
wenzelm@36136
   113
        case Root(root, rest) =>
wenzelm@36136
   114
          result_path.clear
wenzelm@36136
   115
          result_path ++= root
wenzelm@36136
   116
          rest
wenzelm@36136
   117
        case _ => path
wenzelm@31796
   118
      }
wenzelm@31796
   119
    }
wenzelm@31796
   120
    def append(path: String)
wenzelm@31796
   121
    {
wenzelm@36136
   122
      val rest = init(path)
wenzelm@36136
   123
      for (p <- rest.split("/") if p != "" && p != ".") {
wenzelm@31803
   124
        if (p == "..") {
wenzelm@31803
   125
          val result = result_path.toString
wenzelm@36136
   126
          if (!Only_Root.pattern.matcher(result).matches) {
wenzelm@36136
   127
            val i = result.lastIndexOf("/")
wenzelm@36136
   128
            if (result == "")
wenzelm@36136
   129
              result_path ++= ".."
wenzelm@36136
   130
            else if (result.substring(i + 1) == "..")
wenzelm@36136
   131
              result_path ++= "/.."
wenzelm@36136
   132
            else if (i < 0)
wenzelm@36136
   133
              result_path.length = 0
wenzelm@36136
   134
            else
wenzelm@36136
   135
              result_path.length = i
wenzelm@36136
   136
          }
wenzelm@31803
   137
        }
wenzelm@31803
   138
        else {
wenzelm@31803
   139
          val len = result_path.length
wenzelm@31803
   140
          if (len > 0 && result_path(len - 1) != '/')
wenzelm@31803
   141
            result_path += '/'
wenzelm@31803
   142
          result_path ++= p
wenzelm@31803
   143
        }
wenzelm@31796
   144
      }
wenzelm@31796
   145
    }
wenzelm@36136
   146
    val rest = init(isabelle_path)
wenzelm@36136
   147
    for (p <- rest.split("/")) {
wenzelm@31796
   148
      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
wenzelm@31796
   149
      else if (p == "~") append(getenv_strict("HOME"))
wenzelm@31796
   150
      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
wenzelm@31796
   151
      else append(p)
wenzelm@31796
   152
    }
wenzelm@31796
   153
    result_path.toString
wenzelm@31796
   154
  }
wenzelm@31796
   155
wenzelm@31796
   156
wenzelm@31820
   157
  /* platform_path */
wenzelm@27936
   158
wenzelm@31820
   159
  def platform_path(isabelle_path: String): String =
wenzelm@34201
   160
    jvm_path(expand_path(isabelle_path))
wenzelm@27953
   161
wenzelm@31498
   162
  def platform_file(path: String) = new File(platform_path(path))
wenzelm@29152
   163
wenzelm@27953
   164
wenzelm@36991
   165
  /* try_read */
wenzelm@36991
   166
wenzelm@37058
   167
  def try_read(paths: Seq[String]): String =
wenzelm@36991
   168
  {
wenzelm@37058
   169
    val buf = new StringBuilder
wenzelm@37058
   170
    for {
wenzelm@37058
   171
      path <- paths
wenzelm@37058
   172
      file = platform_file(path) if file.isFile
wenzelm@37058
   173
      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
wenzelm@37058
   174
    } buf.append(c)
wenzelm@37058
   175
    buf.toString
wenzelm@36991
   176
  }
wenzelm@36991
   177
wenzelm@36991
   178
wenzelm@31436
   179
  /* source files */
wenzelm@31436
   180
wenzelm@31436
   181
  private def try_file(file: File) = if (file.isFile) Some(file) else None
wenzelm@31436
   182
wenzelm@31498
   183
  def source_file(path: String): Option[File] =
wenzelm@31498
   184
  {
wenzelm@31498
   185
    if (path.startsWith("/") || path == "")
wenzelm@31436
   186
      try_file(platform_file(path))
wenzelm@31436
   187
    else {
wenzelm@34201
   188
      val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
wenzelm@31436
   189
      if (pure_file.isFile) Some(pure_file)
wenzelm@31436
   190
      else if (getenv("ML_SOURCES") != "")
wenzelm@31436
   191
        try_file(platform_file("$ML_SOURCES/" + path))
wenzelm@31436
   192
      else None
wenzelm@31436
   193
    }
wenzelm@31436
   194
  }
wenzelm@31436
   195
wenzelm@31436
   196
wenzelm@32450
   197
wenzelm@31796
   198
  /** system tools **/
wenzelm@31796
   199
wenzelm@35010
   200
  def bash_output(script: String): (String, Int) =
wenzelm@34198
   201
  {
wenzelm@34201
   202
    Standard_System.with_tmp_file("isabelle_script") { script_file =>
wenzelm@34201
   203
      Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
wenzelm@34201
   204
        Standard_System.with_tmp_file("isabelle_output") { output_file =>
wenzelm@34198
   205
wenzelm@34201
   206
          Standard_System.write_file(script_file, script)
wenzelm@34198
   207
wenzelm@35023
   208
          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
wenzelm@34198
   209
            script_file.getPath, pid_file.getPath, output_file.getPath)
wenzelm@34198
   210
wenzelm@34199
   211
          def kill(strict: Boolean) =
wenzelm@34198
   212
          {
wenzelm@34199
   213
            val pid =
wenzelm@34201
   214
              try { Some(Standard_System.read_file(pid_file)) }
wenzelm@34199
   215
              catch { case _: IOException => None }
wenzelm@34199
   216
            if (pid.isDefined) {
wenzelm@34199
   217
              var running = true
wenzelm@37132
   218
              var count = 10   // FIXME property!?
wenzelm@34199
   219
              while (running && count > 0) {
wenzelm@34199
   220
                if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
wenzelm@34199
   221
                  running = false
wenzelm@34199
   222
                else {
wenzelm@37132
   223
                  Thread.sleep(100)   // FIXME property!?
wenzelm@34199
   224
                  if (!strict) count -= 1
wenzelm@34199
   225
                }
wenzelm@34199
   226
              }
wenzelm@34198
   227
            }
wenzelm@34198
   228
          }
wenzelm@34198
   229
wenzelm@34199
   230
          val shutdown_hook = new Thread { override def run = kill(true) }
wenzelm@34201
   231
          Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
wenzelm@34198
   232
wenzelm@34198
   233
          def cleanup() =
wenzelm@34198
   234
            try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
wenzelm@34198
   235
            catch { case _: IllegalStateException => }
wenzelm@34198
   236
wenzelm@34198
   237
          val rc =
wenzelm@34198
   238
            try {
wenzelm@34198
   239
              try { proc.waitFor }  // FIXME read stderr (!??)
wenzelm@34199
   240
              catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
wenzelm@34198
   241
            }
wenzelm@34198
   242
            finally {
wenzelm@34198
   243
              proc.getOutputStream.close
wenzelm@34198
   244
              proc.getInputStream.close
wenzelm@34198
   245
              proc.getErrorStream.close
wenzelm@34198
   246
              proc.destroy
wenzelm@34198
   247
              cleanup()
wenzelm@34198
   248
            }
wenzelm@34198
   249
wenzelm@34198
   250
          val output =
wenzelm@34201
   251
            try { Standard_System.read_file(output_file) }
wenzelm@34198
   252
            catch { case _: IOException => "" }
wenzelm@34198
   253
wenzelm@34198
   254
          (output, rc)
wenzelm@34198
   255
        }
wenzelm@34198
   256
      }
wenzelm@34198
   257
    }
wenzelm@34198
   258
  }
wenzelm@34198
   259
wenzelm@31818
   260
  def isabelle_tool(name: String, args: String*): (String, Int) =
wenzelm@31498
   261
  {
wenzelm@34200
   262
    getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
wenzelm@31818
   263
      val file = platform_file(dir + "/" + name)
wenzelm@34025
   264
      try { file.isFile && file.canRead && file.canExecute }
wenzelm@31818
   265
      catch { case _: SecurityException => false }
wenzelm@34200
   266
    } match {
wenzelm@31818
   267
      case Some(dir) =>
wenzelm@34201
   268
        Standard_System.process_output(
wenzelm@34195
   269
          execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
wenzelm@31818
   270
      case None => ("Unknown Isabelle tool: " + name, 2)
wenzelm@31818
   271
    }
wenzelm@28063
   272
  }
wenzelm@28063
   273
wenzelm@28063
   274
wenzelm@28063
   275
  /* named pipes */
wenzelm@28063
   276
wenzelm@31498
   277
  def mk_fifo(): String =
wenzelm@31498
   278
  {
wenzelm@28496
   279
    val (result, rc) = isabelle_tool("mkfifo")
wenzelm@28063
   280
    if (rc == 0) result.trim
wenzelm@28063
   281
    else error(result)
wenzelm@28063
   282
  }
wenzelm@28063
   283
wenzelm@31498
   284
  def rm_fifo(fifo: String)
wenzelm@31498
   285
  {
wenzelm@28496
   286
    val (result, rc) = isabelle_tool("rmfifo", fifo)
wenzelm@28063
   287
    if (rc != 0) error(result)
wenzelm@28063
   288
  }
wenzelm@28063
   289
wenzelm@34100
   290
  def fifo_stream(fifo: String): BufferedInputStream =
wenzelm@31498
   291
  {
wenzelm@29177
   292
    // blocks until writer is ready
wenzelm@29177
   293
    val stream =
wenzelm@34194
   294
      if (Platform.is_windows) {
wenzelm@34194
   295
        val proc = execute(false, "cat", fifo)
wenzelm@34194
   296
        proc.getOutputStream.close
wenzelm@34194
   297
        proc.getErrorStream.close
wenzelm@34194
   298
        proc.getInputStream
wenzelm@34194
   299
      }
wenzelm@29177
   300
      else new FileInputStream(fifo)
wenzelm@34100
   301
    new BufferedInputStream(stream)
wenzelm@29177
   302
  }
wenzelm@28063
   303
wenzelm@29152
   304
wenzelm@32450
   305
wenzelm@31796
   306
  /** Isabelle resources **/
wenzelm@31796
   307
wenzelm@32328
   308
  /* components */
wenzelm@32328
   309
wenzelm@32328
   310
  def components(): List[String] =
wenzelm@37058
   311
    getenv_strict("ISABELLE_COMPONENTS").split(":").toList
wenzelm@32328
   312
wenzelm@32328
   313
wenzelm@29152
   314
  /* find logics */
wenzelm@29152
   315
wenzelm@31498
   316
  def find_logics(): List[String] =
wenzelm@31498
   317
  {
wenzelm@29152
   318
    val ml_ident = getenv_strict("ML_IDENTIFIER")
wenzelm@34163
   319
    val logics = new mutable.ListBuffer[String]
wenzelm@29152
   320
    for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
wenzelm@29152
   321
      val files = platform_file(dir + "/" + ml_ident).listFiles()
wenzelm@29152
   322
      if (files != null) {
wenzelm@29152
   323
        for (file <- files if file.isFile) logics += file.getName
wenzelm@29152
   324
      }
wenzelm@29152
   325
    }
wenzelm@36012
   326
    logics.toList.sortWith(_ < _)
wenzelm@29152
   327
  }
wenzelm@29570
   328
wenzelm@29570
   329
wenzelm@29570
   330
  /* symbols */
wenzelm@29570
   331
wenzelm@29570
   332
  val symbols = new Symbol.Interpretation(
wenzelm@37058
   333
    try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
wenzelm@34024
   334
wenzelm@34024
   335
wenzelm@34024
   336
  /* fonts */
wenzelm@34024
   337
wenzelm@37058
   338
  val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
wenzelm@34024
   339
wenzelm@36788
   340
  def get_font(size: Int = 1, bold: Boolean = false): Font =
wenzelm@36785
   341
    new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
wenzelm@34024
   342
wenzelm@34044
   343
  def install_fonts()
wenzelm@34044
   344
  {
wenzelm@35006
   345
    def create_font(bold: Boolean): Font =
wenzelm@35006
   346
    {
wenzelm@35006
   347
      val name =
wenzelm@35006
   348
        if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
wenzelm@35006
   349
        else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
wenzelm@35006
   350
      Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
wenzelm@35006
   351
    }
wenzelm@36788
   352
    def check_font() = get_font().getFamily == font_family
wenzelm@35006
   353
wenzelm@34044
   354
    if (!check_font()) {
wenzelm@35006
   355
      val font = create_font(false)
wenzelm@35006
   356
      val bold_font = create_font(true)
wenzelm@35006
   357
wenzelm@34044
   358
      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
wenzelm@35006
   359
      ge.registerFont(font)
wenzelm@35006
   360
      // workaround strange problem with Apple's Java 1.6 font manager
wenzelm@37058
   361
      // FIXME does not quite work!?
wenzelm@35006
   362
      if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
wenzelm@35006
   363
      if (!check_font()) error("Failed to install IsabelleText fonts")
wenzelm@34044
   364
    }
wenzelm@34024
   365
  }
wenzelm@27919
   366
}