doc-src/System/present.tex
changeset 24177 9229d09363c0
parent 20571 cbcca0d536bf
child 24975 592a5d8700a7
equal deleted inserted replaced
24176:9620a57a5a57 24177:9229d09363c0
   359 Usage: usedir [OPTIONS] LOGIC NAME
   359 Usage: usedir [OPTIONS] LOGIC NAME
   360 
   360 
   361   Options are:
   361   Options are:
   362     -C BOOL      copy existing document directory to -D PATH (default true)
   362     -C BOOL      copy existing document directory to -D PATH (default true)
   363     -D PATH      dump generated document sources into PATH
   363     -D PATH      dump generated document sources into PATH
       
   364     -M MAX       multithreading: maximum number of worker threads (default 1)
   364     -P PATH      set path for remote theory browsing information
   365     -P PATH      set path for remote theory browsing information
       
   366     -T LEVEL     multithreading: trace level (default 0)
   365     -V VERSION   declare alternative document VERSION
   367     -V VERSION   declare alternative document VERSION
   366     -b           build mode (output heap image, using current dir)
   368     -b           build mode (output heap image, using current dir)
   367     -c BOOL      tell ML system to compress output image (default true)
   369     -c BOOL      tell ML system to compress output image (default true)
   368     -d FORMAT    build document as FORMAT (default false)
   370     -d FORMAT    build document as FORMAT (default false)
   369     -f NAME      use ML file NAME (default ROOT.ML)
   371     -f NAME      use ML file NAME (default ROOT.ML)
   458   Manual}~\cite{isabelle-ref}.
   460   Manual}~\cite{isabelle-ref}.
   459 
   461 
   460 \medskip The \texttt{-v} option causes additional information to be printed
   462 \medskip The \texttt{-v} option causes additional information to be printed
   461 while running the session, notably the location of prepared documents.
   463 while running the session, notably the location of prepared documents.
   462 
   464 
       
   465 \medskip The \texttt{-M} option specifies the maximum number of
       
   466 parallel threads used for processing independent theory files
       
   467 (multithreading only works on suitable ML platforms).  When tuning the
       
   468 performance of large Isabelle sessions, the number of actual CPU cores
       
   469 of the underlying hardware is a good starting point for option
       
   470 \texttt{-M}.  The \texttt{-T} option determines the level of detail in
       
   471 tracing output concerning the internal locking and scheduling in
       
   472 multithreaded operation.  This may be helpful in isolating performance
       
   473 bottle-necks, e.g.\ due to excessive wait states when locking critical
       
   474 code sections.
       
   475 
   463 \medskip Any \texttt{usedir} session is named by some \emph{session
   476 \medskip Any \texttt{usedir} session is named by some \emph{session
   464   identifier}. These accumulate, documenting the way sessions depend on
   477   identifier}. These accumulate, documenting the way sessions depend on
   465 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   478 others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
   466 examples of FOL, which in turn is built upon Pure.
   479 examples of FOL, which in turn is built upon Pure.
   467 
   480