added usedir -M max (alias for -M 0);
authorwenzelm
Wed, 02 Jan 2008 16:32:52 +0100
changeset 2577428fac5c2af54
parent 25773 0d585d756745
child 25775 90525e67ede7
added usedir -M max (alias for -M 0);
doc-src/System/present.tex
lib/Tools/usedir
     1.1 --- a/doc-src/System/present.tex	Wed Jan 02 16:17:49 2008 +0100
     1.2 +++ b/doc-src/System/present.tex	Wed Jan 02 16:32:52 2008 +0100
     1.3 @@ -469,14 +469,14 @@
     1.4  
     1.5  \medskip The \texttt{-M} option specifies the maximum number of
     1.6  parallel threads used for processing independent theory files
     1.7 -(multithreading only works on suitable ML platforms).  When tuning the
     1.8 -performance of large Isabelle sessions, the number of actual CPU cores
     1.9 -of the underlying hardware is a good starting point for option
    1.10 -\texttt{-M}.  The \texttt{-T} option determines the level of detail in
    1.11 -tracing output concerning the internal locking and scheduling in
    1.12 -multithreaded operation.  This may be helpful in isolating performance
    1.13 -bottle-necks, e.g.\ due to excessive wait states when locking critical
    1.14 -code sections.
    1.15 +(multithreading only works on suitable ML platforms).  The special
    1.16 +value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of
    1.17 +actual CPU cores of the underlying machine, which is a good starting
    1.18 +point for optimal performance tuning.  The \texttt{-T} option
    1.19 +determines the level of detail in tracing output concerning the
    1.20 +internal locking and scheduling in multithreaded operation.  This may
    1.21 +be helpful in isolating performance bottle-necks, e.g.\ due to
    1.22 +excessive wait states when locking critical code sections.
    1.23  
    1.24  \medskip Any \texttt{usedir} session is named by some \emph{session
    1.25    identifier}. These accumulate, documenting the way sessions depend on
     2.1 --- a/lib/Tools/usedir	Wed Jan 02 16:17:49 2008 +0100
     2.2 +++ b/lib/Tools/usedir	Wed Jan 02 16:32:52 2008 +0100
     2.3 @@ -96,8 +96,12 @@
     2.4          DUMP="$OPTARG"
     2.5          ;;
     2.6        M)
     2.7 -        check_number "$OPTARG"
     2.8 -        MAXTHREADS="$OPTARG"
     2.9 +        if [ "$OPTARG" = max ]; then
    2.10 +	  MAXTHREADS=0
    2.11 +	else
    2.12 +          check_number "$OPTARG"
    2.13 +          MAXTHREADS="$OPTARG"
    2.14 +	fi
    2.15          ;;
    2.16        P)
    2.17          RPATH="$OPTARG"