author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73897 | 0ddb5de0506e |
child 75394 | 42267c650205 |
permissions | -rw-r--r-- |
65477 | 1 |
/* Title: Pure/ML/ml_process.scala |
62544 | 2 |
Author: Makarius |
3 |
||
62586 | 4 |
The raw ML process. |
62544 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
73897 | 10 |
import java.util.{Map => JMap, HashMap} |
62573 | 11 |
import java.io.{File => JFile} |
12 |
||
13 |
||
75393 | 14 |
object ML_Process { |
62544 | 15 |
def apply(options: Options, |
71594 | 16 |
sessions_structure: Sessions.Structure, |
71598 | 17 |
store: Sessions.Store, |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
18 |
logic: String = "", |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
19 |
raw_ml_system: Boolean = false, |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
20 |
use_prelude: List[String] = Nil, |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
21 |
eval_main: String = "", |
62544 | 22 |
args: List[String] = Nil, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
23 |
modes: List[String] = Nil, |
62573 | 24 |
cwd: JFile = null, |
73897 | 25 |
env: JMap[String, String] = Isabelle_System.settings(), |
62557 | 26 |
redirect: Boolean = false, |
62603 | 27 |
cleanup: () => Unit = () => (), |
75393 | 28 |
session_base: Option[Sessions.Base] = None |
29 |
): Bash.Process = { |
|
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
30 |
val logic_name = Isabelle_System.default_logic(logic) |
68209 | 31 |
|
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
32 |
val heaps: List[String] = |
62643 | 33 |
if (raw_ml_system) Nil |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
34 |
else { |
72571 | 35 |
sessions_structure.selection(logic_name). |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69831
diff
changeset
|
36 |
build_requirements(List(logic_name)). |
71598 | 37 |
map(a => File.platform_path(store.the_heap(a))) |
62544 | 38 |
} |
39 |
||
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
40 |
val eval_init = |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
41 |
if (heaps.isEmpty) { |
62544 | 42 |
List( |
62912 | 43 |
""" |
44 |
fun chapter (_: string) = (); |
|
45 |
fun section (_: string) = (); |
|
46 |
fun subsection (_: string) = (); |
|
47 |
fun subsubsection (_: string) = (); |
|
48 |
fun paragraph (_: string) = (); |
|
49 |
fun subparagraph (_: string) = (); |
|
50 |
val ML_file = PolyML.use; |
|
51 |
""", |
|
62544 | 52 |
if (Platform.is_windows) |
53 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
54 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
55 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 56 |
else |
57 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
62629
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
58 |
"PolyML.Compiler.prompt1 := \"Poly/ML> \"", |
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
59 |
"PolyML.Compiler.prompt2 := \"Poly/ML# \"") |
62544 | 60 |
} |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
61 |
else |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
62 |
List( |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
63 |
"(PolyML.SaveState.loadHierarchy " + |
66782 | 64 |
ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
65 |
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
66782 | 66 |
ML_Syntax.print_string_bytes(": " + logic_name + "\n") + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
67 |
"); OS.Process.exit OS.Process.failure)") |
62544 | 68 |
|
69 |
val eval_modes = |
|
70 |
if (modes.isEmpty) Nil |
|
66782 | 71 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) |
62544 | 72 |
|
73897 | 73 |
|
62544 | 74 |
// options |
75 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
71114 | 76 |
Isabelle_System.chmod("600", File.path(isabelle_process_options)) |
62544 | 77 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
78 |
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 79 |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
80 |
// session base |
72637 | 81 |
val init_session = Isabelle_System.tmp_file("init_session") |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
82 |
Isabelle_System.chmod("600", File.path(init_session)) |
72637 | 83 |
val eval_init_session = |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
84 |
session_base match { |
72637 | 85 |
case None => Nil |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
86 |
case Some(base) => |
72637 | 87 |
File.write(init_session, new Resources(sessions_structure, base).init_session_yxml) |
88 |
List("Resources.init_session_file (Path.explode " + |
|
89 |
ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")") |
|
90 |
} |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
91 |
|
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65420
diff
changeset
|
92 |
// process |
62544 | 93 |
val eval_process = |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
94 |
proper_string(eval_main).getOrElse( |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
95 |
if (heaps.isEmpty) { |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
96 |
"PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
97 |
} |
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
98 |
else "Isabelle_Process.init ()") |
62544 | 99 |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
100 |
// ISABELLE_TMP |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
101 |
val isabelle_tmp = Isabelle_System.tmp_dir("process") |
71881 | 102 |
|
75393 | 103 |
val ml_runtime_options = { |
64274 | 104 |
val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) |
69702 | 105 |
val ml_options1 = |
106 |
if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options |
|
107 |
else ml_options ::: List("--gcthreads", options.int("threads").toString) |
|
108 |
val ml_options2 = |
|
109 |
if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 |
|
110 |
else ml_options1 ::: List("--codepage", "utf8") |
|
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
71881
diff
changeset
|
111 |
ml_options2 ::: List("--exportstats") |
64274 | 112 |
} |
113 |
||
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
114 |
// bash |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62544
diff
changeset
|
115 |
val bash_args = |
64274 | 116 |
ml_runtime_options ::: |
72637 | 117 |
(eval_init ::: eval_modes ::: eval_options ::: eval_init_session).flatMap(List("--eval", _)) ::: |
71639
ec84f542e411
clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";
wenzelm
parents:
71598
diff
changeset
|
118 |
use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args |
62546 | 119 |
|
73897 | 120 |
val bash_env = new HashMap(env) |
121 |
bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options)) |
|
122 |
bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp)) |
|
123 |
bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath) |
|
124 |
bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(",")) |
|
125 |
||
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
62912
diff
changeset
|
126 |
Bash.process( |
73604 | 127 |
options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + |
64304 | 128 |
Bash.strings(bash_args), |
62614 | 129 |
cwd = cwd, |
73897 | 130 |
env = bash_env, |
62614 | 131 |
redirect = redirect, |
75393 | 132 |
cleanup = () => { |
62602 | 133 |
isabelle_process_options.delete |
72615
f827c3bb6b7f
more scalable: avoid large strings on command-line;
wenzelm
parents:
72614
diff
changeset
|
134 |
init_session.delete |
62602 | 135 |
Isabelle_System.rm_tree(isabelle_tmp) |
62603 | 136 |
cleanup() |
62602 | 137 |
}) |
62544 | 138 |
} |
62586 | 139 |
|
140 |
||
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
141 |
/* Isabelle tool wrapper */ |
62586 | 142 |
|
72763 | 143 |
val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", |
75393 | 144 |
Scala_Project.here, args => { |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
145 |
var dirs: List[Path] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
146 |
var eval_args: List[String] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
147 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
148 |
var modes: List[String] = Nil |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
149 |
var options = Options.init() |
62586 | 150 |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
151 |
val getopts = Getopts(""" |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
152 |
Usage: isabelle process [OPTIONS] |
62586 | 153 |
|
154 |
Options are: |
|
62677 | 155 |
-T THEORY load theory |
62639 | 156 |
-d DIR include session directory |
62586 | 157 |
-e ML_EXPR evaluate ML expression on startup |
158 |
-f ML_FILE evaluate ML file on startup |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
159 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
62586 | 160 |
-m MODE add print mode for output |
161 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
162 |
||
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
163 |
Run the raw Isabelle ML process in batch mode. |
62586 | 164 |
""", |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
165 |
"T:" -> (arg => |
66782 | 166 |
eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
167 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
168 |
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
169 |
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
170 |
"l:" -> (arg => logic = arg), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
171 |
"m:" -> (arg => modes = arg :: modes), |
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
172 |
"o:" -> (arg => options = options + arg)) |
62586 | 173 |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
174 |
val more_args = getopts(args) |
71383 | 175 |
if (args.isEmpty || more_args.nonEmpty) getopts.usage() |
62586 | 176 |
|
72628
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
177 |
val base_info = Sessions.base_info(options, logic, dirs = dirs).check |
71598 | 178 |
val store = Sessions.store(options) |
72557 | 179 |
val result = |
72628
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
180 |
ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, |
5e616a454b23
clarified Resources.init_session for low-level "isabelle process";
wenzelm
parents:
72620
diff
changeset
|
181 |
modes = modes, session_base = Some(base_info.base)) |
72557 | 182 |
.result( |
183 |
progress_stdout = Output.writeln(_, stdout = true), |
|
184 |
progress_stderr = Output.writeln(_)) |
|
185 |
||
186 |
sys.exit(result.rc) |
|
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset
|
187 |
}) |
62544 | 188 |
} |