--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Mar 12 22:22:12 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sat Mar 12 22:31:09 2016 +0100
@@ -315,7 +315,6 @@
val ctxt = Proof.context_of state
val override_params = override_params |> map (normalize_raw_param ctxt)
- val _ = Isabelle_System.mkdir (Path.explode (getenv "ISABELLE_TMP"))
in
if subcommand = runN then
let val i = the_default 1 opt_i in
--- a/src/Pure/PIDE/protocol.ML Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML Sat Mar 12 22:31:09 2016 +0100
@@ -14,11 +14,7 @@
val _ =
Isabelle_Process.protocol_command "Prover.options"
(fn [options_yxml] =>
- let val options = Options.decode (YXML.parse_body options_yxml) in
- Options.set_default options;
- Isabelle_Process.init_options ();
- Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
- end);
+ Isabelle_Process.init_protocol_options (Options.decode (YXML.parse_body options_yxml)));
val _ =
Isabelle_Process.protocol_command "Document.define_blob"
--- a/src/Pure/System/bash.scala Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/System/bash.scala Sat Mar 12 22:31:09 2016 +0100
@@ -29,14 +29,19 @@
def process(script: String,
cwd: JFile = null,
env: Map[String, String] = Map.empty,
- redirect: Boolean = false): Process =
- new Process(script, cwd, env, redirect)
+ redirect: Boolean = false,
+ cleanup: () => Unit = () => ()): Process =
+ new Process(script, cwd, env, redirect, cleanup)
class Process private [Bash](
- script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
+ script: String,
+ cwd: JFile,
+ env: Map[String, String],
+ redirect: Boolean,
+ cleanup: () => Unit)
extends Prover.System_Process
{
- private val timing_file = Isabelle_System.tmp_file("bash_script")
+ private val timing_file = Isabelle_System.tmp_file("bash_timing")
private val timing = Synchronized[Option[Timing]](None)
private val script_file = Isabelle_System.tmp_file("bash_script")
@@ -92,7 +97,7 @@
{
multi_kill("INT") && multi_kill("TERM") && kill("KILL")
proc.destroy
- cleanup()
+ do_cleanup()
}
@@ -106,7 +111,7 @@
// cleanup
- private def cleanup()
+ private def do_cleanup()
{
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
@@ -128,6 +133,8 @@
else Some(Timing.zero)
case some => some
}
+
+ cleanup()
}
@@ -136,7 +143,7 @@
def join: Int =
{
val rc = proc.waitFor
- cleanup()
+ do_cleanup()
rc
}
--- a/src/Pure/System/isabelle_process.ML Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML Sat Mar 12 22:31:09 2016 +0100
@@ -12,6 +12,8 @@
val crashes: exn list Synchronized.var
val init_protocol: string -> unit
val init_options: unit -> unit
+ val init_build_options: unit -> unit
+ val init_protocol_options: Options.T -> unit
end;
structure Isabelle_Process: ISABELLE_PROCESS =
@@ -213,4 +215,13 @@
Multithreading.max_threads_update (Options.default_int "threads");
Goal.parallel_proofs := Options.default_int "parallel_proofs");
+fun init_build_options () =
+ (Options.load_default ();
+ init_options ());
+
+fun init_protocol_options options =
+ (Options.set_default options;
+ init_options ();
+ Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0));
+
end;
--- a/src/Pure/System/isabelle_system.scala Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 12 22:31:09 2016 +0100
@@ -306,9 +306,11 @@
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
progress_limit: Option[Long] = None,
- strict: Boolean = true): Process_Result =
+ strict: Boolean = true,
+ cleanup: () => Unit = () => ()): Process_Result =
{
- Bash.process(script, cwd, env).result(progress_stdout, progress_stderr, progress_limit, strict)
+ Bash.process(script, cwd = cwd, env = env, cleanup = cleanup).
+ result(progress_stdout, progress_stderr, progress_limit, strict)
}
--- a/src/Pure/Tools/build.ML Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/Tools/build.ML Sat Mar 12 22:31:09 2016 +0100
@@ -124,30 +124,30 @@
let
val _ = SHA1_Samples.test ();
- val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info,
- (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
+ val (symbol_codes, (command_timings, (output, (verbose, (browser_info,
+ (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
File.read (Path.explode args_file) |> YXML.parse_body |>
let open XML.Decode in
- pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode
+ pair (list (pair string int)) (pair (list properties) (pair string
(pair bool (pair string (pair (list (pair string string)) (pair string
(pair string (pair string (pair string
- ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
+ ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
end;
val do_output = output <> "";
val symbols = HTML.make_symbols symbol_codes;
- val _ = Options.set_default options;
+ val _ = Isabelle_Process.init_build_options ();
val _ = writeln ("\fSession.name = " ^ name);
val _ =
Session.init
symbols
do_output
- (Options.bool options "browser_info")
+ (Options.default_bool "browser_info")
(Path.explode browser_info)
- (Options.string options "document")
- (Options.string options "document_output")
- (Present.document_variants (Options.string options "document_variants"))
+ (Options.default_string "document")
+ (Options.default_string "document_output")
+ (Present.document_variants (Options.default_string "document_variants"))
(map (apply2 Path.explode) document_files)
(Path.explode graph_file)
parent_name (chapter, name)
@@ -160,7 +160,7 @@
(List.app (build_theories symbols last_timing Path.current)
|> session_timing name verbose
|> Unsynchronized.setmp Output.protocol_message_fn protocol_message
- |> Multithreading.max_threads_setmp (Options.int options "threads")
+ |> Multithreading.max_threads_setmp (Options.default_int "threads")
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
val _ = Par_Exn.release_all [res1, res2];
--- a/src/Pure/Tools/build.scala Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/Tools/build.scala Sat Mar 12 22:31:09 2016 +0100
@@ -549,24 +549,6 @@
try { isabelle.graphview.Graph_File.write(info.options, graph_file, session_graph) }
catch { case ERROR(_) => /*error should be exposed in ML*/ }
- private val args_file = Isabelle_System.tmp_file("args")
- private val args_standard_path = File.standard_path(args_file)
- File.write(args_file, YXML.string_of_body(
- if (is_pure(name)) Options.encode(info.options)
- else
- {
- val theories = info.theories.map(x => (x._2, x._3))
- import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(string, pair(Options.encode,
- pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
- pair(string, pair(string, pair(string,
- list(pair(Options.encode, list(Path.encode))))))))))))))(
- (Symbol.codes, (command_timings, (output_standard_path, (info.options,
- (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
- (parent, (info.chapter, (name,
- theories))))))))))))
- }))
-
output.file.delete
private val env = Map("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
@@ -579,14 +561,29 @@
"Command_Line.tool0 (fn () => (Session.finish (); Options.reset_default ();" +
" Session.shutdown (); ML_Heap.share_common_data ();" +
" ML_Heap.save_state " + ML_Syntax.print_string_raw(output_standard_path) + "));"
- val env1 = env + ("ISABELLE_PROCESS_OPTIONS" -> args_standard_path)
ML_Process(info.options, "RAW_ML_SYSTEM", List("--use", "ROOT.ML", "--eval", eval),
- cwd = info.dir.file, env = env1)
+ cwd = info.dir.file, env = env)
}
else {
+ val args_file = Isabelle_System.tmp_file("build")
+ File.write(args_file, YXML.string_of_body(
+ {
+ val theories = info.theories.map(x => (x._2, x._3))
+ import XML.Encode._
+ pair(list(pair(string, int)), pair(list(properties), pair(string, pair(bool,
+ pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
+ pair(string, pair(string, pair(string,
+ list(pair(Options.encode, list(Path.encode)))))))))))))(
+ (Symbol.codes, (command_timings, (output_standard_path, (verbose,
+ (browser_info, (info.document_files, (File.standard_path(graph_file),
+ (parent, (info.chapter, (name,
+ theories)))))))))))
+ }))
ML_Process(info.options, parent,
- List("--eval", "Build.build " + ML_Syntax.print_string_raw(args_standard_path)),
- cwd = info.dir.file, env = env)
+ List("--eval",
+ "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file))),
+ cwd = info.dir.file, env = env,
+ cleanup = () => args_file.delete)
}
process.result(
progress_stdout = (line: String) =>
@@ -621,7 +618,6 @@
Present.finish(progress, browser_info, graph_file, info, name)
graph_file.delete
- args_file.delete
timeout_request.foreach(_.cancel)
if (result.interrupted) {
--- a/src/Pure/Tools/ml_process.scala Sat Mar 12 22:22:12 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Sat Mar 12 22:31:09 2016 +0100
@@ -20,6 +20,7 @@
cwd: JFile = null,
env: Map[String, String] = Map.empty,
redirect: Boolean = false,
+ cleanup: () => Unit = () => (),
channel: Option[System_Channel] = None): Bash.Process =
{
val load_heaps =
@@ -87,6 +88,10 @@
ML_Syntax.print_string_raw(ch.server_name) + ")")
}
+ // ISABELLE_TMP
+ val isabelle_tmp = Isabelle_System.tmp_dir("process")
+ val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
+
// bash
val bash_args =
Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
@@ -95,22 +100,16 @@
Bash.process(
"""
- [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
-
- export ISABELLE_PID="$$"
- export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID"
- mkdir -p "$ISABELLE_TMP"
- chmod $(umask -S) "$ISABELLE_TMP"
-
librarypath "$ML_HOME"
- "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
- RC="$?"
-
- rm -f "$ISABELLE_PROCESS_OPTIONS"
- rmdir "$ISABELLE_TMP"
-
- exit "$RC"
- """, cwd = cwd, env = env ++ env_options, redirect = redirect)
+ exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """
+ """,
+ cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
+ cleanup = () =>
+ {
+ isabelle_process_options.delete
+ Isabelle_System.rm_tree(isabelle_tmp)
+ cleanup()
+ })
}