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