author | wenzelm |
Sat, 12 Mar 2016 22:51:37 +0100 | |
changeset 62606 | 247963aa1c5d |
parent 62603 | c077eb5e0b56 |
child 62610 | 4c89504c76fb |
permissions | -rw-r--r-- |
62586 | 1 |
/* Title: Pure/Tools/ml_process.scala |
62544 | 2 |
Author: Makarius |
3 |
||
62586 | 4 |
The raw ML process. |
62544 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
62573 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
62544 | 13 |
object ML_Process |
14 |
{ |
|
15 |
def apply(options: Options, |
|
16 |
heap: String = "", |
|
17 |
args: List[String] = Nil, |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
18 |
modes: List[String] = Nil, |
62544 | 19 |
secure: Boolean = false, |
62573 | 20 |
cwd: JFile = null, |
21 |
env: Map[String, String] = Map.empty, |
|
62557 | 22 |
redirect: Boolean = false, |
62603 | 23 |
cleanup: () => Unit = () => (), |
62564 | 24 |
channel: Option[System_Channel] = None): Bash.Process = |
62544 | 25 |
{ |
26 |
val load_heaps = |
|
27 |
{ |
|
28 |
if (heap == "RAW_ML_SYSTEM") Nil |
|
29 |
else if (heap.iterator.contains('/')) { |
|
30 |
val heap_path = Path.explode(heap) |
|
31 |
if (!heap_path.is_file) error("Bad heap file: " + heap_path) |
|
32 |
List(heap_path) |
|
33 |
} |
|
34 |
else { |
|
35 |
val dirs = Isabelle_System.find_logics_dirs() |
|
36 |
val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap |
|
37 |
dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { |
|
38 |
case Some(heap_path) => List(heap_path) |
|
39 |
case None => |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
40 |
error("Unknown logic " + quote(heap_name) + " -- no heap file found in:\n" + |
62544 | 41 |
cat_lines(dirs.map(dir => " " + dir.implode))) |
42 |
} |
|
43 |
} |
|
44 |
} |
|
45 |
||
46 |
val eval_heaps = |
|
47 |
load_heaps.map(load_heap => |
|
62576 | 48 |
"(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + |
49 |
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
|
62544 | 50 |
ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + |
51 |
"); OS.Process.exit OS.Process.failure)") |
|
52 |
||
62560 | 53 |
val eval_initial = |
62544 | 54 |
if (load_heaps.isEmpty) { |
55 |
List( |
|
56 |
if (Platform.is_windows) |
|
57 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
58 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
59 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 60 |
else |
61 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
62 |
"PolyML.Compiler.prompt1 := \"ML> \"", |
|
62576 | 63 |
"PolyML.Compiler.prompt2 := \"ML# \"") |
62544 | 64 |
} |
65 |
else Nil |
|
66 |
||
67 |
val eval_modes = |
|
68 |
if (modes.isEmpty) Nil |
|
69 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) |
|
70 |
||
71 |
// options |
|
72 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
73 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
|
62573 | 74 |
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62547 | 75 |
val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 76 |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
77 |
val eval_secure = if (secure) List("Secure.set_secure ()") else Nil |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
78 |
|
62544 | 79 |
val eval_process = |
62576 | 80 |
if (load_heaps.isEmpty) |
81 |
List("PolyML.print_depth 10") |
|
62565 | 82 |
else |
83 |
channel match { |
|
84 |
case None => |
|
62576 | 85 |
List("(default_print_depth 10; Isabelle_Process.init_options ())") |
62565 | 86 |
case Some(ch) => |
62576 | 87 |
List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
88 |
ML_Syntax.print_string_raw(ch.server_name) + ")") |
|
62565 | 89 |
} |
62544 | 90 |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
91 |
// ISABELLE_TMP |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
92 |
val isabelle_tmp = Isabelle_System.tmp_dir("process") |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
93 |
val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
94 |
|
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
|
95 |
// 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
|
96 |
val bash_args = |
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
|
97 |
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
62560 | 98 |
(eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). |
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
|
99 |
map(eval => List("--eval", eval)).flatten ::: args |
62546 | 100 |
|
62573 | 101 |
Bash.process( |
62606 | 102 |
"""librarypath "$ML_HOME"; exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args), |
62602 | 103 |
cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect, |
104 |
cleanup = () => |
|
105 |
{ |
|
106 |
isabelle_process_options.delete |
|
107 |
Isabelle_System.rm_tree(isabelle_tmp) |
|
62603 | 108 |
cleanup() |
62602 | 109 |
}) |
62544 | 110 |
} |
62586 | 111 |
|
112 |
||
113 |
/* command line entry point */ |
|
114 |
||
115 |
def main(args: Array[String]) |
|
116 |
{ |
|
117 |
Command_Line.tool { |
|
118 |
var eval_args: List[String] = Nil |
|
119 |
var modes: List[String] = Nil |
|
120 |
var options = Options.init() |
|
121 |
||
122 |
val getopts = Getopts(""" |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
123 |
Usage: isabelle process [OPTIONS] [HEAP] |
62586 | 124 |
|
125 |
Options are: |
|
126 |
-e ML_EXPR evaluate ML expression on startup |
|
127 |
-f ML_FILE evaluate ML file on startup |
|
128 |
-m MODE add print mode for output |
|
129 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
130 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
131 |
Run the raw Isabelle ML process in batch mode, using a given heap image. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
132 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
133 |
If HEAP is a plain name (default ISABELLE_LOGIC=""" + |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
134 |
quote(Isabelle_System.getenv("ISABELLE_LOGIC")) + """), it is searched in |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
135 |
ISABELLE_PATH; if it contains a slash, it is taken as literal file; |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
136 |
if it is "RAW_ML_SYSTEM", the initial ML heap is used. |
62586 | 137 |
""", |
138 |
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
|
139 |
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
|
140 |
"m:" -> (arg => modes = arg :: modes), |
|
141 |
"o:" -> (arg => options = options + arg)) |
|
142 |
||
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62586
diff
changeset
|
143 |
if (args.isEmpty) getopts.usage() |
62586 | 144 |
val heap = |
145 |
getopts(args) match { |
|
146 |
case Nil => "" |
|
147 |
case List(heap) => heap |
|
148 |
case _ => getopts.usage() |
|
149 |
} |
|
150 |
||
151 |
ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes). |
|
152 |
result().print_stdout.rc |
|
153 |
} |
|
154 |
} |
|
62544 | 155 |
} |