# HG changeset patch # User wenzelm # Date 1457818269 -3600 # Node ID 8dac815f9f6a5c8cc013269ef6c1be1483ace9c9 # Parent f26dc26f21610f7a64fb62d744cb94a3cff1717e# Parent 7f325faed9f7cbe2700a169908897581653fc017 merged diff -r f26dc26f2161 -r 8dac815f9f6a src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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 diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/PIDE/protocol.ML --- 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" diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/System/bash.scala --- 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 } diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/System/isabelle_process.ML --- 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; diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/System/isabelle_system.scala --- 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) } diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/Tools/build.ML --- 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]; diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/Tools/build.scala --- 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) { diff -r f26dc26f2161 -r 8dac815f9f6a src/Pure/Tools/ml_process.scala --- 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() + }) }