# HG changeset patch # User wenzelm # Date 1386791867 -3600 # Node ID 5cfcb71779881fd06d43b05f3fd018b0b761215c # Parent 55ed20a29a8c04e18e42ec1517ffeb084cdd57b1# Parent 8c5221d698cdcb867d1ede37647d93cb41942a97 merged diff -r 55ed20a29a8c -r 5cfcb7177988 lib/scripts/run-polyml-5.5.2 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/run-polyml-5.5.2 Wed Dec 11 20:57:47 2013 +0100 @@ -0,0 +1,90 @@ +#!/usr/bin/env bash +# :mode=shellscript: +# +# Author: Makarius +# +# Startup script for Poly/ML 5.5.2. + +export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE + + +## diagnostics + +function fail() +{ + echo "$1" >&2 + exit 2 +} + +function fail_out() +{ + fail "Unable to create output heap file: \"$OUTFILE\"" +} + +function check_file() +{ + [ ! -f "$1" ] && fail "Unable to locate \"$1\"" +} + + +## compiler executables and libraries + +[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)" + +POLY="$ML_HOME/poly" +check_file "$POLY" + +librarypath "$ML_HOME" + + + +## prepare databases + +if [ -z "$INFILE" ]; then + INIT="" + EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);" +else + check_file "$INFILE" + INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));" + EXIT="" +fi + +if [ -z "$OUTFILE" ]; then + COMMIT='fun commit () = false;' + MLEXIT="" +else + if [ -z "$INFILE" ]; then + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);" + else + COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");" + fi + [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } + MLEXIT="commit();" +fi + + +## run it! + +MLTEXT="$INIT $EXIT $COMMIT $MLTEXT" + +if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then + "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \ + --error-exit exit 1;\n' -q $mirabelle_logic" . $quiet; + "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet; if ($output_log) { my $outcome = ($result ? "failure" : "success"); diff -r 55ed20a29a8c -r 5cfcb7177988 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Wed Dec 11 22:53:32 2013 +0800 +++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Dec 11 20:57:47 2013 +0100 @@ -17,7 +17,7 @@ declare [[sledgehammer_instantiate_inducts = false]] ML {* -!Multithreading.max_threads +Multithreading.max_threads_value () *} ML {* diff -r 55ed20a29a8c -r 5cfcb7177988 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Dec 11 22:53:32 2013 +0800 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Dec 11 20:57:47 2013 +0100 @@ -19,7 +19,7 @@ hide_fact (open) HOL.ext ML {* -!Multithreading.max_threads +Multithreading.max_threads_value () *} ML {* diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ML-Systems/multithreading.ML --- a/src/Pure/ML-Systems/multithreading.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/ML-Systems/multithreading.ML Wed Dec 11 20:57:47 2013 +0100 @@ -14,8 +14,9 @@ sig include BASIC_MULTITHREADING val available: bool - val max_threads: int ref val max_threads_value: unit -> int + val max_threads_update: int -> unit + val max_threads_setmp: int -> ('a -> 'b) -> 'a -> 'b val enabled: unit -> bool val no_interrupts: Thread.threadAttribute list val public_interrupts: Thread.threadAttribute list @@ -39,8 +40,9 @@ (* options *) val available = false; -val max_threads = ref (1: int); fun max_threads_value () = 1: int; +fun max_threads_update _ = (); +fun max_threads_setmp _ f x = f x; fun enabled () = false; diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Dec 11 20:57:47 2013 +0100 @@ -25,21 +25,6 @@ structure Multithreading: MULTITHREADING = struct -(* options *) - -val available = true; - -val max_threads = ref 1; - -fun max_threads_value () = - let val m = ! max_threads in - if m > 0 then m - else Int.min (Int.max (Thread.numProcessors (), 1), 8) - end; - -fun enabled () = max_threads_value () > 1; - - (* thread attributes *) val no_interrupts = @@ -90,6 +75,37 @@ f (fn g => fn y => with_attributes atts (fn _ => g y)) x); +(* options *) + +val available = true; + +fun max_threads_result m = + if m > 0 then m + else + let val n = + (case Thread.numPhysicalProcessors () of + SOME n => n + | NONE => Thread.numProcessors ()) + in Int.min (Int.max (n, 1), 8) end; + +val max_threads = ref 1; + +fun max_threads_value () = ! max_threads; + +fun max_threads_update m = max_threads := max_threads_result m; + +fun max_threads_setmp m f x = + uninterruptible (fn restore_attributes => fn () => + let + val max_threads_orig = ! max_threads; + val _ = max_threads_update m; + val result = Exn.capture (restore_attributes f) x; + val _ = max_threads := max_threads_orig; + in Exn.release result end) (); + +fun enabled () = max_threads_value () > 1; + + (* synchronous wait *) fun sync_wait opt_atts time cond lock = diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/ML-Systems/polyml.ML Wed Dec 11 20:57:47 2013 +0100 @@ -4,6 +4,25 @@ Compatibility wrapper for Poly/ML. *) +(* ML system operations *) + +use "ML-Systems/ml_system.ML"; + +if ML_System.name = "polyml-5.3.0" +then use "ML-Systems/share_common_data_polyml-5.3.0.ML" +else (); + +structure ML_System = +struct + +open ML_System; + +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; +val save_state = PolyML.SaveState.saveState; + +end; + + (* exceptions *) fun reraise exn = @@ -25,6 +44,9 @@ else use "ML-Systems/single_assignment_polyml.ML"; open Thread; +if ML_System.name = "polyml-5.5.2" then () +else use "ML-Systems/thread_physical_processors.ML"; + use "ML-Systems/multithreading.ML"; use "ML-Systems/multithreading_polyml.ML"; @@ -56,25 +78,6 @@ fun quit () = exit 0; -(* ML system operations *) - -use "ML-Systems/ml_system.ML"; - -if ML_System.name = "polyml-5.3.0" -then use "ML-Systems/share_common_data_polyml-5.3.0.ML" -else (); - -structure ML_System = -struct - -open ML_System; - -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; -val save_state = PolyML.SaveState.saveState; - -end; - - (* ML runtime system *) fun print_exception_trace (_: exn -> string) = PolyML.exception_trace; @@ -128,7 +131,7 @@ val pretty_ml = let fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd) - | convert _ (PolyML.PrettyBlock (ind, _, + | convert _ (PolyML.PrettyBlock (_, _, [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) = ML_Pretty.Break (true, 1) | convert len (PolyML.PrettyBlock (ind, _, context, prts)) = @@ -136,7 +139,7 @@ fun property name default = (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of SOME (PolyML.ContextProperty (_, b)) => b - | NONE => default); + | _ => default); val bg = property "begin" ""; val en = property "end" ""; val len' = property "length" len; diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ML-Systems/thread_physical_processors.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/thread_physical_processors.ML Wed Dec 11 20:57:47 2013 +0100 @@ -0,0 +1,12 @@ +(* Title: Pure/ML-Systems/thread_physical_processors.ML + Author: Makarius + +Emulation of structure Thread in Poly/ML 5.5.2 (SVN 1890). +*) + +structure Thread = +struct + open Thread; + + fun numPhysicalProcessors () : int option = NONE; +end; diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/PIDE/protocol.ML Wed Dec 11 20:57:47 2013 +0100 @@ -18,7 +18,7 @@ Options.set_default options; Future.ML_statistics := true; Multithreading.trace := Options.int options "threads_trace"; - Multithreading.max_threads := Options.int options "threads"; + Multithreading.max_threads_update (Options.int options "threads"); Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0) end); diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ROOT --- a/src/Pure/ROOT Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/ROOT Wed Dec 11 20:57:47 2013 +0100 @@ -19,6 +19,7 @@ "ML-Systems/share_common_data_polyml-5.3.0.ML" "ML-Systems/smlnj.ML" "ML-Systems/thread_dummy.ML" + "ML-Systems/thread_physical_processors.ML" "ML-Systems/universal.ML" "ML-Systems/unsynchronized.ML" "ML-Systems/use_context.ML" @@ -41,6 +42,7 @@ "ML-Systems/single_assignment_polyml.ML" "ML-Systems/smlnj.ML" "ML-Systems/thread_dummy.ML" + "ML-Systems/thread_physical_processors.ML" "ML-Systems/universal.ML" "ML-Systems/unsynchronized.ML" "ML-Systems/use_context.ML" diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/ROOT.ML Wed Dec 11 20:57:47 2013 +0100 @@ -76,10 +76,13 @@ else use "ML/exn_properties_dummy.ML"; if ML_System.name = "polyml-5.5.1" + orelse ML_System.name = "polyml-5.5.2" then use "ML/exn_trace_polyml-5.5.1.ML" else (); -if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1" +if ML_System.name = "polyml-5.5.0" + orelse ML_System.name = "polyml-5.5.1" + orelse ML_System.name = "polyml-5.5.2" then use "ML/ml_statistics_polyml-5.5.0.ML" else use "ML/ml_statistics_dummy.ML"; @@ -347,5 +350,4 @@ val cd = File.cd o Path.explode; Proofterm.proofs := 0; -Multithreading.max_threads := 0; diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/System/isar.ML Wed Dec 11 20:57:47 2013 +0100 @@ -155,6 +155,7 @@ fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} = (Context.set_thread_data NONE; + Multithreading.max_threads_update (Options.default_int "threads"); if do_init then init () else (); Output.Internal.protocol_message_fn := protocol_message; if welcome then writeln (Session.welcome ()) else (); diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/Tools/build.ML Wed Dec 11 20:57:47 2013 +0100 @@ -107,7 +107,7 @@ (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") - |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") + |> Multithreading.max_threads_setmp (Options.int options "threads") |> Unsynchronized.setmp Future.ML_statistics true |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin") |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing"); @@ -167,7 +167,7 @@ (List.app (use_theories_condition last_timing) |> session_timing name verbose |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message - |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads") + |> Multithreading.max_threads_setmp (Options.int options "threads") |> Exn.capture); val res2 = Exn.capture Session.finish (); val _ = Par_Exn.release_all [res1, res2]; diff -r 55ed20a29a8c -r 5cfcb7177988 src/Pure/Tools/proof_general_pure.ML --- a/src/Pure/Tools/proof_general_pure.ML Wed Dec 11 22:53:32 2013 +0800 +++ b/src/Pure/Tools/proof_general_pure.ML Wed Dec 11 20:57:47 2013 +0100 @@ -161,9 +161,11 @@ "Record full proof objects internally"; val _ = - ProofGeneral.preference_int ProofGeneral.category_proof + ProofGeneral.preference ProofGeneral.category_proof NONE - Multithreading.max_threads + (Markup.print_int o Multithreading.max_threads_value) + (Multithreading.max_threads_update o Markup.parse_int) + ProofGeneral.pgipint "max-threads" "Maximum number of threads"; @@ -172,7 +174,7 @@ NONE (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1)) (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0)) - ProofGeneral.pgipbool + ProofGeneral.pgipint "parallel-proofs" "Check proofs in parallel";