src/Pure/System/isabelle_system.scala
author wenzelm
Mon Oct 03 16:50:29 2016 +0200 (2016-10-03)
changeset 64021 1e23caac8757
parent 63687 1134ee401b20
child 64139 387c811cad6a
permissions -rw-r--r--
basic setup for Admin/build_history -- outside of Isabelle environment;
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@62610
    54
  def settings(): Map[String, String] =
wenzelm@50652
    55
  {
wenzelm@50652
    56
    if (_settings.isEmpty) init()  // unsynchronized check
wenzelm@62610
    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@62610
   115
          val (output, rc) = process_output(process(cmd1 ::: cmd2, env = env, redirect = true))
wenzelm@51820
   116
          if (rc != 0) error(output)
wenzelm@56477
   117
wenzelm@51820
   118
          val entries =
wenzelm@62610
   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@62304
   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@62614
   147
  def library_path(env: Map[String, String], elem: String): Map[String, String] =
wenzelm@62614
   148
    if (Platform.is_windows) env
wenzelm@62614
   149
    else {
wenzelm@62614
   150
      val x = if (Platform.is_macos) "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"
wenzelm@62614
   151
      env.getOrElse(x, "") match {
wenzelm@62614
   152
        case "" => env + (x -> elem)
wenzelm@62614
   153
        case y => env + (x -> (y + ":" + elem))
wenzelm@62614
   154
      }
wenzelm@62614
   155
    }
wenzelm@62614
   156
wenzelm@31796
   157
wenzelm@54039
   158
wenzelm@43606
   159
  /** file-system operations **/
wenzelm@31796
   160
wenzelm@48923
   161
  /* source files of Isabelle/ML bootstrap */
wenzelm@31436
   162
wenzelm@48923
   163
  def source_file(path: Path): Option[Path] =
wenzelm@31498
   164
  {
wenzelm@48923
   165
    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
wenzelm@48923
   166
wenzelm@48923
   167
    if (path.is_absolute || path.is_current) check(path)
wenzelm@31436
   168
    else {
wenzelm@48923
   169
      check(Path.explode("~~/src/Pure") + path) orElse
wenzelm@55876
   170
        (if (getenv("ML_SOURCES") == "") None
wenzelm@55876
   171
         else check(Path.explode("$ML_SOURCES") + path))
wenzelm@31436
   172
    }
wenzelm@31436
   173
  }
wenzelm@31436
   174
wenzelm@31436
   175
wenzelm@50893
   176
  /* mkdirs */
wenzelm@50893
   177
wenzelm@60013
   178
  def mkdirs(path: Path): Unit =
wenzelm@60263
   179
    if (!path.is_dir) {
wenzelm@62545
   180
      bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"")
wenzelm@60988
   181
      if (!path.is_dir) error("Failed to create directory: " + quote(File.platform_path(path)))
wenzelm@60263
   182
    }
wenzelm@50893
   183
wenzelm@50893
   184
wenzelm@56428
   185
  /* tmp files */
wenzelm@56428
   186
wenzelm@56428
   187
  private def isabelle_tmp_prefix(): JFile =
wenzelm@56428
   188
  {
wenzelm@56428
   189
    val path = Path.explode("$ISABELLE_TMP_PREFIX")
wenzelm@60013
   190
    path.file.mkdirs  // low-level mkdirs
wenzelm@60988
   191
    File.platform_file(path)
wenzelm@56428
   192
  }
wenzelm@56428
   193
wenzelm@63687
   194
  def tmp_file(name: String, ext: String = ""): JFile =
wenzelm@56428
   195
  {
wenzelm@56428
   196
    val suffix = if (ext == "") "" else "." + ext
wenzelm@56428
   197
    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
wenzelm@56428
   198
    file.deleteOnExit
wenzelm@56428
   199
    file
wenzelm@56428
   200
  }
wenzelm@56428
   201
wenzelm@56428
   202
  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
wenzelm@56428
   203
  {
wenzelm@56428
   204
    val file = tmp_file(name, ext)
wenzelm@56428
   205
    try { body(file) } finally { file.delete }
wenzelm@56428
   206
  }
wenzelm@56428
   207
wenzelm@56428
   208
wenzelm@56477
   209
  /* tmp dirs */
wenzelm@56477
   210
wenzelm@56477
   211
  def rm_tree(root: JFile)
wenzelm@56477
   212
  {
wenzelm@56477
   213
    root.delete
wenzelm@56477
   214
    if (root.isDirectory) {
wenzelm@56477
   215
      Files.walkFileTree(root.toPath,
wenzelm@56477
   216
        new SimpleFileVisitor[JPath] {
wenzelm@56477
   217
          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
wenzelm@56477
   218
          {
wenzelm@56477
   219
            Files.delete(file)
wenzelm@56477
   220
            FileVisitResult.CONTINUE
wenzelm@56477
   221
          }
wenzelm@56477
   222
wenzelm@56477
   223
          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
wenzelm@56477
   224
          {
wenzelm@56477
   225
            if (e == null) {
wenzelm@56477
   226
              Files.delete(dir)
wenzelm@56477
   227
              FileVisitResult.CONTINUE
wenzelm@56477
   228
            }
wenzelm@56477
   229
            else throw e
wenzelm@56477
   230
          }
wenzelm@56477
   231
        }
wenzelm@56477
   232
      )
wenzelm@56477
   233
    }
wenzelm@56477
   234
  }
wenzelm@56477
   235
wenzelm@56477
   236
  def tmp_dir(name: String): JFile =
wenzelm@56477
   237
  {
wenzelm@56477
   238
    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
wenzelm@56477
   239
    dir.deleteOnExit
wenzelm@56477
   240
    dir
wenzelm@56477
   241
  }
wenzelm@56477
   242
wenzelm@56477
   243
  def with_tmp_dir[A](name: String)(body: JFile => A): A =
wenzelm@56477
   244
  {
wenzelm@56477
   245
    val dir = tmp_dir(name)
wenzelm@56477
   246
    try { body(dir) } finally { rm_tree(dir) }
wenzelm@56477
   247
  }
wenzelm@56477
   248
wenzelm@56477
   249
wenzelm@62613
   250
wenzelm@62613
   251
  /** external processes **/
wenzelm@62613
   252
wenzelm@62613
   253
  /* raw process */
wenzelm@62613
   254
wenzelm@62613
   255
  def process(command_line: List[String],
wenzelm@62613
   256
    cwd: JFile = null,
wenzelm@62613
   257
    env: Map[String, String] = settings(),
wenzelm@62613
   258
    redirect: Boolean = false): Process =
wenzelm@62613
   259
  {
wenzelm@62613
   260
    val proc = new ProcessBuilder
wenzelm@62613
   261
    proc.command(command_line:_*)  // fragile on Windows
wenzelm@62613
   262
    if (cwd != null) proc.directory(cwd)
wenzelm@64021
   263
    if (env != null) {
wenzelm@64021
   264
      proc.environment.clear
wenzelm@64021
   265
      for ((x, y) <- env) proc.environment.put(x, y)
wenzelm@64021
   266
    }
wenzelm@62613
   267
    proc.redirectErrorStream(redirect)
wenzelm@62613
   268
    proc.start
wenzelm@62613
   269
  }
wenzelm@62613
   270
wenzelm@62613
   271
  def process_output(proc: Process): (String, Int) =
wenzelm@62613
   272
  {
wenzelm@62613
   273
    proc.getOutputStream.close
wenzelm@62613
   274
wenzelm@62613
   275
    val output = File.read_stream(proc.getInputStream)
wenzelm@62613
   276
    val rc =
wenzelm@62613
   277
      try { proc.waitFor }
wenzelm@62613
   278
      finally {
wenzelm@62613
   279
        proc.getInputStream.close
wenzelm@62613
   280
        proc.getErrorStream.close
wenzelm@62613
   281
        proc.destroy
wenzelm@62613
   282
        Thread.interrupted
wenzelm@62613
   283
      }
wenzelm@62613
   284
    (output, rc)
wenzelm@62613
   285
  }
wenzelm@61025
   286
wenzelm@61025
   287
  def kill(signal: String, group_pid: String): (String, Int) =
wenzelm@61025
   288
  {
wenzelm@61025
   289
    val bash =
wenzelm@61291
   290
      if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
wenzelm@61025
   291
      else List("/usr/bin/env", "bash")
wenzelm@62610
   292
    process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
wenzelm@61025
   293
  }
wenzelm@61025
   294
wenzelm@61025
   295
wenzelm@62613
   296
  /* GNU bash */
wenzelm@31796
   297
wenzelm@62610
   298
  def bash(script: String,
wenzelm@62610
   299
    cwd: JFile = null,
wenzelm@62610
   300
    env: Map[String, String] = settings(),
wenzelm@62610
   301
    redirect: Boolean = false,
wenzelm@51962
   302
    progress_stdout: String => Unit = (_: String) => (),
wenzelm@51962
   303
    progress_stderr: String => Unit = (_: String) => (),
wenzelm@56871
   304
    progress_limit: Option[Long] = None,
wenzelm@62602
   305
    strict: Boolean = true,
wenzelm@62602
   306
    cleanup: () => Unit = () => ()): Process_Result =
wenzelm@34198
   307
  {
wenzelm@62610
   308
    Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
wenzelm@62602
   309
      result(progress_stdout, progress_stderr, progress_limit, strict)
wenzelm@34198
   310
  }
wenzelm@34198
   311
wenzelm@54690
   312
  def open(arg: String): Unit =
wenzelm@62616
   313
    bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
wenzelm@54690
   314
wenzelm@54690
   315
  def pdf_viewer(arg: Path): Unit =
wenzelm@62616
   316
    bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
wenzelm@54690
   317
wenzelm@62615
   318
  def hg(cmd_line: String, cwd: JFile = null): Process_Result =
wenzelm@62615
   319
    bash("\"${HG:-hg}\" " + cmd_line, cwd = cwd)
wenzelm@28063
   320
wenzelm@32450
   321
wenzelm@62400
   322
wenzelm@31796
   323
  /** Isabelle resources **/
wenzelm@31796
   324
wenzelm@32328
   325
  /* components */
wenzelm@32328
   326
wenzelm@43669
   327
  def components(): List[Path] =
wenzelm@43669
   328
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
wenzelm@32328
   329
wenzelm@32328
   330
wenzelm@62633
   331
  /* default logic */
wenzelm@48503
   332
wenzelm@50403
   333
  def default_logic(args: String*): String =
wenzelm@50403
   334
  {
wenzelm@50403
   335
    args.find(_ != "") match {
wenzelm@50403
   336
      case Some(logic) => logic
wenzelm@50403
   337
      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
wenzelm@50403
   338
    }
wenzelm@50403
   339
  }
wenzelm@27919
   340
}