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