author | wenzelm |
Tue, 08 Mar 2016 18:38:29 +0100 | |
changeset 62560 | 498f6ff16804 |
parent 62557 | a4ea3a222e0e |
child 62563 | 2e352f63d15f |
permissions | -rw-r--r-- |
62544 | 1 |
/* Title: Pure/System/ml_process.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
The underlying ML process. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object ML_Process |
|
11 |
{ |
|
12 |
def apply(options: Options, |
|
13 |
heap: String = "", |
|
14 |
args: List[String] = Nil, |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
15 |
modes: List[String] = Nil, |
62544 | 16 |
secure: Boolean = false, |
62557 | 17 |
redirect: Boolean = false, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
18 |
process_socket: String = ""): Bash.Process = |
62544 | 19 |
{ |
20 |
val load_heaps = |
|
21 |
{ |
|
22 |
if (heap == "RAW_ML_SYSTEM") Nil |
|
23 |
else if (heap.iterator.contains('/')) { |
|
24 |
val heap_path = Path.explode(heap) |
|
25 |
if (!heap_path.is_file) error("Bad heap file: " + heap_path) |
|
26 |
List(heap_path) |
|
27 |
} |
|
28 |
else { |
|
29 |
val dirs = Isabelle_System.find_logics_dirs() |
|
30 |
val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap |
|
31 |
dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { |
|
32 |
case Some(heap_path) => List(heap_path) |
|
33 |
case None => |
|
34 |
error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" + |
|
35 |
cat_lines(dirs.map(dir => " " + dir.implode))) |
|
36 |
} |
|
37 |
} |
|
38 |
} |
|
39 |
||
40 |
val eval_heaps = |
|
41 |
load_heaps.map(load_heap => |
|
42 |
"PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + |
|
43 |
" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
|
44 |
ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + |
|
45 |
"); OS.Process.exit OS.Process.failure)") |
|
46 |
||
62560 | 47 |
val eval_initial = |
62544 | 48 |
if (load_heaps.isEmpty) { |
49 |
List( |
|
50 |
if (Platform.is_windows) |
|
51 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
52 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
53 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 54 |
else |
55 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
56 |
"PolyML.Compiler.prompt1 := \"ML> \"", |
|
57 |
"PolyML.Compiler.prompt2 := \"ML# \"", |
|
62547 | 58 |
"PolyML.print_depth 10") |
62544 | 59 |
} |
60 |
else Nil |
|
61 |
||
62 |
val eval_modes = |
|
63 |
if (modes.isEmpty) Nil |
|
64 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) |
|
65 |
||
66 |
// options |
|
67 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
68 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
|
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
|
69 |
val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62547 | 70 |
val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 71 |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
72 |
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
|
73 |
|
62544 | 74 |
val eval_process = |
75 |
if (process_socket == "") Nil |
|
76 |
else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket)) |
|
77 |
||
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
|
78 |
// 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
|
79 |
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
|
80 |
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
62560 | 81 |
(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
|
82 |
map(eval => List("--eval", eval)).flatten ::: args |
62546 | 83 |
|
62557 | 84 |
Bash.process(env = env, redirect = redirect, script = |
62544 | 85 |
""" |
86 |
[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle |
|
87 |
||
88 |
export ISABELLE_PID="$$" |
|
89 |
export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" |
|
90 |
mkdir -p "$ISABELLE_TMP" |
|
91 |
chmod $(umask -S) "$ISABELLE_TMP" |
|
92 |
||
93 |
librarypath "$ML_HOME" |
|
62548 | 94 |
"$ML_HOME/poly" -q -i """ + File.bash_args(bash_args) + """ |
62544 | 95 |
RC="$?" |
96 |
||
97 |
rm -f "$ISABELLE_PROCESS_OPTIONS" |
|
98 |
rmdir "$ISABELLE_TMP" |
|
99 |
||
100 |
exit "$RC" |
|
62546 | 101 |
""") |
62544 | 102 |
} |
103 |
} |