provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
/* Title: Pure/ML/ml_process.scala
Author: Makarius
The raw ML process.
*/
package isabelle
import java.io.{File => JFile}
object ML_Process
{
def apply(options: Options,
sessions_structure: Sessions.Structure,
store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
use_prelude: List[String] = Nil,
eval_main: String = "",
args: List[String] = Nil,
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
cleanup: () => Unit = () => (),
session_base: Option[Sessions.Base] = None): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
val heaps: List[String] =
if (raw_ml_system) Nil
else {
sessions_structure.selection(Sessions.Selection.session(logic_name)).
build_requirements(List(logic_name)).
map(a => File.platform_path(store.the_heap(a)))
}
val eval_init =
if (heaps.isEmpty) {
List(
"""
fun chapter (_: string) = ();
fun section (_: string) = ();
fun subsection (_: string) = ();
fun subsubsection (_: string) = ();
fun paragraph (_: string) = ();
fun subparagraph (_: string) = ();
val ML_file = PolyML.use;
""",
if (Platform.is_windows)
"fun exit 0 = OS.Process.exit OS.Process.success" +
" | exit 1 = OS.Process.exit OS.Process.failure" +
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))"
else
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)",
"PolyML.Compiler.prompt1 := \"Poly/ML> \"",
"PolyML.Compiler.prompt2 := \"Poly/ML# \"")
}
else
List(
"(PolyML.SaveState.loadHierarchy " +
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
"); OS.Process.exit OS.Process.failure)")
val eval_modes =
if (modes.isEmpty) Nil
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
// options
val isabelle_process_options = Isabelle_System.tmp_file("options")
Isabelle_System.chmod("600", File.path(isabelle_process_options))
File.write(isabelle_process_options, YXML.string_of_body(options.encode))
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
// session base
val eval_session_base =
session_base match {
case None => Nil
case Some(base) =>
def print_table(table: List[(String, String)]): String =
ML_Syntax.print_list(
ML_Syntax.print_pair(
ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
def print_list(list: List[String]): String =
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
def print_sessions(list: List[(String, Position.T)]): String =
ML_Syntax.print_list(
ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
List("Resources.init_session" +
"{session_positions = " + print_sessions(sessions_structure.session_positions) +
", session_directories = " + print_table(sessions_structure.dest_session_directories) +
", docs = " + print_list(base.doc_names) +
", global_theories = " + print_table(base.global_theories.toList) +
", loaded_theories = " + print_list(base.loaded_theories.keys) + "}")
}
// process
val eval_process =
proper_string(eval_main).getOrElse(
if (heaps.isEmpty) {
"PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
}
else "Isabelle_Process.init ()")
// ISABELLE_TMP
val isabelle_tmp = Isabelle_System.tmp_dir("process")
val env_tmp =
Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp),
"POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath)
val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
val ml_runtime_options =
{
val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
val ml_options1 =
if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
else ml_options ::: List("--gcthreads", options.int("threads").toString)
val ml_options2 =
if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
else ml_options1 ::: List("--codepage", "utf8")
ml_options2 ::: List("--exportstats")
}
// bash
val bash_args =
ml_runtime_options :::
(eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) :::
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args
Bash.process(
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
Bash.strings(bash_args),
cwd = cwd,
env = env ++ env_options ++ env_tmp ++ env_functions,
redirect = redirect,
cleanup = () =>
{
isabelle_process_options.delete
Isabelle_System.rm_tree(isabelle_tmp)
cleanup()
})
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
{
var dirs: List[Path] = Nil
var eval_args: List[String] = Nil
var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
var modes: List[String] = Nil
var options = Options.init()
val getopts = Getopts("""
Usage: isabelle process [OPTIONS]
Options are:
-T THEORY load theory
-d DIR include session directory
-e ML_EXPR evaluate ML expression on startup
-f ML_FILE evaluate ML file on startup
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
-m MODE add print mode for output
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
Run the raw Isabelle ML process in batch mode.
""",
"T:" -> (arg =>
eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
"o:" -> (arg => options = options + arg))
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
val sessions_structure = Sessions.load_structure(options, dirs = dirs)
val store = Sessions.store(options)
val rc =
ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
.result().print_stdout.rc
sys.exit(rc)
})
}