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 *)