src/Pure/Tools/ml_process.scala
author wenzelm
Thu, 10 Mar 2016 10:07:23 +0100
changeset 62586 a522a5692832
parent 62577 src/Pure/System/ml_process.scala@7e2aa1d67dd8
child 62588 cd266473b81b
permissions -rw-r--r--
clarified modules;
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,
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    21
    env: Map[String, String] = Map.empty,
62557
a4ea3a222e0e tuned signature;
wenzelm
parents: 62556
diff changeset
    22
    redirect: Boolean = false,
62564
40624a9e94c4 tuned signature;
wenzelm
parents: 62563
diff changeset
    23
    channel: Option[System_Channel] = None): Bash.Process =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    24
  {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    25
    val load_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    26
    {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    27
      if (heap == "RAW_ML_SYSTEM") Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    28
      else if (heap.iterator.contains('/')) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    29
        val heap_path = Path.explode(heap)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    30
        if (!heap_path.is_file) error("Bad heap file: " + heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    31
        List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    32
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    33
      else {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    34
        val dirs = Isabelle_System.find_logics_dirs()
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    35
        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
    36
        dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    37
          case Some(heap_path) => List(heap_path)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    38
          case None =>
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    39
            error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    40
              cat_lines(dirs.map(dir => "  " + dir.implode)))
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    41
        }
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
    val eval_heaps =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    46
      load_heaps.map(load_heap =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    47
        "(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
    48
        "; 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
    49
        ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    50
        "); OS.Process.exit OS.Process.failure)")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    51
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    52
    val eval_initial =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    53
      if (load_heaps.isEmpty) {
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    54
        List(
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    55
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    56
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    57
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    58
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    59
          else
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    60
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    61
          "PolyML.Compiler.prompt1 := \"ML> \"",
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    62
          "PolyML.Compiler.prompt2 := \"ML# \"")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    63
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    64
      else Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    65
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    66
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    67
      if (modes.isEmpty) Nil
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
      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
    69
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    70
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    71
    val isabelle_process_options = Isabelle_System.tmp_file("options")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    72
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    73
    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
62547
b33dea503665 clarified RAW_ML_SYSTEM;
wenzelm
parents: 62546
diff changeset
    74
    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
    75
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    76
    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
    77
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    78
    val eval_process =
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    79
      if (load_heaps.isEmpty)
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    80
        List("PolyML.print_depth 10")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    81
      else
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    82
        channel match {
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    83
          case None =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    84
            List("(default_print_depth 10; Isabelle_Process.init_options ())")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    85
          case Some(ch) =>
62576
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    86
            List("(default_print_depth 10; Isabelle_Process.init_protocol " +
26179aa33fe7 more careful print_depth on startup;
wenzelm
parents: 62573
diff changeset
    87
              ML_Syntax.print_string_raw(ch.server_name) + ")")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    88
        }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    89
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
    90
    // 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
    91
    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
    92
      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    93
      (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
    94
        map(eval => List("--eval", eval)).flatten ::: args
62546
wenzelm
parents: 62545
diff changeset
    95
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    96
    Bash.process(
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    97
      """
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    98
        [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    99
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   100
        export ISABELLE_PID="$$"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   101
        export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   102
        mkdir -p "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   103
        chmod $(umask -S) "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   104
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   105
        librarypath "$ML_HOME"
62577
7e2aa1d67dd8 clarified interactive mode, which is relevant for ML prompts;
wenzelm
parents: 62576
diff changeset
   106
        "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   107
        RC="$?"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   108
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   109
        rm -f "$ISABELLE_PROCESS_OPTIONS"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   110
        rmdir "$ISABELLE_TMP"
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   111
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   112
        exit "$RC"
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
   113
      """, cwd = cwd, env = env ++ env_options, redirect = redirect)
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   114
  }
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   115
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   116
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   117
  /* command line entry point */
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   118
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   119
  def main(args: Array[String])
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   120
  {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   121
    Command_Line.tool {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   122
      var eval_args: List[String] = Nil
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   123
      var modes: List[String] = Nil
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   124
      var options = Options.init()
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   125
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   126
      val getopts = Getopts("""
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   127
Usage: isabelle_process [OPTIONS] [HEAP]
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   128
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   129
  Options are:
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   130
    -e ML_EXPR   evaluate ML expression on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   131
    -f ML_FILE   evaluate ML file on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   132
    -m MODE      add print mode for output
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   133
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   134
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   135
  If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   136
  $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   137
  if it is RAW_ML_SYSTEM, the initial ML heap is used.
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   138
""",
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   139
        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   140
        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   141
        "m:" -> (arg => modes = arg :: modes),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   142
        "o:" -> (arg => options = options + arg))
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   143
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   144
      val heap =
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   145
        getopts(args) match {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   146
          case Nil => ""
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   147
          case List(heap) => heap
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   148
          case _ => getopts.usage()
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   149
        }
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   150
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   151
      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   152
        result().print_stdout.rc
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   153
    }
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   154
  }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   155
}