1.1 --- a/doc-src/System/Thy/Presentation.thy	Sat Jan 10 16:58:56 2009 +0100
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Sat Jan 10 21:32:30 2009 +0100
     1.3 @@ -442,6 +442,7 @@
     1.4      -D PATH      dump generated document sources into PATH
     1.5      -M MAX       multithreading: maximum number of worker threads (default 1)
     1.6      -P PATH      set path for remote theory browsing information
     1.7 +    -Q BOOL      check proofs in parallel (default true)
     1.8      -T LEVEL     multithreading: trace level (default 0)
     1.9      -V VERSION   declare alternative document VERSION
    1.10      -b           build mode (output heap image, using current dir)
    1.11 @@ -461,6 +462,11 @@
    1.12  
    1.13    ISABELLE_USEDIR_OPTIONS=
    1.14    HOL_USEDIR_OPTIONS=
    1.15 +
    1.16 +  ML_PLATFORM=x86-linux
    1.17 +  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    1.18 +  ML_SYSTEM=polyml-5.2.1
    1.19 +  ML_OPTIONS=-H 500
    1.20  \end{ttbox}
    1.21  
    1.22    Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
    1.23 @@ -574,6 +580,13 @@
    1.24    bottle-necks, e.g.\ due to excessive wait states when locking
    1.25    critical code sections.
    1.26  
    1.27 +  \medskip The @{verbatim "-Q"} option tells whether individual proofs
    1.28 +  should be checked in parallel; the default is @{verbatim true}.
    1.29 +  Note that fine-grained proof parallelism requires considerable
    1.30 +  amounts of extra memory, since full proof context information is
    1.31 +  maintained for each independent derivation thread, until checking is
    1.32 +  completed.
    1.33 +
    1.34    \medskip Any @{tool usedir} session is named by some \emph{session
    1.35    identifier}. These accumulate, documenting the way sessions depend
    1.36    on others. For example, consider @{verbatim "Pure/FOL/ex"}, which

     2.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sat Jan 10 16:58:56 2009 +0100
     2.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Sat Jan 10 21:32:30 2009 +0100
     2.3 @@ -468,6 +468,7 @@
     2.4      -D PATH      dump generated document sources into PATH
     2.5      -M MAX       multithreading: maximum number of worker threads (default 1)
     2.6      -P PATH      set path for remote theory browsing information
     2.7 +    -Q BOOL      check proofs in parallel (default true)
     2.8      -T LEVEL     multithreading: trace level (default 0)
     2.9      -V VERSION   declare alternative document VERSION
    2.10      -b           build mode (output heap image, using current dir)
    2.11 @@ -487,6 +488,11 @@
    2.12  
    2.13    ISABELLE_USEDIR_OPTIONS=
    2.14    HOL_USEDIR_OPTIONS=
    2.15 +
    2.16 +  ML_PLATFORM=x86-linux
    2.17 +  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    2.18 +  ML_SYSTEM=polyml-5.2.1
    2.19 +  ML_OPTIONS=-H 500
    2.20  \end{ttbox}
    2.21  
    2.22    Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}}
    2.23 @@ -590,6 +596,13 @@
    2.24    bottle-necks, e.g.\ due to excessive wait states when locking
    2.25    critical code sections.
    2.26  
    2.27 +  \medskip The \verb|-Q| option tells whether individual proofs
    2.28 +  should be checked in parallel; the default is \verb|true|.
    2.29 +  Note that fine-grained proof parallelism requires considerable
    2.30 +  amounts of extra memory, since full proof context information is
    2.31 +  maintained for each independent derivation thread, until checking is
    2.32 +  completed.
    2.33 +
    2.34    \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
    2.35    identifier}. These accumulate, documenting the way sessions depend
    2.36    on others. For example, consider \verb|Pure/FOL/ex|, which

     3.1 --- a/lib/Tools/usedir	Sat Jan 10 16:58:56 2009 +0100
     3.2 +++ b/lib/Tools/usedir	Sat Jan 10 21:32:30 2009 +0100
     3.3 @@ -19,6 +19,7 @@
     3.4    echo "    -D PATH      dump generated document sources into PATH"
     3.5    echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
     3.6    echo "    -P PATH      set path for remote theory browsing information"
     3.7 +  echo "    -Q BOOL      check proofs in parallel (default true)"
     3.8    echo "    -T LEVEL     multithreading: trace level (default 0)"
     3.9    echo "    -V VERSION   declare alternative document VERSION"
    3.10    echo "    -b           build mode (output heap image, using current dir)"
    3.11 @@ -72,6 +73,7 @@
    3.12  DUMP=""
    3.13  MAXTHREADS="1"
    3.14  RPATH=""
    3.15 +PARALLEL_PROOFS="true"
    3.16  TRACETHREADS="0"
    3.17  DOCUMENT_VERSIONS=""
    3.18  BUILD=""
    3.19 @@ -89,7 +91,7 @@
    3.20  function getoptions()
    3.21  {
    3.22    OPTIND=1
    3.23 -  while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
    3.24 +  while getopts "C:D:M:P:Q:T:V:bc:d:f:g:i:m:p:rs:v:" OPT
    3.25    do
    3.26      case "$OPT" in
    3.27        C)
    3.28 @@ -101,15 +103,18 @@
    3.29          ;;
    3.30        M)
    3.31          if [ "$OPTARG" = max ]; then
    3.32 -	  MAXTHREADS=0
    3.33 -	else
    3.34 +          MAXTHREADS=0
    3.35 +        else
    3.36            check_number "$OPTARG"
    3.37            MAXTHREADS="$OPTARG"
    3.38 -	fi
    3.39 +        fi
    3.40          ;;
    3.41        P)
    3.42          RPATH="$OPTARG"
    3.43          ;;
    3.44 +      Q)
    3.45 +        PARALLEL_PROOFS="$OPTARG"
    3.46 +        ;;
    3.47        T)
    3.48          check_number "$OPTARG"
    3.49          TRACETHREADS="$OPTARG"
    3.50 @@ -232,7 +237,7 @@
    3.51    [ "$COMPRESS" = true ] && OPT_C="-c"
    3.52  
    3.53    "$ISABELLE_PROCESS" \
    3.54 -    -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;" \
    3.55 +    -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;" \
    3.56      $OPT_C -q -w $LOGIC $NAME > "$LOG"
    3.57    RC="$?"
    3.58  else
    3.59 @@ -241,7 +246,7 @@
    3.60    LOG="$LOGDIR/$ITEM"
    3.61  
    3.62    "$ISABELLE_PROCESS" \
    3.63 -    -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();" \
    3.64 +    -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();" \
    3.65      -r -q "$LOGIC" > "$LOG"
    3.66    RC="$?"
    3.67    cd ..

     4.1 --- a/src/Pure/Isar/proof.ML	Sat Jan 10 16:58:56 2009 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Sat Jan 10 21:32:30 2009 +0100
     4.3 @@ -1041,7 +1041,7 @@
     4.4  local
     4.5  
     4.6  fun future_terminal_proof proof1 proof2 meths int state =
     4.7 -  if int orelse is_relevant state orelse not (Future.enabled ())
     4.8 +  if int orelse is_relevant state orelse not (Future.enabled () andalso ! Goal.parallel_proofs)
     4.9    then proof1 meths state
    4.10    else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
    4.11  

     5.1 --- a/src/Pure/Isar/session.ML	Sat Jan 10 16:58:56 2009 +0100
     5.2 +++ b/src/Pure/Isar/session.ML	Sat Jan 10 21:32:30 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      Pure/Isar/session.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7  
     5.8  Session management -- maintain state of logic images.
     5.9 @@ -11,7 +10,7 @@
    5.10    val name: unit -> string
    5.11    val welcome: unit -> string
    5.12    val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
    5.13 -    string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
    5.14 +    string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
    5.15    val finish: unit -> unit
    5.16  end;
    5.17  
    5.18 @@ -87,7 +86,7 @@
    5.19    | dumping (cp, path) = SOME (cp, Path.explode path);
    5.20  
    5.21  fun use_dir root build modes reset info doc doc_graph doc_versions
    5.22 -    parent name dump rpath level verbose max_threads trace_threads =
    5.23 +    parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
    5.24    ((fn () =>
    5.25       (init reset parent name;
    5.26        Present.init build info doc doc_graph doc_versions (path ()) name
    5.27 @@ -96,6 +95,7 @@
    5.28        finish ()))
    5.29      |> setmp_noncritical Proofterm.proofs level
    5.30      |> setmp_noncritical print_mode (modes @ print_mode_value ())
    5.31 +    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
    5.32      |> setmp_noncritical Multithreading.trace trace_threads
    5.33      |> setmp_noncritical Multithreading.max_threads
    5.34        (if Multithreading.available then max_threads

     6.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Jan 10 16:58:56 2009 +0100
     6.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Jan 10 21:32:30 2009 +0100
     6.3 @@ -34,7 +34,8 @@
     6.4    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
     6.5  
     6.6  fun prove ctxt xs asms prop tac =
     6.7 -  (if Future.enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     6.8 +  (if Future.enabled () andalso ! Goal.parallel_proofs then Goal.prove_future else Goal.prove)
     6.9 +    ctxt xs asms prop
    6.10      (fn args => fn st =>
    6.11        if ! quick_and_dirty
    6.12        then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st

     7.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jan 10 16:58:56 2009 +0100
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jan 10 21:32:30 2009 +0100
     7.3 @@ -745,7 +745,7 @@
     7.4    let
     7.5      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
     7.6  
     7.7 -    val immediate = not (Future.enabled ());
     7.8 +    val immediate = not (Future.enabled () andalso ! Goal.parallel_proofs);
     7.9      val (results, end_state) = fold_map (proof_result immediate) input toplevel;
    7.10      val _ =
    7.11        (case end_state of

     8.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Jan 10 16:58:56 2009 +0100
     8.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Jan 10 21:32:30 2009 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      Pure/ProofGeneral/preferences.ML
     8.5 -    ID:         $Id$
     8.6      Author:     David Aspinall and Markus Wenzel
     8.7  
     8.8  User preferences for Isabelle which are maintained by the interface.
     8.9 @@ -164,7 +163,10 @@
    8.10    proof_pref,
    8.11    nat_pref Multithreading.max_threads
    8.12      "max-threads"
    8.13 -    "Maximum number of threads"];
    8.14 +    "Maximum number of threads",
    8.15 +  bool_pref Goal.parallel_proofs
    8.16 +    "parallel-proofs"
    8.17 +    "Check proofs in parallel"];
    8.18  
    8.19  val pure_preferences =
    8.20   [("Display", display_preferences),

     9.1 --- a/src/Pure/goal.ML	Sat Jan 10 16:58:56 2009 +0100
     9.2 +++ b/src/Pure/goal.ML	Sat Jan 10 21:32:30 2009 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  signature BASIC_GOAL =
     9.6  sig
     9.7 +  val parallel_proofs: bool ref
     9.8    val SELECT_GOAL: tactic -> int -> tactic
     9.9    val CONJUNCTS: tactic -> int -> tactic
    9.10    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    9.11 @@ -123,6 +124,8 @@
    9.12        |> fold (Thm.elim_implies o Thm.assume) assms;
    9.13    in local_result end;
    9.14  
    9.15 +val parallel_proofs = ref true;
    9.16 +
    9.17  
    9.18  
    9.19  (** tactical theorem proving **)
    9.20 @@ -172,7 +175,8 @@
    9.21              else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
    9.22            end);
    9.23      val res =
    9.24 -      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
    9.25 +      if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse
    9.26 +        not (Future.enabled () andalso ! parallel_proofs)
    9.27        then result ()
    9.28        else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
    9.29    in