--- /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 </dev/null
+ RC="$?"
+else
+ if [ -z "$TERMINATE" ]; then
+ FEEDER_OPTS=""
+ else
+ FEEDER_OPTS="-q"
+ ML_OPTIONS="$ML_OPTIONS --error-exit"
+ fi
+ "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+ { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+ RC="$?"
+fi
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Dec 11 22:53:32 2013 +0800
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Dec 11 20:57:47 2013 +0100
@@ -158,7 +158,7 @@
if ($output_log) { print "Mirabelle: $thy_file\n"; }
my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-o quick_and_dirty -e 'Unsynchronized.setmp Multithreading.max_threads 1 use_thy \"$path/$new_thy_name\" handle _ => 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");
--- 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 {*
--- 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 {*
--- 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;
--- 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 =
--- 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;
--- /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;
--- 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);
--- 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"
--- 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;
--- 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 ();
--- 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];
--- 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";