src/Pure/Tools/ml_process.scala
author wenzelm
Fri, 18 Mar 2016 21:21:09 +0100
changeset 62672 068b430e678f
parent 62668 360d3464919c
child 62677 0df43889f496
permissions -rw-r--r--
clarified print depth;
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,
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    16
    logic: String = "",
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    17
    args: List[String] = Nil,
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    18
    dirs: List[Path] = Nil,
62556
c115e69f457f more abstract Session.start, without prover command-line;
wenzelm
parents: 62548
diff changeset
    19
    modes: List[String] = Nil,
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62639
diff changeset
    20
    raw_ml_system: Boolean = false,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    21
    cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62606
diff changeset
    22
    env: Map[String, String] = Isabelle_System.settings(),
62557
a4ea3a222e0e tuned signature;
wenzelm
parents: 62556
diff changeset
    23
    redirect: Boolean = false,
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
    24
    cleanup: () => Unit = () => (),
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62629
diff changeset
    25
    channel: Option[System_Channel] = None,
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    26
    tree: Option[Sessions.Tree] = None,
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62629
diff changeset
    27
    store: Sessions.Store = Sessions.store()): Bash.Process =
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    28
  {
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    29
    val logic_name = Isabelle_System.default_logic(logic)
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    30
    val heaps: List[String] =
62643
6f7ac44365d7 eliminated without magic name;
wenzelm
parents: 62639
diff changeset
    31
      if (raw_ml_system) Nil
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    32
      else {
62644
c36a4495ba5f pro-forma selection for improved error message;
wenzelm
parents: 62643
diff changeset
    33
        val (_, session_tree) =
c36a4495ba5f pro-forma selection for improved error message;
wenzelm
parents: 62643
diff changeset
    34
          tree.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    35
        (session_tree.ancestors(logic_name) ::: List(logic_name)).
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    36
          map(a => File.platform_path(store.heap(a)))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    37
      }
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    38
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    39
    val eval_init =
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    40
      if (heaps.isEmpty) {
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    41
        List(
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    42
          if (Platform.is_windows)
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    43
            "fun exit 0 = OS.Process.exit OS.Process.success" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    44
            " | exit 1 = OS.Process.exit OS.Process.failure" +
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    45
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
62560
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    46
          else
498f6ff16804 clarified initial ML;
wenzelm
parents: 62557
diff changeset
    47
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
62629
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    48
          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
1815513a57f1 clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents: 62614
diff changeset
    49
          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    50
      }
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    51
      else
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    52
        List(
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    53
          "(PolyML.SaveState.loadHierarchy " +
62638
751cf9f3d433 tuned signature;
wenzelm
parents: 62637
diff changeset
    54
            ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    55
          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
62638
751cf9f3d433 tuned signature;
wenzelm
parents: 62637
diff changeset
    56
          ML_Syntax.print_string0(": " + logic_name + "\n") +
62637
0189fe0f6452 support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents: 62634
diff changeset
    57
          "); OS.Process.exit OS.Process.failure)")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    58
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    59
    val eval_modes =
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    60
      if (modes.isEmpty) Nil
62638
751cf9f3d433 tuned signature;
wenzelm
parents: 62637
diff changeset
    61
      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    62
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    63
    // options
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    64
    val isabelle_process_options = Isabelle_System.tmp_file("options")
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    65
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62565
diff changeset
    66
    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    67
    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    68
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    69
    val eval_process =
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
    70
      if (heaps.isEmpty)
62672
068b430e678f clarified print depth;
wenzelm
parents: 62668
diff changeset
    71
        List("PolyML.print_depth 20")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    72
      else
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    73
        channel match {
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    74
          case None =>
62672
068b430e678f clarified print depth;
wenzelm
parents: 62668
diff changeset
    75
            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    76
          case Some(ch) =>
62672
068b430e678f clarified print depth;
wenzelm
parents: 62668
diff changeset
    77
            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " +
62638
751cf9f3d433 tuned signature;
wenzelm
parents: 62637
diff changeset
    78
              ML_Syntax.print_string0(ch.server_name) + ")")
62565
cd3ea66fe2ce proper support for RAW_ML_SYSTEM;
wenzelm
parents: 62564
diff changeset
    79
        }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
    80
62601
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    81
    // ISABELLE_TMP
a937889f0086 create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents: 62600
diff changeset
    82
    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
    83
    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
    84
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
    85
    // 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
    86
    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
    87
      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
62668
360d3464919c discontinued slightly odd "secure" mode;
wenzelm
parents: 62661
diff changeset
    88
      (eval_init ::: eval_modes ::: eval_options ::: 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
    89
        map(eval => List("--eval", eval)).flatten ::: args
62546
wenzelm
parents: 62545
diff changeset
    90
62614
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    91
    Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    92
      cwd = cwd,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    93
      env =
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    94
        Isabelle_System.library_path(env ++ env_options ++ env_tmp,
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    95
          Isabelle_System.getenv_strict("ML_HOME")),
0a01bc7f0946 prefer Scala over bash function;
wenzelm
parents: 62610
diff changeset
    96
      redirect = redirect,
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
    97
      cleanup = () =>
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
    98
        {
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
    99
          isabelle_process_options.delete
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   100
          Isabelle_System.rm_tree(isabelle_tmp)
62603
c077eb5e0b56 clarified cleanup;
wenzelm
parents: 62602
diff changeset
   101
          cleanup()
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62601
diff changeset
   102
        })
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   103
  }
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   104
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   105
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   106
  /* command line entry point */
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   107
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   108
  def main(args: Array[String])
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   109
  {
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   110
    Command_Line.tool {
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   111
      var dirs: List[Path] = Nil
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   112
      var eval_args: List[String] = Nil
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   113
      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   114
      var modes: List[String] = Nil
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   115
      var options = Options.init()
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   116
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   117
      val getopts = Getopts("""
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   118
Usage: isabelle process [OPTIONS]
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   119
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   120
  Options are:
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   121
    -d DIR       include session directory
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   122
    -e ML_EXPR   evaluate ML expression on startup
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   123
    -f ML_FILE   evaluate ML file on startup
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   124
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   125
    -m MODE      add print mode for output
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   126
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   127
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   128
  Run the raw Isabelle ML process in batch mode.
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   129
""",
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   130
        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   131
        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   132
        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   133
        "l:" -> (arg => logic = arg),
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   134
        "m:" -> (arg => modes = arg :: modes),
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   135
        "o:" -> (arg => options = options + arg))
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   136
62634
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   137
      val more_args = getopts(args)
aa3b47b32100 less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents: 62633
diff changeset
   138
      if (args.isEmpty || !more_args.isEmpty) getopts.usage()
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   139
62639
699e86051e35 isabelle process -d;
wenzelm
parents: 62638
diff changeset
   140
      ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
62586
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   141
        result().print_stdout.rc
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   142
    }
a522a5692832 clarified modules;
wenzelm
parents: 62577
diff changeset
   143
  }
62544
efa178abe023 manage the underlying ML process in Scala;
wenzelm
parents:
diff changeset
   144
}