author | wenzelm |
Wed, 16 Mar 2016 20:50:38 +0100 | |
changeset 62638 | 751cf9f3d433 |
parent 62637 | 0189fe0f6452 |
child 62639 | 699e86051e35 |
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, |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
16 |
logic: String = "", |
62544 | 17 |
args: List[String] = Nil, |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
18 |
dirs: List[Path] = Nil, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
19 |
modes: List[String] = Nil, |
62544 | 20 |
secure: Boolean = false, |
62573 | 21 |
cwd: JFile = null, |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62606
diff
changeset
|
22 |
env: Map[String, String] = Isabelle_System.settings(), |
62557 | 23 |
redirect: Boolean = false, |
62603 | 24 |
cleanup: () => Unit = () => (), |
62633 | 25 |
channel: Option[System_Channel] = None, |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
26 |
tree: Option[Sessions.Tree] = None, |
62633 | 27 |
store: Sessions.Store = Sessions.store()): Bash.Process = |
62544 | 28 |
{ |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
29 |
val logic_name = Isabelle_System.default_logic(logic) |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
30 |
val heaps: List[String] = |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
31 |
if (logic_name == "RAW_ML_SYSTEM") Nil |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
32 |
else { |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
33 |
val session_tree = tree.getOrElse(Sessions.load(options, dirs)) |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
34 |
(session_tree.ancestors(logic_name) ::: List(logic_name)). |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
35 |
map(a => File.platform_path(store.heap(a))) |
62544 | 36 |
} |
37 |
||
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
38 |
val eval_init = |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
39 |
if (heaps.isEmpty) { |
62544 | 40 |
List( |
41 |
if (Platform.is_windows) |
|
42 |
"fun exit 0 = OS.Process.exit OS.Process.success" + |
|
43 |
" | exit 1 = OS.Process.exit OS.Process.failure" + |
|
44 |
" | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" |
|
62560 | 45 |
else |
46 |
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", |
|
62629
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
47 |
"PolyML.Compiler.prompt1 := \"Poly/ML> \"", |
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset
|
48 |
"PolyML.Compiler.prompt2 := \"Poly/ML# \"") |
62544 | 49 |
} |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
50 |
else |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
51 |
List( |
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
52 |
"(PolyML.SaveState.loadHierarchy " + |
62638 | 53 |
ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
54 |
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + |
62638 | 55 |
ML_Syntax.print_string0(": " + logic_name + "\n") + |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
56 |
"); OS.Process.exit OS.Process.failure)") |
62544 | 57 |
|
58 |
val eval_modes = |
|
59 |
if (modes.isEmpty) Nil |
|
62638 | 60 |
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes)) |
62544 | 61 |
|
62 |
// options |
|
63 |
val isabelle_process_options = Isabelle_System.tmp_file("options") |
|
64 |
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) |
|
62573 | 65 |
val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
66 |
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") |
62544 | 67 |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62548
diff
changeset
|
68 |
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
|
69 |
|
62544 | 70 |
val eval_process = |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
71 |
if (heaps.isEmpty) |
62576 | 72 |
List("PolyML.print_depth 10") |
62565 | 73 |
else |
74 |
channel match { |
|
75 |
case None => |
|
62576 | 76 |
List("(default_print_depth 10; Isabelle_Process.init_options ())") |
62565 | 77 |
case Some(ch) => |
62576 | 78 |
List("(default_print_depth 10; Isabelle_Process.init_protocol " + |
62638 | 79 |
ML_Syntax.print_string0(ch.server_name) + ")") |
62565 | 80 |
} |
62544 | 81 |
|
62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
82 |
// ISABELLE_TMP |
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset
|
83 |
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
|
84 |
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
|
85 |
|
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
|
86 |
// 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
|
87 |
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
|
88 |
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: |
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset
|
89 |
(eval_init ::: 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
|
90 |
map(eval => List("--eval", eval)).flatten ::: args |
62546 | 91 |
|
62614 | 92 |
Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args), |
93 |
cwd = cwd, |
|
94 |
env = |
|
95 |
Isabelle_System.library_path(env ++ env_options ++ env_tmp, |
|
96 |
Isabelle_System.getenv_strict("ML_HOME")), |
|
97 |
redirect = redirect, |
|
62602 | 98 |
cleanup = () => |
99 |
{ |
|
100 |
isabelle_process_options.delete |
|
101 |
Isabelle_System.rm_tree(isabelle_tmp) |
|
62603 | 102 |
cleanup() |
62602 | 103 |
}) |
62544 | 104 |
} |
62586 | 105 |
|
106 |
||
107 |
/* command line entry point */ |
|
108 |
||
109 |
def main(args: Array[String]) |
|
110 |
{ |
|
111 |
Command_Line.tool { |
|
112 |
var eval_args: List[String] = Nil |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
113 |
var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
62586 | 114 |
var modes: List[String] = Nil |
115 |
var options = Options.init() |
|
116 |
||
117 |
val getopts = Getopts(""" |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
118 |
Usage: isabelle process [OPTIONS] |
62586 | 119 |
|
120 |
Options are: |
|
121 |
-e ML_EXPR evaluate ML expression on startup |
|
122 |
-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
|
123 |
-l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
62586 | 124 |
-m MODE add print mode for output |
125 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
126 |
||
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
127 |
Run the raw Isabelle ML process in batch mode. |
62586 | 128 |
""", |
129 |
"e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), |
|
130 |
"f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
131 |
"l:" -> (arg => logic = arg), |
62586 | 132 |
"m:" -> (arg => modes = arg :: modes), |
133 |
"o:" -> (arg => options = options + arg)) |
|
134 |
||
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
135 |
val more_args = getopts(args) |
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
136 |
if (args.isEmpty || !more_args.isEmpty) getopts.usage() |
62586 | 137 |
|
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
138 |
ML_Process(options, logic = logic, args = eval_args ::: args.toList, modes = modes). |
62586 | 139 |
result().print_stdout.rc |
140 |
} |
|
141 |
} |
|
62544 | 142 |
} |