src/Pure/Tools/ml_process.scala
author wenzelm
Sun, 13 Mar 2016 13:04:50 +0100
changeset 62614 0a01bc7f0946
parent 62610 4c89504c76fb
child 62629 1815513a57f1
permissions -rw-r--r--
prefer Scala over bash function;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
     1
/*  Title:      Pure/Tools/ml_process.scala
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     3
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
     4
The raw ML process.
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     5
*/
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     6
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     8
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
     9
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    10
import java.io.{File => JFile}
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    11
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    12
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    13
object ML_Process
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    14
{
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    15
  def apply(options: Options,
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    16
    heap: String = "",
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    17
    args: List[String] = Nil,
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    18
    modes: List[String] = Nil,
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    19
    secure: Boolean = false,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    20
    cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62606
diff changeset
    21
    env: Map[String, String] = Isabelle_System.settings(),
62557
a4ea3a222e0e tuned signature;
wenzelm
parents: 62556
diff changeset
    22
    redirect: Boolean = false,
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
    23
    cleanup: () => Unit = () => (),
62564
40624a9e94c4 tuned signature;
wenzelm
parents: 62563
diff changeset
    24
    channel: Option[System_Channel] = None): Bash.Process =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    25
  {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    26
    val load_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    27
    {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    28
      if (heap == "RAW_ML_SYSTEM") Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    29
      else if (heap.iterator.contains('/')) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    30
        val heap_path = Path.explode(heap)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    31
        if (!heap_path.is_file) error("Bad heap file: " + heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    32
        List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    33
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    34
      else {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    35
        val dirs = Isabelle_System.find_logics_dirs()
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    36
        val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    37
        dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    38
          case Some(heap_path) => List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    39
          case None =>
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
    40
            error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" +
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    41
              cat_lines(dirs.map(dir => "  " + dir.implode)))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    42
        }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    43
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    44
    }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    45
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    46
    val eval_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    47
      load_heaps.map(load_heap =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    48
        "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) +
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    49
        "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    50
        ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    51
        "); OS.Process.exit OS.Process.failure)")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    52
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    53
    val eval_initial =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    54
      if (load_heaps.isEmpty) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    55
        List(
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    56
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    57
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    58
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    59
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    60
          else
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    61
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    62
          "PolyML.Compiler.prompt1 := \"ML> \"",
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    63
          "PolyML.Compiler.prompt2 := \"ML# \"")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    64
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    65
      else Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    66
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    67
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
      if (modes.isEmpty) Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    69
      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    70
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    71
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    72
    val isabelle_process_options = Isabelle_System.tmp_file("options")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    73
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    74
    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
62547
b33dea503665 clarified RAW_ML_SYSTEM;
wenzelm
parents: 62546
diff changeset
    75
    val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    76
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    77
    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    78
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    79
    val eval_process =
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    80
      if (load_heaps.isEmpty)
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    81
        List("PolyML.print_depth 10")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    82
      else
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    83
        channel match {
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    84
          case None =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    85
            List("(default_print_depth 10; Isabelle_Process.init_options ())")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    86
          case Some(ch) =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    87
            List("(default_print_depth 10; Isabelle_Process.init_protocol " +
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    88
              ML_Syntax.print_string_raw(ch.server_name) + ")")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    89
        }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    90
62601
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    91
    // ISABELLE_TMP
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    92
    val isabelle_tmp = Isabelle_System.tmp_dir("process")
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    93
    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    94
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
    95
    // bash
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
    96
    val bash_args =
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
    97
      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    98
      (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62544
diff changeset
    99
        map(eval => List("--eval", eval)).flatten ::: args
62546
wenzelm
parents: 62545
diff changeset
   100
62614
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   101
    Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   102
      cwd = cwd,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   103
      env =
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   104
        Isabelle_System.library_path(env ++ env_options ++ env_tmp,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   105
          Isabelle_System.getenv_strict("ML_HOME")),
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
   106
      redirect = redirect,
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   107
      cleanup = () =>
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   108
        {
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   109
          isabelle_process_options.delete
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   110
          Isabelle_System.rm_tree(isabelle_tmp)
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
   111
          cleanup()
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   112
        })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   113
  }
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   114
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   115
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   116
  /* command line entry point */
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   117
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   118
  def main(args: Array[String])
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   119
  {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   120
    Command_Line.tool {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   121
      var eval_args: List[String] = Nil
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   122
      var modes: List[String] = Nil
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   123
      var options = Options.init()
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   124
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   125
      val getopts = Getopts("""
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   126
Usage: isabelle process [OPTIONS] [HEAP]
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   127
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   128
  Options are:
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   129
    -e ML_EXPR   evaluate ML expression on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   130
    -f ML_FILE   evaluate ML file on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   131
    -m MODE      add print mode for output
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   132
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   133
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   134
  Run the raw Isabelle ML process in batch mode, using a given heap image.
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   135
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   136
  If HEAP is a plain name (default ISABELLE_LOGIC=""" +
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   137
  quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   138
  ISABELLE_PATH; if it contains a slash, it is taken as literal file;
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   139
  if it is "RAW_ML_SYSTEM", the initial ML heap is used.
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   140
""",
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   141
        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   142
        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   143
        "m:" -> (arg => modes = arg :: modes),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   144
        "o:" -> (arg => options = options + arg))
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   145
62588
cd266473b81b isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents: 62586
diff changeset
   146
      if (args.isEmpty) getopts.usage()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   147
      val heap =
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   148
        getopts(args) match {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   149
          case Nil => ""
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   150
          case List(heap) => heap
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   151
          case _ => getopts.usage()
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   152
        }
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   153
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   154
      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   155
        result().print_stdout.rc
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   156
    }
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   157
  }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   158
}