parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
--- a/NEWS Sun Jul 19 19:20:17 2009 +0200
+++ b/NEWS Sun Jul 19 19:24:04 2009 +0200
@@ -120,6 +120,9 @@
* Removed "compress" option from isabelle-process and isabelle usedir;
this is always enabled.
+* More fine-grained control of proof parallelism, cf.
+Goal.parallel_proofs in ML and usedir option -q LEVEL.
+
New in Isabelle2009 (April 2009)
--- a/doc-src/System/Thy/Presentation.thy Sun Jul 19 19:20:17 2009 +0200
+++ b/doc-src/System/Thy/Presentation.thy Sun Jul 19 19:24:04 2009 +0200
@@ -451,7 +451,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -564,6 +565,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \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.
+
\medskip The @{verbatim "-t"} option produces a more detailed
internal timing report of the session.
@@ -583,13 +590,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The @{verbatim "-Q"} option tells whether individual proofs
- should be checked in parallel; the default is @{verbatim true}.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any @{tool usedir} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
--- a/doc-src/System/Thy/document/Presentation.tex Sun Jul 19 19:20:17 2009 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Sun Jul 19 19:24:04 2009 +0200
@@ -477,7 +477,8 @@
-g BOOL generate session graph image for document (default false)
-i BOOL generate theory browser information (default false)
-m MODE add print mode for output
- -p LEVEL set level of detail for proof objects
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
-r reset session path
-s NAME override session NAME
-t BOOL internal session timing (default false)
@@ -581,6 +582,12 @@
for internal proof objects, see also the \emph{Isabelle Reference
Manual}~\cite{isabelle-ref}.
+ \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.
+
\medskip The \verb|-t| option produces a more detailed
internal timing report of the session.
@@ -599,13 +606,6 @@
bottle-necks, e.g.\ due to excessive wait states when locking
critical code sections.
- \medskip The \verb|-Q| option tells whether individual proofs
- should be checked in parallel; the default is \verb|true|.
- Note that fine-grained proof parallelism requires considerable
- amounts of extra memory, since full proof context information is
- maintained for each independent derivation thread, until checking is
- completed.
-
\medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
identifier}. These accumulate, documenting the way sessions depend
on others. For example, consider \verb|Pure/FOL/ex|, which
--- a/etc/settings Sun Jul 19 19:20:17 2009 +0200
+++ b/etc/settings Sun Jul 19 19:24:04 2009 +0200
@@ -96,7 +96,7 @@
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2 -Q false"
+#HOL_USEDIR_OPTIONS="-p 2 -q 1"
#Source file identification (default: full name + date stamp)
ISABELLE_FILE_IDENT=""
--- a/lib/Tools/usedir Sun Jul 19 19:20:17 2009 +0200
+++ b/lib/Tools/usedir Sun Jul 19 19:24:04 2009 +0200
@@ -19,7 +19,6 @@
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 BOOL check proofs in parallel (default true)"
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)"
@@ -28,7 +27,8 @@
echo " -g BOOL generate session graph image for document (default false)"
echo " -i BOOL generate HTML and graph browser information (default false)"
echo " -m MODE add print mode for output"
- echo " -p LEVEL set level of detail for proof objects"
+ echo " -p LEVEL set level of detail for proof objects (default 0)"
+ echo " -q LEVEL set level of parallel proof checking (default 1)"
echo " -r reset session path"
echo " -s NAME override session NAME"
echo " -t BOOL internal session timing (default false)"
@@ -73,7 +73,6 @@
DUMP=""
MAXTHREADS="1"
RPATH=""
-PARALLEL_PROOFS="true"
TRACETHREADS="0"
DOCUMENT_VERSIONS=""
BUILD=""
@@ -84,14 +83,15 @@
MODES=""
RESET=false
SESSION=""
-PROOFS=0
+PROOFS="0"
+PARALLEL_PROOFS="1"
TIMING=false
VERBOSE=false
function getoptions()
{
OPTIND=1
- while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
+ while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
do
case "$OPT" in
C)
@@ -112,9 +112,6 @@
P)
RPATH="$OPTARG"
;;
- Q)
- PARALLEL_PROOFS="$OPTARG"
- ;;
T)
check_number "$OPTARG"
TRACETHREADS="$OPTARG"
@@ -154,6 +151,10 @@
check_number "$OPTARG"
PROOFS="$OPTARG"
;;
+ q)
+ check_number "$OPTARG"
+ PARALLEL_PROOFS="$OPTARG"
+ ;;
r)
RESET=true
;;
--- a/src/Pure/Isar/isar_cmd.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sun Jul 19 19:24:04 2009 +0200
@@ -230,7 +230,7 @@
(* local endings *)
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
val local_default_proof = Toplevel.proof Proof.local_default_proof;
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
val local_done_proof = Toplevel.proof Proof.local_done_proof;
--- a/src/Pure/Isar/proof.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/Isar/proof.ML Sun Jul 19 19:24:04 2009 +0200
@@ -1043,7 +1043,7 @@
local
fun future_terminal_proof proof1 proof2 meths int state =
- if int orelse is_relevant state orelse not (Goal.future_enabled ())
+ if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
then proof1 meths state
else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
--- a/src/Pure/ProofGeneral/preferences.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Sun Jul 19 19:24:04 2009 +0200
@@ -84,6 +84,12 @@
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) ();
+val parallel_proof_pref =
+ let
+ fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
+ fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
+ in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
+
val thm_depsN = "thm_deps";
val thm_deps_pref =
let
@@ -171,9 +177,7 @@
nat_pref Multithreading.max_threads
"max-threads"
"Maximum number of threads",
- bool_pref Goal.parallel_proofs
- "parallel-proofs"
- "Check proofs in parallel"];
+ parallel_proof_pref];
val pure_preferences =
[(category_display, display_preferences),
--- a/src/Pure/System/session.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/System/session.ML Sun Jul 19 19:24:04 2009 +0200
@@ -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 -> bool -> unit
+ string -> int -> bool -> bool -> int -> int -> int -> unit
val finish: unit -> unit
end;
--- a/src/Pure/Thy/thy_info.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Sun Jul 19 19:24:04 2009 +0200
@@ -350,7 +350,7 @@
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
- val par_proofs = ! parallel_proofs;
+ val par_proofs = ! parallel_proofs >= 1;
fun fork (name, body) tab =
let
--- a/src/Pure/goal.ML Sun Jul 19 19:20:17 2009 +0200
+++ b/src/Pure/goal.ML Sun Jul 19 19:24:04 2009 +0200
@@ -6,7 +6,7 @@
signature BASIC_GOAL =
sig
- val parallel_proofs: bool ref
+ val parallel_proofs: int ref
val SELECT_GOAL: tactic -> int -> tactic
val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -21,6 +21,7 @@
val finish: thm -> thm
val norm_result: thm -> thm
val future_enabled: unit -> bool
+ val local_future_enabled: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -95,10 +96,12 @@
(* future_enabled *)
-val parallel_proofs = ref true;
+val parallel_proofs = ref 1;
fun future_enabled () =
- Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
+ Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+
+fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
(* future_result *)