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