doc-src/System/present.tex
changeset 25774 28fac5c2af54
parent 24975 592a5d8700a7
child 26908 25fb7241f32e
equal deleted inserted replaced
25773:0d585d756745 25774:28fac5c2af54
   467 \medskip The \texttt{-v} option causes additional information to be printed
   467 \medskip The \texttt{-v} option causes additional information to be printed
   468 while running the session, notably the location of prepared documents.
   468 while running the session, notably the location of prepared documents.
   469 
   469 
   470 \medskip The \texttt{-M} option specifies the maximum number of
   470 \medskip The \texttt{-M} option specifies the maximum number of
   471 parallel threads used for processing independent theory files
   471 parallel threads used for processing independent theory files
   472 (multithreading only works on suitable ML platforms).  When tuning the
   472 (multithreading only works on suitable ML platforms).  The special
   473 performance of large Isabelle sessions, the number of actual CPU cores
   473 value of ``\texttt{0}'' or ``\texttt{max}'' refers to the number of
   474 of the underlying hardware is a good starting point for option
   474 actual CPU cores of the underlying machine, which is a good starting
   475 \texttt{-M}.  The \texttt{-T} option determines the level of detail in
   475 point for optimal performance tuning.  The \texttt{-T} option
   476 tracing output concerning the internal locking and scheduling in
   476 determines the level of detail in tracing output concerning the
   477 multithreaded operation.  This may be helpful in isolating performance
   477 internal locking and scheduling in multithreaded operation.  This may
   478 bottle-necks, e.g.\ due to excessive wait states when locking critical
   478 be helpful in isolating performance bottle-necks, e.g.\ due to
   479 code sections.
   479 excessive wait states when locking critical code sections.
   480 
   480 
   481 \medskip Any \texttt{usedir} session is named by some \emph{session
   481 \medskip Any \texttt{usedir} session is named by some \emph{session
   482   identifier}. These accumulate, documenting the way sessions depend on
   482   identifier}. These accumulate, documenting the way sessions depend on
   483 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   483 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   484 examples of FOL, which in turn is built upon Pure.
   484 examples of FOL, which in turn is built upon Pure.