author  wenzelm 
Sun, 03 Apr 2016 22:54:31 +0200  
changeset 62835  1a9ce1b13b20 
parent 62712  22a17cec2efe 
child 62855  82859dac5f59 
permissions  rwrr 
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 commandline;
wenzelm
parents:
62548
diff
changeset

19 
modes: List[String] = Nil, 
62643  20 
raw_ml_system: 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] = 
62643  31 
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

32 
else { 
62644  33 
val (_, session_tree) = 
34 
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

35 
(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

36 
map(a => File.platform_path(store.heap(a))) 
62544  37 
} 
38 

62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset

39 
val eval_init = 
62634
aa3b47b32100
less physical "logic" argument, with option l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset

40 
if (heaps.isEmpty) { 
62544  41 
List( 
42 
if (Platform.is_windows) 

43 
"fun exit 0 = OS.Process.exit OS.Process.success" + 

44 
"  exit 1 = OS.Process.exit OS.Process.failure" + 

45 
"  exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" 

62560  46 
else 
47 
"fun exit rc = Posix.Process.exit (Word8.fromInt rc)", 

62629
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset

48 
"PolyML.Compiler.prompt1 := \"Poly/ML> \"", 
1815513a57f1
clarified prompt: "ML" usually means Isabelle/ML;
wenzelm
parents:
62614
diff
changeset

49 
"PolyML.Compiler.prompt2 := \"Poly/ML# \"") 
62544  50 
} 
62637
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset

51 
else 
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset

52 
List( 
0189fe0f6452
support for Poly/ML heap hierarchy, which saves a lot of disk space;
wenzelm
parents:
62634
diff
changeset

53 
"(PolyML.SaveState.loadHierarchy " + 
62638  54 
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

55 
"; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + 
62638  56 
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

57 
"); OS.Process.exit OS.Process.failure)") 
62544  58 

59 
val eval_modes = 

60 
if (modes.isEmpty) Nil 

62638  61 
else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes)) 
62544  62 

63 
// options 

64 
val isabelle_process_options = Isabelle_System.tmp_file("options") 

65 
File.write(isabelle_process_options, YXML.string_of_body(options.encode)) 

62573  66 
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

67 
val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") 
62544  68 

69 
val eval_process = 

62634
aa3b47b32100
less physical "logic" argument, with option l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset

70 
if (heaps.isEmpty) 
62712  71 
List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))) 
62565  72 
else 
73 
channel match { 

74 
case None => 

62712  75 
List("Isabelle_Process.init_options ()") 
62565  76 
case Some(ch) => 
62712  77 
List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name)) 
62565  78 
} 
62544  79 

62601
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset

80 
// ISABELLE_TMP 
a937889f0086
create ISABELLE_TMP in Scala (despite odd/obsolete chmod in d84b4d39bce1);
wenzelm
parents:
62600
diff
changeset

81 
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

82 
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

83 

62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not welldefined;
wenzelm
parents:
62544
diff
changeset

84 
// bash 
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not welldefined;
wenzelm
parents:
62544
diff
changeset

85 
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 welldefined;
wenzelm
parents:
62544
diff
changeset

86 
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: 
62668  87 
(eval_init ::: eval_modes ::: eval_options ::: 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 welldefined;
wenzelm
parents:
62544
diff
changeset

88 
map(eval => List("eval", eval)).flatten ::: args 
62546  89 

62614  90 
Bash.process("""exec "$ML_HOME/poly" q """ + File.bash_args(bash_args), 
91 
cwd = cwd, 

92 
env = 

93 
Isabelle_System.library_path(env ++ env_options ++ env_tmp, 

94 
Isabelle_System.getenv_strict("ML_HOME")), 

95 
redirect = redirect, 

62602  96 
cleanup = () => 
97 
{ 

98 
isabelle_process_options.delete 

99 
Isabelle_System.rm_tree(isabelle_tmp) 

62603  100 
cleanup() 
62602  101 
}) 
62544  102 
} 
62586  103 

104 

62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

105 
/* Isabelle tool wrapper */ 
62586  106 

62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

107 
val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => 
62586  108 
{ 
62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

109 
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

110 
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

111 
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

112 
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

113 
var options = Options.init() 
62586  114 

62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

115 
val getopts = Getopts(""" 
62634
aa3b47b32100
less physical "logic" argument, with option l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset

116 
Usage: isabelle process [OPTIONS] 
62586  117 

118 
Options are: 

62677  119 
T THEORY load theory 
62639  120 
d DIR include session directory 
62586  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 
""", 
62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

129 
"T:" > (arg => 
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

130 
eval_args = eval_args ::: List("eval", "use_thy " + ML_Syntax.print_string0(arg))), 
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

131 
"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

132 
"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

133 
"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

134 
"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

135 
"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

136 
"o:" > (arg => options = options + arg)) 
62586  137 

62835
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

138 
val more_args = getopts(args) 
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

139 
if (args.isEmpty  !more_args.isEmpty) getopts.usage() 
62586  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 
ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes). 
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

142 
result().print_stdout.rc 
1a9ce1b13b20
prefer internal tool  assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62712
diff
changeset

143 
}) 
62544  144 
} 