--- a/NEWS Fri Feb 04 14:16:55 2011 +0100
+++ b/NEWS Fri Feb 04 17:25:12 2011 +0100
@@ -4,12 +4,20 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Parallelization of nested Isar proofs is subject to
+Goal.parallel_proofs_threshold (default 100). See also isabelle
+usedir option -Q.
+
+
*** Document preparation ***
* New term style "isub" as ad-hoc conversion of variables x1, y23 into
subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
+
New in Isabelle2011 (January 2011)
----------------------------------
--- a/doc-src/System/Thy/Presentation.thy Fri Feb 04 14:16:55 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy Fri Feb 04 17:25:12 2011 +0100
@@ -446,6 +446,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -Q INT set threshold for sub-proof parallelization (default 100)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -565,8 +566,9 @@
\medskip The @{verbatim "-q"} option specifies the level of parallel
proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
- The resulting speedup may vary, depending on the number of worker
- threads, granularity of proofs, and whether proof terms are enabled.
+ The option @{verbatim "-Q"} specifies a threshold for @{verbatim
+ "-q2"}: nested proofs are only parallelized when the current number
+ of forked proofs falls below the given value (default 100).
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
--- a/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 14:16:55 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Fri Feb 04 17:25:12 2011 +0100
@@ -472,6 +472,7 @@
-D PATH dump generated document sources into PATH
-M MAX multithreading: maximum number of worker threads (default 1)
-P PATH set path for remote theory browsing information
+ -Q INT set threshold for sub-proof parallelization (default 100)
-T LEVEL multithreading: trace level (default 0)
-V VERSION declare alternative document VERSION
-b build mode (output heap image, using current dir)
@@ -582,8 +583,8 @@
\medskip The \verb|-q| option specifies the level of parallel
proof checking: \verb|0| no proofs, \verb|1| toplevel
proofs (default), \verb|2| toplevel and nested Isar proofs.
- The resulting speedup may vary, depending on the number of worker
- threads, granularity of proofs, and whether proof terms are enabled.
+ The option \verb|-Q| specifies a threshold for \verb|-q2|: nested proofs are only parallelized when the current number
+ of forked proofs falls below the given value (default 100).
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
--- a/lib/Tools/usedir Fri Feb 04 14:16:55 2011 +0100
+++ b/lib/Tools/usedir Fri Feb 04 17:25:12 2011 +0100
@@ -19,6 +19,7 @@
echo " -D PATH dump generated document sources into PATH"
echo " -M MAX multithreading: maximum number of worker threads (default 1)"
echo " -P PATH set path for remote theory browsing information"
+ echo " -Q INT set threshold for sub-proof parallelization (default 100)"
echo " -T LEVEL multithreading: trace level (default 0)"
echo " -V VERSION declare alternative document VERSION"
echo " -b build mode (output heap image, using current dir)"
@@ -84,13 +85,14 @@
SESSION=""
PROOFS="0"
PARALLEL_PROOFS="1"
+PARALLEL_PROOFS_THRESHOLD="100"
TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
+ while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -111,6 +113,10 @@
P)
RPATH="$OPTARG"
;;
+ Q)
+ check_number "$OPTARG"
+ PARALLEL_PROOFS_THRESHOLD="$OPTARG"
+ ;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
@@ -235,7 +241,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
-q -w $LOGIC $NAME > "$LOG"
RC="$?"
else
@@ -244,7 +250,7 @@
LOG="$LOGDIR/$ITEM"
"$ISABELLE_PROCESS" \
- -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
+ -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
-r -q "$LOGIC" > "$LOG"
RC="$?"
cd ..
--- a/src/HOL/List.thy Fri Feb 04 14:16:55 2011 +0100
+++ b/src/HOL/List.thy Fri Feb 04 17:25:12 2011 +0100
@@ -456,7 +456,9 @@
"xs \<noteq> x # xs"
by (induct xs) auto
-lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
+lemma not_Cons_self2 [simp]:
+ "x # xs \<noteq> xs"
+by (rule not_Cons_self [symmetric])
lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
by (induct xs) auto
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Feb 04 17:25:12 2011 +0100
@@ -214,7 +214,7 @@
end;
fun add_dt_realizers config names thy =
- if ! Proofterm.proofs < 2 then thy
+ if not (Proofterm.proofs_enabled ()) then thy
else
let
val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
--- a/src/Pure/Concurrent/lazy.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/Concurrent/lazy.ML Fri Feb 04 17:25:12 2011 +0100
@@ -43,7 +43,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- uninterruptible (fn restore_interrupts => fn () =>
+ uninterruptible (fn restore_attributes => fn () =>
let
val (expr, x) =
Synchronized.change_result var
@@ -55,7 +55,7 @@
(case expr of
SOME e =>
let
- val res0 = restore_interrupts (fn () => Exn.capture e ()) ();
+ val res0 = Exn.capture (restore_attributes e) ();
val _ = Future.fulfill_result x res0;
val res = Future.join_result x;
(*semantic race: some other threads might see the same
@@ -65,7 +65,7 @@
Synchronized.change var (fn _ => Expr e)
else ();
in res end
- | NONE => restore_interrupts (fn () => Future.join_result x) ())
+ | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
end) ());
fun force r = Exn.release (force_result r);
--- a/src/Pure/Concurrent/task_queue.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Fri Feb 04 17:25:12 2011 +0100
@@ -120,12 +120,13 @@
fun timing_of_task (Task {timing, ...}) = Synchronized.value timing;
fun update_timing update (Task {timing, ...}) e =
- let
- val start = Time.now ();
- val result = Exn.capture e ();
- val t = Time.- (Time.now (), start);
- val _ = Synchronized.change timing (update t);
- in Exn.release result end;
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val start = Time.now ();
+ val result = Exn.capture (restore_attributes e) ();
+ val t = Time.- (Time.now (), start);
+ val _ = Synchronized.change timing (update t);
+ in Exn.release result end) ();
fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
@@ -147,7 +148,9 @@
fun waiting task deps =
update_timing (fn t => fn (a, b, ds) =>
- (Time.- (a, t), Time.+ (b, t), fold (insert (op =) o name_of_task) deps ds)) task;
+ (Time.- (a, t), Time.+ (b, t),
+ if ! Multithreading.trace > 0
+ then fold (insert (op =) o name_of_task) deps ds else ds)) task;
--- a/src/Pure/Isar/toplevel.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/Isar/toplevel.ML Fri Feb 04 17:25:12 2011 +0100
@@ -663,8 +663,7 @@
val future_proof = Proof.global_future_proof
(fn prf =>
- singleton
- (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
+ Goal.fork_name "Toplevel.future_proof"
(fn () =>
let val (states, result_state) =
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
--- a/src/Pure/ProofGeneral/preferences.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Fri Feb 04 17:25:12 2011 +0100
@@ -84,7 +84,7 @@
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
let
- fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
+ fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
--- a/src/Pure/System/session.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/System/session.ML Fri Feb 04 17:25:12 2011 +0100
@@ -11,7 +11,7 @@
val welcome: unit -> string
val use_dir: string -> string -> bool -> string list -> bool -> bool ->
string -> bool -> string list -> string -> string -> bool * string ->
- string -> int -> bool -> bool -> int -> int -> int -> unit
+ string -> int -> bool -> bool -> int -> int -> int -> int -> unit
val finish: unit -> unit
end;
@@ -93,7 +93,8 @@
| dumping (cp, path) = SOME (cp, Path.explode path);
fun use_dir item root build modes reset info doc doc_graph doc_versions parent
- name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
+ name dump rpath level timing verbose max_threads trace_threads
+ parallel_proofs parallel_proofs_threshold =
((fn () =>
(init reset parent name;
Present.init build info doc doc_graph doc_versions (path ()) name
@@ -113,6 +114,7 @@
|> Unsynchronized.setmp Proofterm.proofs level
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
+ |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
|> Unsynchronized.setmp Multithreading.trace trace_threads
|> Unsynchronized.setmp Multithreading.max_threads
(if Multithreading.available then max_threads
--- a/src/Pure/goal.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/goal.ML Fri Feb 04 17:25:12 2011 +0100
@@ -7,6 +7,7 @@
signature BASIC_GOAL =
sig
val parallel_proofs: int Unsynchronized.ref
+ val parallel_proofs_threshold: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -105,21 +106,47 @@
#> Drule.zero_var_indexes;
-(* parallel proofs *)
+(* forked proofs *)
+
+val forked_proofs = Synchronized.var "forked_proofs" 0;
+
+fun forked i =
+ Synchronized.change forked_proofs (fn m =>
+ let
+ val n = m + i;
+ val _ =
+ Multithreading.tracing 1 (fn () =>
+ ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
+ in n end);
fun fork_name name e =
- singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
- (fn () => Future.status e);
+ uninterruptible (fn _ => fn () =>
+ let
+ val _ = forked 1;
+ val future =
+ singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1})
+ (fn () =>
+ (*interruptible*)
+ Exn.release
+ (Exn.capture Future.status e before forked ~1
+ handle exn => (forked ~1; reraise exn)));
+ in future end) ();
fun fork e = fork_name "Goal.fork" e;
+(* scheduling parameters *)
+
val parallel_proofs = Unsynchronized.ref 1;
+val parallel_proofs_threshold = Unsynchronized.ref 100;
fun future_enabled () =
- Multithreading.enabled () andalso is_some (Future.worker_task ()) andalso ! parallel_proofs >= 1;
+ Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso
+ is_some (Future.worker_task ());
-fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
+fun local_future_enabled () =
+ future_enabled () andalso ! parallel_proofs >= 2 andalso
+ Synchronized.value forked_proofs < ! parallel_proofs_threshold;
(* future_result *)
--- a/src/Pure/proofterm.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/proofterm.ML Fri Feb 04 17:25:12 2011 +0100
@@ -52,6 +52,7 @@
val approximate_proof_body: proof -> proof_body
(** primitive operations **)
+ val proofs_enabled: unit -> bool
val proof_combt: proof * term list -> proof
val proof_combt': proof * term option list -> proof
val proof_combP: proof * proof list -> proof
@@ -973,6 +974,7 @@
(***** axioms and theorems *****)
val proofs = Unsynchronized.ref 2;
+fun proofs_enabled () = ! proofs >= 2;
fun vars_of t = map Var (rev (Term.add_vars t []));
fun frees_of t = map Free (rev (Term.add_frees t []));
@@ -1444,7 +1446,7 @@
fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
val body0 =
- if ! proofs <> 2 then Future.value (make_body0 MinProof)
+ if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
singleton
@@ -1453,6 +1455,7 @@
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
val (i, body') =
+ (*non-deterministic, depends on unknown promises*)
(case strip_combt (fst (strip_combP prf)) of
(PThm (i, ((old_name, prop', NONE), body')), args') =>
if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'
--- a/src/Pure/thm.ML Fri Feb 04 14:16:55 2011 +0100
+++ b/src/Pure/thm.ML Fri Feb 04 17:25:12 2011 +0100
@@ -576,6 +576,7 @@
(* closed derivations with official name *)
+(*non-deterministic, depends on unknown promises*)
fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
@@ -585,7 +586,7 @@
val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;
val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
- val ps = map (apsnd (Future.map proof_body_of)) promises;
+ val ps = map (apsnd (Future.map fulfill_body)) promises;
val thy = Theory.deref thy_ref;
val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;
val der' = make_deriv [] [] [pthm] proof;
@@ -1226,7 +1227,7 @@
val tfrees = rev (Term.add_tfree_names prop []);
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
- val ps = map (apsnd (Future.map proof_body_of)) promises;
+ val ps = map (apsnd (Future.map fulfill_body)) promises;
val thy = Theory.deref thy_ref;
val (pthm as (_, (_, prop', _)), proof) =
Proofterm.unconstrain_thm_proof thy shyps prop ps body;