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