src/Pure/ML/ml_process.scala
author wenzelm
Thu May 17 15:38:36 2018 +0200 (11 months ago)
changeset 68204 a554da2811f2
parent 67586 8b19a8a7f029
child 68209 aeffd8f1f079
permissions -rw-r--r--
clarified signature;
wenzelm@65477
     1
/*  Title:      Pure/ML/ml_process.scala
wenzelm@62544
     2
    Author:     Makarius
wenzelm@62544
     3
wenzelm@62586
     4
The raw ML process.
wenzelm@62544
     5
*/
wenzelm@62544
     6
wenzelm@62544
     7
package isabelle
wenzelm@62544
     8
wenzelm@62544
     9
wenzelm@62573
    10
import java.io.{File => JFile}
wenzelm@62573
    11
wenzelm@62573
    12
wenzelm@62544
    13
object ML_Process
wenzelm@62544
    14
{
wenzelm@62544
    15
  def apply(options: Options,
wenzelm@62634
    16
    logic: String = "",
wenzelm@62544
    17
    args: List[String] = Nil,
wenzelm@62637
    18
    dirs: List[Path] = Nil,
wenzelm@62556
    19
    modes: List[String] = Nil,
wenzelm@62643
    20
    raw_ml_system: Boolean = false,
wenzelm@62573
    21
    cwd: JFile = null,
wenzelm@62610
    22
    env: Map[String, String] = Isabelle_System.settings(),
wenzelm@62557
    23
    redirect: Boolean = false,
wenzelm@62603
    24
    cleanup: () => Unit = () => (),
wenzelm@62633
    25
    channel: Option[System_Channel] = None,
wenzelm@68204
    26
    sessions_structure: Option[Sessions.Structure] = None,
wenzelm@65431
    27
    session_base: Option[Sessions.Base] = None,
wenzelm@62633
    28
    store: Sessions.Store = Sessions.store()): Bash.Process =
wenzelm@62544
    29
  {
wenzelm@62637
    30
    val logic_name = Isabelle_System.default_logic(logic)
wenzelm@62637
    31
    val heaps: List[String] =
wenzelm@62643
    32
      if (raw_ml_system) Nil
wenzelm@62637
    33
      else {
wenzelm@65419
    34
        val selection = Sessions.Selection(sessions = List(logic_name))
wenzelm@67025
    35
        val selected_sessions =
wenzelm@68204
    36
          sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
wenzelm@68204
    37
            .selection(selection)
wenzelm@66848
    38
        selected_sessions.build_requirements(List(logic_name)).
wenzelm@62637
    39
          map(a => File.platform_path(store.heap(a)))
wenzelm@62544
    40
      }
wenzelm@62544
    41
wenzelm@62637
    42
    val eval_init =
wenzelm@62634
    43
      if (heaps.isEmpty) {
wenzelm@62544
    44
        List(
wenzelm@62912
    45
          """
wenzelm@62912
    46
          fun chapter (_: string) = ();
wenzelm@62912
    47
          fun section (_: string) = ();
wenzelm@62912
    48
          fun subsection (_: string) = ();
wenzelm@62912
    49
          fun subsubsection (_: string) = ();
wenzelm@62912
    50
          fun paragraph (_: string) = ();
wenzelm@62912
    51
          fun subparagraph (_: string) = ();
wenzelm@62912
    52
          val ML_file = PolyML.use;
wenzelm@62912
    53
          """,
wenzelm@64557
    54
          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
wenzelm@64557
    55
            """
wenzelm@64557
    56
              structure FixedInt = IntInf;
wenzelm@64557
    57
              structure RunCall =
wenzelm@64557
    58
              struct
wenzelm@64557
    59
                open RunCall
wenzelm@64557
    60
                val loadWord: word * word -> word =
wenzelm@64557
    61
                  run_call2 RuntimeCalls.POLY_SYS_load_word;
wenzelm@64557
    62
                val storeWord: word * word * word -> unit =
wenzelm@64557
    63
                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
wenzelm@64557
    64
              end;
wenzelm@64557
    65
            """
wenzelm@62855
    66
          else "",
wenzelm@62544
    67
          if (Platform.is_windows)
wenzelm@62544
    68
            "fun exit 0 = OS.Process.exit OS.Process.success" +
wenzelm@62544
    69
            " | exit 1 = OS.Process.exit OS.Process.failure" +
wenzelm@62544
    70
            " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
wenzelm@62560
    71
          else
wenzelm@62560
    72
            "fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
wenzelm@62629
    73
          "PolyML.Compiler.prompt1 := \"Poly/ML> \"",
wenzelm@62629
    74
          "PolyML.Compiler.prompt2 := \"Poly/ML# \"")
wenzelm@62544
    75
      }
wenzelm@62637
    76
      else
wenzelm@62637
    77
        List(
wenzelm@62637
    78
          "(PolyML.SaveState.loadHierarchy " +
wenzelm@66782
    79
            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
wenzelm@62637
    80
          "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
wenzelm@66782
    81
          ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
wenzelm@62637
    82
          "); OS.Process.exit OS.Process.failure)")
wenzelm@62544
    83
wenzelm@62544
    84
    val eval_modes =
wenzelm@62544
    85
      if (modes.isEmpty) Nil
wenzelm@66782
    86
      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
wenzelm@62544
    87
wenzelm@62544
    88
    // options
wenzelm@62544
    89
    val isabelle_process_options = Isabelle_System.tmp_file("options")
wenzelm@62544
    90
    File.write(isabelle_process_options, YXML.string_of_body(options.encode))
wenzelm@62573
    91
    val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
wenzelm@62634
    92
    val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
wenzelm@62544
    93
wenzelm@65431
    94
    // session base
wenzelm@65431
    95
    val eval_session_base =
wenzelm@65431
    96
      session_base match {
wenzelm@65431
    97
        case None => Nil
wenzelm@65431
    98
        case Some(base) =>
wenzelm@65441
    99
          def print_table(table: List[(String, String)]): String =
wenzelm@65431
   100
            ML_Syntax.print_list(
wenzelm@65431
   101
              ML_Syntax.print_pair(
wenzelm@66782
   102
                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
wenzelm@66712
   103
          def print_list(list: List[String]): String =
wenzelm@66782
   104
            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
wenzelm@67493
   105
          def print_sessions(list: List[(String, Position.T)]): String =
wenzelm@67493
   106
            ML_Syntax.print_list(
wenzelm@67493
   107
              ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
wenzelm@67493
   108
wenzelm@65532
   109
          List("Resources.init_session_base" +
wenzelm@67493
   110
            " {sessions = " + print_sessions(base.known.sessions.toList) +
wenzelm@67520
   111
            ", docs = " + print_list(base.doc_names) +
wenzelm@67219
   112
            ", global_theories = " + print_table(base.global_theories.toList) +
wenzelm@66717
   113
            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
wenzelm@65441
   114
            ", known_theories = " + print_table(base.dest_known_theories) + "}")
wenzelm@65431
   115
      }
wenzelm@65431
   116
wenzelm@65431
   117
    // process
wenzelm@62544
   118
    val eval_process =
wenzelm@62634
   119
      if (heaps.isEmpty)
wenzelm@62712
   120
        List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
wenzelm@62565
   121
      else
wenzelm@62565
   122
        channel match {
wenzelm@62565
   123
          case None =>
wenzelm@62712
   124
            List("Isabelle_Process.init_options ()")
wenzelm@62565
   125
          case Some(ch) =>
wenzelm@66782
   126
            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
wenzelm@62565
   127
        }
wenzelm@62544
   128
wenzelm@62601
   129
    // ISABELLE_TMP
wenzelm@62601
   130
    val isabelle_tmp = Isabelle_System.tmp_dir("process")
wenzelm@62601
   131
    val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
wenzelm@62601
   132
wenzelm@64274
   133
    val ml_runtime_options =
wenzelm@64274
   134
    {
wenzelm@64274
   135
      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
wenzelm@64274
   136
      if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
wenzelm@64274
   137
      else ml_options ::: List("--gcthreads", options.int("threads").toString)
wenzelm@64274
   138
    }
wenzelm@64274
   139
wenzelm@62545
   140
    // bash
wenzelm@62545
   141
    val bash_args =
wenzelm@64274
   142
      ml_runtime_options :::
wenzelm@65431
   143
      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
wenzelm@62545
   144
        map(eval => List("--eval", eval)).flatten ::: args
wenzelm@62546
   145
wenzelm@63986
   146
    Bash.process(
wenzelm@63986
   147
      "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
wenzelm@64304
   148
        Bash.strings(bash_args),
wenzelm@62614
   149
      cwd = cwd,
wenzelm@67586
   150
      env = env ++ env_options ++ env_tmp,
wenzelm@62614
   151
      redirect = redirect,
wenzelm@62602
   152
      cleanup = () =>
wenzelm@62602
   153
        {
wenzelm@62602
   154
          isabelle_process_options.delete
wenzelm@62602
   155
          Isabelle_System.rm_tree(isabelle_tmp)
wenzelm@62603
   156
          cleanup()
wenzelm@62602
   157
        })
wenzelm@62544
   158
  }
wenzelm@62586
   159
wenzelm@62586
   160
wenzelm@62835
   161
  /* Isabelle tool wrapper */
wenzelm@62586
   162
wenzelm@62835
   163
  val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
wenzelm@62586
   164
  {
wenzelm@62835
   165
    var dirs: List[Path] = Nil
wenzelm@62835
   166
    var eval_args: List[String] = Nil
wenzelm@62835
   167
    var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@62835
   168
    var modes: List[String] = Nil
wenzelm@62835
   169
    var options = Options.init()
wenzelm@62586
   170
wenzelm@62835
   171
    val getopts = Getopts("""
wenzelm@62634
   172
Usage: isabelle process [OPTIONS]
wenzelm@62586
   173
wenzelm@62586
   174
  Options are:
wenzelm@62677
   175
    -T THEORY    load theory
wenzelm@62639
   176
    -d DIR       include session directory
wenzelm@62586
   177
    -e ML_EXPR   evaluate ML expression on startup
wenzelm@62586
   178
    -f ML_FILE   evaluate ML file on startup
wenzelm@62634
   179
    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
wenzelm@62586
   180
    -m MODE      add print mode for output
wenzelm@62586
   181
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62586
   182
wenzelm@62634
   183
  Run the raw Isabelle ML process in batch mode.
wenzelm@62586
   184
""",
wenzelm@62835
   185
      "T:" -> (arg =>
wenzelm@66782
   186
        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
wenzelm@62835
   187
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@62835
   188
      "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
wenzelm@62835
   189
      "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
wenzelm@62835
   190
      "l:" -> (arg => logic = arg),
wenzelm@62835
   191
      "m:" -> (arg => modes = arg :: modes),
wenzelm@62835
   192
      "o:" -> (arg => options = options + arg))
wenzelm@62586
   193
wenzelm@62835
   194
    val more_args = getopts(args)
wenzelm@62835
   195
    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
wenzelm@62586
   196
wenzelm@62888
   197
    val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
wenzelm@62835
   198
      result().print_stdout.rc
wenzelm@62888
   199
    sys.exit(rc)
wenzelm@62835
   200
  })
wenzelm@62544
   201
}