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. |