# HG changeset patch # User wenzelm # Date 1248024244 -7200 # Node ID 11f8ee55662da5d2761cc65a988236f4bd737059 # Parent b54cb3acbbe4db0a49b46e5c5b3eb673ff49b63b parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs; diff -r b54cb3acbbe4 -r 11f8ee55662d NEWS --- 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) diff -r b54cb3acbbe4 -r 11f8ee55662d doc-src/System/Thy/Presentation.thy --- 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 diff -r b54cb3acbbe4 -r 11f8ee55662d doc-src/System/Thy/document/Presentation.tex --- 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 diff -r b54cb3acbbe4 -r 11f8ee55662d etc/settings --- 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="" diff -r b54cb3acbbe4 -r 11f8ee55662d lib/Tools/usedir --- 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 ;; diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/Isar/isar_cmd.ML --- 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; diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/Isar/proof.ML --- 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); diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/ProofGeneral/preferences.ML --- 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), diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/System/session.ML --- 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; diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/Thy/thy_info.ML --- 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 diff -r b54cb3acbbe4 -r 11f8ee55662d src/Pure/goal.ML --- 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 *)