1.1 --- a/NEWS	Sun Jul 19 19:20:17 2009 +0200
     1.2 +++ b/NEWS	Sun Jul 19 19:24:04 2009 +0200
     1.3 @@ -120,6 +120,9 @@
     1.4  * Removed "compress" option from isabelle-process and isabelle usedir;
     1.5  this is always enabled.
     1.6  
     1.7 +* More fine-grained control of proof parallelism, cf.
     1.8 +Goal.parallel_proofs in ML and usedir option -q LEVEL.
     1.9 +
    1.10  
    1.11  
    1.12  New in Isabelle2009 (April 2009)

     2.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Jul 19 19:20:17 2009 +0200
     2.2 +++ b/doc-src/System/Thy/Presentation.thy	Sun Jul 19 19:24:04 2009 +0200
     2.3 @@ -451,7 +451,8 @@
     2.4      -g BOOL      generate session graph image for document (default false)
     2.5      -i BOOL      generate theory browser information (default false)
     2.6      -m MODE      add print mode for output
     2.7 -    -p LEVEL     set level of detail for proof objects
     2.8 +    -p LEVEL     set level of detail for proof objects (default 0)
     2.9 +    -q LEVEL     set level of parallel proof checking (default 1)
    2.10      -r           reset session path
    2.11      -s NAME      override session NAME
    2.12      -t BOOL      internal session timing (default false)
    2.13 @@ -564,6 +565,12 @@
    2.14    for internal proof objects, see also the \emph{Isabelle Reference
    2.15    Manual}~\cite{isabelle-ref}.
    2.16  
    2.17 +  \medskip The @{verbatim "-q"} option specifies the level of parallel
    2.18 +  proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
    2.19 +  proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
    2.20 +  The resulting speedup may vary, depending on the number of worker
    2.21 +  threads, granularity of proofs, and whether proof terms are enabled.
    2.22 +
    2.23    \medskip The @{verbatim "-t"} option produces a more detailed
    2.24    internal timing report of the session.
    2.25  
    2.26 @@ -583,13 +590,6 @@
    2.27    bottle-necks, e.g.\ due to excessive wait states when locking
    2.28    critical code sections.
    2.29  
    2.30 -  \medskip The @{verbatim "-Q"} option tells whether individual proofs
    2.31 -  should be checked in parallel; the default is @{verbatim true}.
    2.32 -  Note that fine-grained proof parallelism requires considerable
    2.33 -  amounts of extra memory, since full proof context information is
    2.34 -  maintained for each independent derivation thread, until checking is
    2.35 -  completed.
    2.36 -
    2.37    \medskip Any @{tool usedir} session is named by some \emph{session
    2.38    identifier}. These accumulate, documenting the way sessions depend
    2.39    on others. For example, consider @{verbatim "Pure/FOL/ex"}, which

     3.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sun Jul 19 19:20:17 2009 +0200
     3.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Sun Jul 19 19:24:04 2009 +0200
     3.3 @@ -477,7 +477,8 @@
     3.4      -g BOOL      generate session graph image for document (default false)
     3.5      -i BOOL      generate theory browser information (default false)
     3.6      -m MODE      add print mode for output
     3.7 -    -p LEVEL     set level of detail for proof objects
     3.8 +    -p LEVEL     set level of detail for proof objects (default 0)
     3.9 +    -q LEVEL     set level of parallel proof checking (default 1)
    3.10      -r           reset session path
    3.11      -s NAME      override session NAME
    3.12      -t BOOL      internal session timing (default false)
    3.13 @@ -581,6 +582,12 @@
    3.14    for internal proof objects, see also the \emph{Isabelle Reference
    3.15    Manual}~\cite{isabelle-ref}.
    3.16  
    3.17 +  \medskip The \verb|-q| option specifies the level of parallel
    3.18 +  proof checking: \verb|0| no proofs, \verb|1| toplevel
    3.19 +  proofs (default), \verb|2| toplevel and nested Isar proofs.
    3.20 +  The resulting speedup may vary, depending on the number of worker
    3.21 +  threads, granularity of proofs, and whether proof terms are enabled.
    3.22 +
    3.23    \medskip The \verb|-t| option produces a more detailed
    3.24    internal timing report of the session.
    3.25  
    3.26 @@ -599,13 +606,6 @@
    3.27    bottle-necks, e.g.\ due to excessive wait states when locking
    3.28    critical code sections.
    3.29  
    3.30 -  \medskip The \verb|-Q| option tells whether individual proofs
    3.31 -  should be checked in parallel; the default is \verb|true|.
    3.32 -  Note that fine-grained proof parallelism requires considerable
    3.33 -  amounts of extra memory, since full proof context information is
    3.34 -  maintained for each independent derivation thread, until checking is
    3.35 -  completed.
    3.36 -
    3.37    \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session
    3.38    identifier}. These accumulate, documenting the way sessions depend
    3.39    on others. For example, consider \verb|Pure/FOL/ex|, which

     4.1 --- a/etc/settings	Sun Jul 19 19:20:17 2009 +0200
     4.2 +++ b/etc/settings	Sun Jul 19 19:24:04 2009 +0200
     4.3 @@ -96,7 +96,7 @@
     4.4  
     4.5  # Specifically for the HOL image
     4.6  HOL_USEDIR_OPTIONS=""
     4.7 -#HOL_USEDIR_OPTIONS="-p 2 -Q false"
     4.8 +#HOL_USEDIR_OPTIONS="-p 2 -q 1"
     4.9  
    4.10  #Source file identification (default: full name + date stamp)
    4.11  ISABELLE_FILE_IDENT=""

     5.1 --- a/lib/Tools/usedir	Sun Jul 19 19:20:17 2009 +0200
     5.2 +++ b/lib/Tools/usedir	Sun Jul 19 19:24:04 2009 +0200
     5.3 @@ -19,7 +19,6 @@
     5.4    echo "    -D PATH      dump generated document sources into PATH"
     5.5    echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
     5.6    echo "    -P PATH      set path for remote theory browsing information"
     5.7 -  echo "    -Q BOOL      check proofs in parallel (default true)"
     5.8    echo "    -T LEVEL     multithreading: trace level (default 0)"
     5.9    echo "    -V VERSION   declare alternative document VERSION"
    5.10    echo "    -b           build mode (output heap image, using current dir)"
    5.11 @@ -28,7 +27,8 @@
    5.12    echo "    -g BOOL      generate session graph image for document (default false)"
    5.13    echo "    -i BOOL      generate HTML and graph browser information (default false)"
    5.14    echo "    -m MODE      add print mode for output"
    5.15 -  echo "    -p LEVEL     set level of detail for proof objects"
    5.16 +  echo "    -p LEVEL     set level of detail for proof objects (default 0)"
    5.17 +  echo "    -q LEVEL     set level of parallel proof checking (default 1)"
    5.18    echo "    -r           reset session path"
    5.19    echo "    -s NAME      override session NAME"
    5.20    echo "    -t BOOL      internal session timing (default false)"
    5.21 @@ -73,7 +73,6 @@
    5.22  DUMP=""
    5.23  MAXTHREADS="1"
    5.24  RPATH=""
    5.25 -PARALLEL_PROOFS="true"
    5.26  TRACETHREADS="0"
    5.27  DOCUMENT_VERSIONS=""
    5.28  BUILD=""
    5.29 @@ -84,14 +83,15 @@
    5.30  MODES=""
    5.31  RESET=false
    5.32  SESSION=""
    5.33 -PROOFS=0
    5.34 +PROOFS="0"
    5.35 +PARALLEL_PROOFS="1"
    5.36  TIMING=false
    5.37  VERBOSE=false
    5.38  
    5.39  function getoptions()
    5.40  {
    5.41    OPTIND=1
    5.42 -  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:rs:t:v:" OPT
    5.43 +  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    5.44    do
    5.45      case "$OPT" in
    5.46        C)
    5.47 @@ -112,9 +112,6 @@
    5.48        P)
    5.49          RPATH="$OPTARG"
    5.50          ;;
    5.51 -      Q)
    5.52 -        PARALLEL_PROOFS="$OPTARG"
    5.53 -        ;;
    5.54        T)
    5.55          check_number "$OPTARG"
    5.56          TRACETHREADS="$OPTARG"
    5.57 @@ -154,6 +151,10 @@
    5.58          check_number "$OPTARG"
    5.59          PROOFS="$OPTARG"
    5.60          ;;
    5.61 +      q)
    5.62 +        check_number "$OPTARG"
    5.63 +        PARALLEL_PROOFS="$OPTARG"
    5.64 +        ;;
    5.65        r)
    5.66          RESET=true
    5.67          ;;

     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jul 19 19:20:17 2009 +0200
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 19 19:24:04 2009 +0200
     6.3 @@ -230,7 +230,7 @@
     6.4  (* local endings *)
     6.5  
     6.6  fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
     6.7 -val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
     6.8 +val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
     6.9  val local_default_proof = Toplevel.proof Proof.local_default_proof;
    6.10  val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
    6.11  val local_done_proof = Toplevel.proof Proof.local_done_proof;

     7.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 19 19:20:17 2009 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Sun Jul 19 19:24:04 2009 +0200
     7.3 @@ -1043,7 +1043,7 @@
     7.4  local
     7.5  
     7.6  fun future_terminal_proof proof1 proof2 meths int state =
     7.7 -  if int orelse is_relevant state orelse not (Goal.future_enabled ())
     7.8 +  if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
     7.9    then proof1 meths state
    7.10    else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
    7.11  

     8.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sun Jul 19 19:20:17 2009 +0200
     8.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sun Jul 19 19:24:04 2009 +0200
     8.3 @@ -84,6 +84,12 @@
     8.4      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
     8.5    in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
     8.6  
     8.7 +val parallel_proof_pref =
     8.8 +  let
     8.9 +    fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
    8.10 +    fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
    8.11 +  in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
    8.12 +
    8.13  val thm_depsN = "thm_deps";
    8.14  val thm_deps_pref =
    8.15    let
    8.16 @@ -171,9 +177,7 @@
    8.17    nat_pref Multithreading.max_threads
    8.18      "max-threads"
    8.19      "Maximum number of threads",
    8.20 -  bool_pref Goal.parallel_proofs
    8.21 -    "parallel-proofs"
    8.22 -    "Check proofs in parallel"];
    8.23 +  parallel_proof_pref];
    8.24  
    8.25  val pure_preferences =
    8.26   [(category_display, display_preferences),

     9.1 --- a/src/Pure/System/session.ML	Sun Jul 19 19:20:17 2009 +0200
     9.2 +++ b/src/Pure/System/session.ML	Sun Jul 19 19:24:04 2009 +0200
     9.3 @@ -11,7 +11,7 @@
     9.4    val welcome: unit -> string
     9.5    val use_dir: string -> string -> bool -> string list -> bool -> bool ->
     9.6      string -> bool -> string list -> string -> string -> bool * string ->
     9.7 -    string -> int -> bool -> bool -> int -> int -> bool -> unit
     9.8 +    string -> int -> bool -> bool -> int -> int -> int -> unit
     9.9    val finish: unit -> unit
    9.10  end;
    9.11  

    10.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jul 19 19:20:17 2009 +0200
    10.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jul 19 19:24:04 2009 +0200
    10.3 @@ -350,7 +350,7 @@
    10.4      val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
    10.5        (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
    10.6  
    10.7 -    val par_proofs = ! parallel_proofs;
    10.8 +    val par_proofs = ! parallel_proofs >= 1;
    10.9  
   10.10      fun fork (name, body) tab =
   10.11        let

    11.1 --- a/src/Pure/goal.ML	Sun Jul 19 19:20:17 2009 +0200
    11.2 +++ b/src/Pure/goal.ML	Sun Jul 19 19:24:04 2009 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  
    11.5  signature BASIC_GOAL =
    11.6  sig
    11.7 -  val parallel_proofs: bool ref
    11.8 +  val parallel_proofs: int ref
    11.9    val SELECT_GOAL: tactic -> int -> tactic
   11.10    val CONJUNCTS: tactic -> int -> tactic
   11.11    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
   11.12 @@ -21,6 +21,7 @@
   11.13    val finish: thm -> thm
   11.14    val norm_result: thm -> thm
   11.15    val future_enabled: unit -> bool
   11.16 +  val local_future_enabled: unit -> bool
   11.17    val future_result: Proof.context -> thm future -> term -> thm
   11.18    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
   11.19    val prove_multi: Proof.context -> string list -> term list -> term list ->
   11.20 @@ -95,10 +96,12 @@
   11.21  
   11.22  (* future_enabled *)
   11.23  
   11.24 -val parallel_proofs = ref true;
   11.25 +val parallel_proofs = ref 1;
   11.26  
   11.27  fun future_enabled () =
   11.28 -  Future.enabled () andalso ! parallel_proofs andalso Future.is_worker ();
   11.29 +  Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
   11.30 +
   11.31 +fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
   11.32  
   11.33  
   11.34  (* future_result *)