src/Pure/System/isabelle_system.scala
author wenzelm
Tue Nov 03 16:35:38 2015 +0100 (2015-11-03)
changeset 61559 313eca3fa847
parent 61556 0d4ee4168e41
child 62291 98df25a6e2ac
permissions -rw-r--r--
more direct task future implementation, with proper cancel operation;
more uniform Future.thread;
wenzelm@30175
     1
/*  Title:      Pure/System/isabelle_system.scala
wenzelm@27919
     2
    Author:     Makarius
wenzelm@27919
     3
wenzelm@43695
     4
Fundamental Isabelle system environment: quasi-static module with
wenzelm@43695
     5
optional init operation.
wenzelm@27919
     6
*/
wenzelm@27919
     7
wenzelm@27919
     8
package isabelle
wenzelm@27919
     9
wenzelm@55618
    10
wenzelm@61281
    11
import java.io.{File => JFile, IOException, BufferedReader, InputStreamReader}
wenzelm@56477
    12
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
wenzelm@56477
    13
import java.nio.file.attribute.BasicFileAttributes
wenzelm@27936
    14
wenzelm@61281
    15
import scala.collection.mutable
wenzelm@61281
    16
wenzelm@27919
    17
wenzelm@43514
    18
object Isabelle_System
wenzelm@43514
    19
{
wenzelm@50652
    20
  /** bootstrap information **/
wenzelm@43661
    21
wenzelm@50652
    22
  def jdk_home(): String =
wenzelm@43661
    23
  {
wenzelm@53582
    24
    val java_home = System.getProperty("java.home", "")
wenzelm@50652
    25
    val home = new JFile(java_home)
wenzelm@50652
    26
    val parent = home.getParent
wenzelm@50652
    27
    if (home.getName == "jre" && parent != null &&
wenzelm@50652
    28
        (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
wenzelm@50652
    29
    else java_home
wenzelm@43661
    30
  }
wenzelm@37013
    31
wenzelm@61291
    32
  def bootstrap_directory(
wenzelm@61291
    33
    preference: String, envar: String, property: String, description: String): String =
wenzelm@50652
    34
  {
wenzelm@61291
    35
    def check(s: String): Option[String] =
wenzelm@61291
    36
      if (s != null && s != "") Some(s) else None
wenzelm@50652
    37
wenzelm@61291
    38
    val value =
wenzelm@61291
    39
      check(preference) orElse  // explicit argument
wenzelm@61291
    40
      check(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
wenzelm@61291
    41
      check(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
wenzelm@61291
    42
      error("Unknown " + description + " directory")
wenzelm@50652
    43
wenzelm@61291
    44
    if ((new JFile(value)).isDirectory) value
wenzelm@61291
    45
    else error("Bad " + description + " directory " + quote(value))
wenzelm@50652
    46
  }
wenzelm@50652
    47
wenzelm@50652
    48
wenzelm@50652
    49
wenzelm@50652
    50
  /** implicit settings environment **/
wenzelm@50652
    51
wenzelm@50652
    52
  @volatile private var _settings: Option[Map[String, String]] = None
wenzelm@50652
    53
wenzelm@50652
    54
  def settings(): Map[String, String] =
wenzelm@50652
    55
  {
wenzelm@50652
    56
    if (_settings.isEmpty) init()  // unsynchronized check
wenzelm@50652
    57
    _settings.get
wenzelm@50652
    58
  }
wenzelm@31796
    59
wenzelm@61293
    60
  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
wenzelm@50652
    61
    if (_settings.isEmpty) {
wenzelm@43661
    62
      import scala.collection.JavaConversions._
wenzelm@37013
    63
wenzelm@61293
    64
      val isabelle_root1 =
wenzelm@61293
    65
        bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
wenzelm@61291
    66
wenzelm@61291
    67
      val cygwin_root1 =
wenzelm@61291
    68
        if (Platform.is_windows)
wenzelm@61291
    69
          bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
wenzelm@61291
    70
        else ""
wenzelm@61291
    71
wenzelm@61295
    72
      if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
wenzelm@61295
    73
wenzelm@51820
    74
      def set_cygwin_root()
wenzelm@43661
    75
      {
wenzelm@51820
    76
        if (Platform.is_windows)
wenzelm@61291
    77
          _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
wenzelm@51820
    78
      }
wenzelm@47725
    79
wenzelm@51820
    80
      set_cygwin_root()
wenzelm@57411
    81
wenzelm@58640
    82
      def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
wenzelm@58640
    83
        if (env.isDefinedAt(entry._1) || entry._2 == "") env
wenzelm@58640
    84
        else env + entry
wenzelm@58640
    85
wenzelm@57411
    86
      val env =
wenzelm@57411
    87
      {
wenzelm@58640
    88
        val temp_windows =
wenzelm@58640
    89
        {
wenzelm@61291
    90
          val temp = if (Platform.is_windows) System.getenv("TEMP") else null
wenzelm@58640
    91
          if (temp != null && temp.contains('\\')) temp else ""
wenzelm@58640
    92
        }
wenzelm@57411
    93
        val user_home = System.getProperty("user.home", "")
wenzelm@57411
    94
        val isabelle_app = System.getProperty("isabelle.app", "")
wenzelm@51820
    95
wenzelm@58640
    96
        default(
wenzelm@58640
    97
          default(
wenzelm@60992
    98
            default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
wenzelm@60215
    99
              "TEMP_WINDOWS" -> temp_windows),
wenzelm@60215
   100
            "HOME" -> user_home),
wenzelm@60215
   101
          "ISABELLE_APP" -> "true")
wenzelm@57411
   102
      }
wenzelm@29177
   103
wenzelm@51820
   104
      val settings =
wenzelm@56428
   105
      {
wenzelm@56428
   106
        val dump = JFile.createTempFile("settings", null)
wenzelm@56428
   107
        dump.deleteOnExit
wenzelm@56428
   108
        try {
wenzelm@61293
   109
          val cmd1 =
wenzelm@61291
   110
            if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l") else Nil
wenzelm@61293
   111
          val cmd2 =
wenzelm@61293
   112
            List(isabelle_root1 + JFile.separator + "bin" + JFile.separator + "isabelle",
wenzelm@61293
   113
              "getenv", "-d", dump.toString)
wenzelm@61293
   114
wenzelm@61293
   115
          val (output, rc) = process_output(raw_execute(null, env, true, (cmd1 ::: cmd2): _*))
wenzelm@51820
   116
          if (rc != 0) error(output)
wenzelm@56477
   117
wenzelm@51820
   118
          val entries =
wenzelm@56661
   119
            (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
wenzelm@51820
   120
              val i = entry.indexOf('=')
wenzelm@60215
   121
              if (i <= 0) entry -> ""
wenzelm@60215
   122
              else entry.substring(0, i) -> entry.substring(i + 1)
wenzelm@51820
   123
            }).toMap
wenzelm@51820
   124
          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
wenzelm@51820
   125
        }
wenzelm@56428
   126
        finally { dump.delete }
wenzelm@56428
   127
      }
wenzelm@50652
   128
      _settings = Some(settings)
wenzelm@51820
   129
      set_cygwin_root()
wenzelm@43661
   130
    }
wenzelm@27953
   131
  }
wenzelm@27919
   132
wenzelm@31796
   133
wenzelm@31796
   134
  /* getenv */
wenzelm@31796
   135
wenzelm@47661
   136
  def getenv(name: String): String = settings.getOrElse(name, "")
wenzelm@31498
   137
wenzelm@31498
   138
  def getenv_strict(name: String): String =
wenzelm@31498
   139
  {
wenzelm@31234
   140
    val value = getenv(name)
wenzelm@60196
   141
    if (value != "") value
wenzelm@60196
   142
    else error("Undefined Isabelle environment variable: " + quote(name))
wenzelm@27919
   143
  }
wenzelm@27919
   144
wenzelm@61291
   145
  def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
wenzelm@51820
   146
wenzelm@31796
   147
wenzelm@54039
   148
wenzelm@43606
   149
  /** file-system operations **/
wenzelm@31796
   150
wenzelm@48923
   151
  /* source files of Isabelle/ML bootstrap */
wenzelm@31436
   152
wenzelm@48923
   153
  def source_file(path: Path): Option[Path] =
wenzelm@31498
   154
  {
wenzelm@48923
   155
    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
wenzelm@48923
   156
wenzelm@48923
   157
    if (path.is_absolute || path.is_current) check(path)
wenzelm@31436
   158
    else {
wenzelm@48923
   159
      check(Path.explode("~~/src/Pure") + path) orElse
wenzelm@55876
   160
        (if (getenv("ML_SOURCES") == "") None
wenzelm@55876
   161
         else check(Path.explode("$ML_SOURCES") + path))
wenzelm@31436
   162
    }
wenzelm@31436
   163
  }
wenzelm@31436
   164
wenzelm@31436
   165
wenzelm@50893
   166
  /* mkdirs */
wenzelm@50893
   167
wenzelm@60013
   168
  def mkdirs(path: Path): Unit =
wenzelm@60263
   169
    if (!path.is_dir) {
wenzelm@60988
   170
      bash("perl -e \"use File::Path make_path; make_path(" + File.shell_path(path) + ");\"")
wenzelm@60988
   171
      if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
wenzelm@60263
   172
    }
wenzelm@50893
   173
wenzelm@50893
   174
wenzelm@32450
   175
wenzelm@39583
   176
  /** external processes **/
wenzelm@39583
   177
wenzelm@50651
   178
  /* raw execute for bootstrapping */
wenzelm@50651
   179
wenzelm@52667
   180
  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
wenzelm@50651
   181
  {
wenzelm@50651
   182
    val cmdline = new java.util.LinkedList[String]
wenzelm@50651
   183
    for (s <- args) cmdline.add(s)
wenzelm@50651
   184
wenzelm@50651
   185
    val proc = new ProcessBuilder(cmdline)
wenzelm@50651
   186
    if (cwd != null) proc.directory(cwd)
wenzelm@50651
   187
    if (env != null) {
wenzelm@50651
   188
      proc.environment.clear
wenzelm@50651
   189
      for ((x, y) <- env) proc.environment.put(x, y)
wenzelm@50651
   190
    }
wenzelm@50651
   191
    proc.redirectErrorStream(redirect)
wenzelm@50651
   192
    proc.start
wenzelm@50651
   193
  }
wenzelm@50651
   194
wenzelm@61282
   195
  def process_output(proc: Process): (String, Int) =
wenzelm@50651
   196
  {
wenzelm@50651
   197
    proc.getOutputStream.close
wenzelm@61281
   198
wenzelm@61282
   199
    val output = File.read_stream(proc.getInputStream)
wenzelm@50651
   200
    val rc =
wenzelm@50651
   201
      try { proc.waitFor }
wenzelm@50651
   202
      finally {
wenzelm@50651
   203
        proc.getInputStream.close
wenzelm@50651
   204
        proc.getErrorStream.close
wenzelm@50651
   205
        proc.destroy
wenzelm@50651
   206
        Thread.interrupted
wenzelm@50651
   207
      }
wenzelm@50651
   208
    (output, rc)
wenzelm@50651
   209
  }
wenzelm@50651
   210
wenzelm@50651
   211
wenzelm@39583
   212
  /* plain execute */
wenzelm@39583
   213
wenzelm@48409
   214
  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
wenzelm@39583
   215
  {
wenzelm@39583
   216
    val cmdline =
wenzelm@61291
   217
      if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ::: args.toList
wenzelm@39583
   218
      else args
wenzelm@48353
   219
    val env1 = if (env == null) settings else settings ++ env
wenzelm@50651
   220
    raw_execute(cwd, env1, redirect, cmdline: _*)
wenzelm@39583
   221
  }
wenzelm@39583
   222
wenzelm@48353
   223
  def execute(redirect: Boolean, args: String*): Process =
wenzelm@48353
   224
    execute_env(null, null, redirect, args: _*)
wenzelm@48353
   225
wenzelm@39583
   226
wenzelm@56428
   227
  /* tmp files */
wenzelm@56428
   228
wenzelm@56428
   229
  private def isabelle_tmp_prefix(): JFile =
wenzelm@56428
   230
  {
wenzelm@56428
   231
    val path = Path.explode("$ISABELLE_TMP_PREFIX")
wenzelm@60013
   232
    path.file.mkdirs  // low-level mkdirs
wenzelm@60988
   233
    File.platform_file(path)
wenzelm@56428
   234
  }
wenzelm@56428
   235
wenzelm@56428
   236
  def tmp_file[A](name: String, ext: String = ""): JFile =
wenzelm@56428
   237
  {
wenzelm@56428
   238
    val suffix = if (ext == "") "" else "." + ext
wenzelm@56428
   239
    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
wenzelm@56428
   240
    file.deleteOnExit
wenzelm@56428
   241
    file
wenzelm@56428
   242
  }
wenzelm@56428
   243
wenzelm@56428
   244
  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
wenzelm@56428
   245
  {
wenzelm@56428
   246
    val file = tmp_file(name, ext)
wenzelm@56428
   247
    try { body(file) } finally { file.delete }
wenzelm@56428
   248
  }
wenzelm@56428
   249
wenzelm@56428
   250
wenzelm@56477
   251
  /* tmp dirs */
wenzelm@56477
   252
wenzelm@56477
   253
  def rm_tree(root: JFile)
wenzelm@56477
   254
  {
wenzelm@56477
   255
    root.delete
wenzelm@56477
   256
    if (root.isDirectory) {
wenzelm@56477
   257
      Files.walkFileTree(root.toPath,
wenzelm@56477
   258
        new SimpleFileVisitor[JPath] {
wenzelm@56477
   259
          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
wenzelm@56477
   260
          {
wenzelm@56477
   261
            Files.delete(file)
wenzelm@56477
   262
            FileVisitResult.CONTINUE
wenzelm@56477
   263
          }
wenzelm@56477
   264
wenzelm@56477
   265
          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
wenzelm@56477
   266
          {
wenzelm@56477
   267
            if (e == null) {
wenzelm@56477
   268
              Files.delete(dir)
wenzelm@56477
   269
              FileVisitResult.CONTINUE
wenzelm@56477
   270
            }
wenzelm@56477
   271
            else throw e
wenzelm@56477
   272
          }
wenzelm@56477
   273
        }
wenzelm@56477
   274
      )
wenzelm@56477
   275
    }
wenzelm@56477
   276
  }
wenzelm@56477
   277
wenzelm@56477
   278
  def tmp_dir(name: String): JFile =
wenzelm@56477
   279
  {
wenzelm@56477
   280
    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
wenzelm@56477
   281
    dir.deleteOnExit
wenzelm@56477
   282
    dir
wenzelm@56477
   283
  }
wenzelm@56477
   284
wenzelm@56477
   285
  def with_tmp_dir[A](name: String)(body: JFile => A): A =
wenzelm@56477
   286
  {
wenzelm@56477
   287
    val dir = tmp_dir(name)
wenzelm@56477
   288
    try { body(dir) } finally { rm_tree(dir) }
wenzelm@56477
   289
  }
wenzelm@56477
   290
wenzelm@56477
   291
wenzelm@61025
   292
  /* kill */
wenzelm@61025
   293
wenzelm@61025
   294
  def kill(signal: String, group_pid: String): (String, Int) =
wenzelm@61025
   295
  {
wenzelm@61025
   296
    val bash =
wenzelm@61291
   297
      if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
wenzelm@61025
   298
      else List("/usr/bin/env", "bash")
wenzelm@61025
   299
    val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
wenzelm@61282
   300
    process_output(raw_execute(null, null, true, cmdline: _*))
wenzelm@61025
   301
  }
wenzelm@61025
   302
wenzelm@61025
   303
wenzelm@39583
   304
  /* bash */
wenzelm@31796
   305
wenzelm@60991
   306
  private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])
wenzelm@56666
   307
  {
wenzelm@56666
   308
    private var count = 0L
wenzelm@56666
   309
    def apply(progress: String => Unit)(line: String): Unit = synchronized {
wenzelm@56666
   310
      progress(line)
wenzelm@56666
   311
      count = count + line.length + 1
wenzelm@56666
   312
      progress_limit match {
wenzelm@56666
   313
        case Some(limit) if count > limit => proc.terminate
wenzelm@56666
   314
        case _ =>
wenzelm@56666
   315
      }
wenzelm@56666
   316
    }
wenzelm@56666
   317
  }
wenzelm@56666
   318
wenzelm@50845
   319
  def bash_env(cwd: JFile, env: Map[String, String], script: String,
wenzelm@51962
   320
    progress_stdout: String => Unit = (_: String) => (),
wenzelm@51962
   321
    progress_stderr: String => Unit = (_: String) => (),
wenzelm@56871
   322
    progress_limit: Option[Long] = None,
wenzelm@60991
   323
    strict: Boolean = true): Bash.Result =
wenzelm@34198
   324
  {
wenzelm@56428
   325
    with_tmp_file("isabelle_script") { script_file =>
wenzelm@48411
   326
      File.write(script_file, script)
wenzelm@60992
   327
      val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file))
wenzelm@51962
   328
      proc.stdin.close
wenzelm@39581
   329
wenzelm@56666
   330
      val limited = new Limited_Progress(proc, progress_limit)
wenzelm@61559
   331
      val stdout =
wenzelm@61559
   332
        Future.thread("bash_stdout") { File.read_lines(proc.stdout, limited(progress_stdout)) }
wenzelm@61559
   333
      val stderr =
wenzelm@61559
   334
        Future.thread("bash_stderr") { File.read_lines(proc.stderr, limited(progress_stderr)) }
wenzelm@34198
   335
wenzelm@39581
   336
      val rc =
wenzelm@39583
   337
        try { proc.join }
wenzelm@56667
   338
        catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
wenzelm@56871
   339
      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
wenzelm@56871
   340
wenzelm@60991
   341
      Bash.Result(stdout.join, stderr.join, rc)
wenzelm@34198
   342
    }
wenzelm@34198
   343
  }
wenzelm@34198
   344
wenzelm@60991
   345
  def bash(script: String): Bash.Result = bash_env(null, null, script)
wenzelm@48353
   346
wenzelm@39583
   347
wenzelm@39583
   348
  /* system tools */
wenzelm@39583
   349
wenzelm@31818
   350
  def isabelle_tool(name: String, args: String*): (String, Int) =
wenzelm@31498
   351
  {
wenzelm@43669
   352
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
wenzelm@48373
   353
      val file = (dir + Path.basic(name)).file
wenzelm@42124
   354
      try {
wenzelm@42124
   355
        file.isFile && file.canRead && file.canExecute &&
wenzelm@42124
   356
          !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@42124
   357
      }
wenzelm@31818
   358
      catch { case _: SecurityException => false }
wenzelm@34200
   359
    } match {
wenzelm@31818
   360
      case Some(dir) =>
wenzelm@60988
   361
        val file = File.standard_path(dir + Path.basic(name))
wenzelm@61282
   362
        process_output(execute(true, (List(file) ::: args.toList): _*))
wenzelm@31818
   363
      case None => ("Unknown Isabelle tool: " + name, 2)
wenzelm@31818
   364
    }
wenzelm@28063
   365
  }
wenzelm@28063
   366
wenzelm@54690
   367
  def open(arg: String): Unit =
wenzelm@54690
   368
    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
wenzelm@54690
   369
wenzelm@54690
   370
  def pdf_viewer(arg: Path): Unit =
wenzelm@60988
   371
    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
wenzelm@54690
   372
wenzelm@60991
   373
  def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
wenzelm@60988
   374
    bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
wenzelm@28063
   375
wenzelm@32450
   376
wenzelm@31796
   377
  /** Isabelle resources **/
wenzelm@31796
   378
wenzelm@32328
   379
  /* components */
wenzelm@32328
   380
wenzelm@43669
   381
  def components(): List[Path] =
wenzelm@43669
   382
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
wenzelm@32328
   383
wenzelm@32328
   384
wenzelm@50403
   385
  /* logic images */
wenzelm@29152
   386
wenzelm@48503
   387
  def find_logics_dirs(): List[Path] =
wenzelm@31498
   388
  {
wenzelm@48503
   389
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm@48503
   390
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
wenzelm@29152
   391
  }
wenzelm@29570
   392
wenzelm@48503
   393
  def find_logics(): List[String] =
wenzelm@48503
   394
    (for {
wenzelm@48503
   395
      dir <- find_logics_dirs()
wenzelm@48503
   396
      files = dir.file.listFiles() if files != null
wenzelm@48503
   397
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm@48503
   398
wenzelm@50403
   399
  def default_logic(args: String*): String =
wenzelm@50403
   400
  {
wenzelm@50403
   401
    args.find(_ != "") match {
wenzelm@50403
   402
      case Some(logic) => logic
wenzelm@50403
   403
      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
wenzelm@50403
   404
    }
wenzelm@50403
   405
  }
wenzelm@27919
   406
}