# HG changeset patch
# User wenzelm
# Date 1231619550 -3600
# Node ID a5f84ac146090aca3ee7201a01e831590c9ef255
# Parent  3f49ae779bddcbedabbce7da511403182e9a7cfc
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

diff -r 3f49ae779bdd -r a5f84ac14609 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Sat Jan 10 16:58:56 2009 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Sat Jan 10 21:32:30 2009 +0100
@@ -442,6 +442,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 BOOL      check proofs in parallel (default true)
     -T LEVEL     multithreading: trace level (default 0)
     -V VERSION   declare alternative document VERSION
     -b           build mode (output heap image, using current dir)
@@ -461,6 +462,11 @@
 
   ISABELLE_USEDIR_OPTIONS=
   HOL_USEDIR_OPTIONS=
+
+  ML_PLATFORM=x86-linux
+  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
+  ML_SYSTEM=polyml-5.2.1
+  ML_OPTIONS=-H 500
 \end{ttbox}
 
   Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
@@ -574,6 +580,13 @@
   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 3f49ae779bdd -r a5f84ac14609 doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Sat Jan 10 16:58:56 2009 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex	Sat Jan 10 21:32:30 2009 +0100
@@ -468,6 +468,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 BOOL      check proofs in parallel (default true)
     -T LEVEL     multithreading: trace level (default 0)
     -V VERSION   declare alternative document VERSION
     -b           build mode (output heap image, using current dir)
@@ -487,6 +488,11 @@
 
   ISABELLE_USEDIR_OPTIONS=
   HOL_USEDIR_OPTIONS=
+
+  ML_PLATFORM=x86-linux
+  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
+  ML_SYSTEM=polyml-5.2.1
+  ML_OPTIONS=-H 500
 \end{ttbox}
 
   Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
@@ -590,6 +596,13 @@
   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 3f49ae779bdd -r a5f84ac14609 lib/Tools/usedir
--- a/lib/Tools/usedir	Sat Jan 10 16:58:56 2009 +0100
+++ b/lib/Tools/usedir	Sat Jan 10 21:32:30 2009 +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 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)"
@@ -72,6 +73,7 @@
 DUMP=""
 MAXTHREADS="1"
 RPATH=""
+PARALLEL_PROOFS="true"
 TRACETHREADS="0"
 DOCUMENT_VERSIONS=""
 BUILD=""
@@ -89,7 +91,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
+  while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       C)
@@ -101,15 +103,18 @@
         ;;
       M)
         if [ "$OPTARG" = max ]; then
-	  MAXTHREADS=0
-	else
+          MAXTHREADS=0
+        else
           check_number "$OPTARG"
           MAXTHREADS="$OPTARG"
-	fi
+        fi
         ;;
       P)
         RPATH="$OPTARG"
         ;;
+      Q)
+        PARALLEL_PROOFS="$OPTARG"
+        ;;
       T)
         check_number "$OPTARG"
         TRACETHREADS="$OPTARG"
@@ -232,7 +237,7 @@
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \
+    -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \
     $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
@@ -241,7 +246,7 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \
+    -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; quit();" \
     -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -1041,7 +1041,7 @@
 local
 
 fun future_terminal_proof proof1 proof2 meths int state =
-  if int orelse is_relevant state orelse not (Future.enabled ())
+  if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
   then proof1 meths state
   else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
 
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/Isar/session.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/session.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Session management -- maintain state of logic images.
@@ -11,7 +10,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
-    string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
+    string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
   val finish: unit -> unit
 end;
 
@@ -87,7 +86,7 @@
   | dumping (cp, path) = SOME (cp, Path.explode path);
 
 fun use_dir root build modes reset info doc doc_graph doc_versions
-    parent name dump rpath level verbose max_threads trace_threads =
+    parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
   ((fn () =>
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
@@ -96,6 +95,7 @@
       finish ()))
     |> setmp_noncritical Proofterm.proofs level
     |> setmp_noncritical print_mode (modes @ print_mode_value ())
+    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
     |> setmp_noncritical Multithreading.trace trace_threads
     |> setmp_noncritical Multithreading.max_threads
       (if Multithreading.available then max_threads
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -34,7 +34,8 @@
   ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
 
 fun prove ctxt xs asms prop tac =
-  (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
+  (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
+    ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
       then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -745,7 +745,7 @@
   let
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
-    val immediate = not (Future.enabled ());
+    val immediate = not (Future.enabled () andalso ! Goal.parallel_proofs);
     val (results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/preferences.ML
-    ID:         $Id$
     Author:     David Aspinall and Markus Wenzel
 
 User preferences for Isabelle which are maintained by the interface.
@@ -164,7 +163,10 @@
   proof_pref,
   nat_pref Multithreading.max_threads
     "max-threads"
-    "Maximum number of threads"];
+    "Maximum number of threads",
+  bool_pref Goal.parallel_proofs
+    "parallel-proofs"
+    "Check proofs in parallel"];
 
 val pure_preferences =
  [("Display", display_preferences),
diff -r 3f49ae779bdd -r a5f84ac14609 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Jan 10 16:58:56 2009 +0100
+++ b/src/Pure/goal.ML	Sat Jan 10 21:32:30 2009 +0100
@@ -6,6 +6,7 @@
 
 signature BASIC_GOAL =
 sig
+  val parallel_proofs: bool ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -123,6 +124,8 @@
       |> fold (Thm.elim_implies o Thm.assume) assms;
   in local_result end;
 
+val parallel_proofs = ref true;
+
 
 
 (** tactical theorem proving **)
@@ -172,7 +175,8 @@
             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
-      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
+      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
+        not (Future.enabled () andalso ! parallel_proofs)
       then result ()
       else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
   in