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