475 -d FORMAT build document as FORMAT (default false) |
475 -d FORMAT build document as FORMAT (default false) |
476 -f NAME use ML file NAME (default ROOT.ML) |
476 -f NAME use ML file NAME (default ROOT.ML) |
477 -g BOOL generate session graph image for document (default false) |
477 -g BOOL generate session graph image for document (default false) |
478 -i BOOL generate theory browser information (default false) |
478 -i BOOL generate theory browser information (default false) |
479 -m MODE add print mode for output |
479 -m MODE add print mode for output |
480 -p LEVEL set level of detail for proof objects |
480 -p LEVEL set level of detail for proof objects (default 0) |
|
481 -q LEVEL set level of parallel proof checking (default 1) |
481 -r reset session path |
482 -r reset session path |
482 -s NAME override session NAME |
483 -s NAME override session NAME |
483 -t BOOL internal session timing (default false) |
484 -t BOOL internal session timing (default false) |
484 -v BOOL be verbose (default false) |
485 -v BOOL be verbose (default false) |
485 |
486 |
578 facilitates debugging of serious {\LaTeX} errors, for example. |
579 facilitates debugging of serious {\LaTeX} errors, for example. |
579 |
580 |
580 \medskip The \verb|-p| option determines the level of detail |
581 \medskip The \verb|-p| option determines the level of detail |
581 for internal proof objects, see also the \emph{Isabelle Reference |
582 for internal proof objects, see also the \emph{Isabelle Reference |
582 Manual}~\cite{isabelle-ref}. |
583 Manual}~\cite{isabelle-ref}. |
|
584 |
|
585 \medskip The \verb|-q| option specifies the level of parallel |
|
586 proof checking: \verb|0| no proofs, \verb|1| toplevel |
|
587 proofs (default), \verb|2| toplevel and nested Isar proofs. |
|
588 The resulting speedup may vary, depending on the number of worker |
|
589 threads, granularity of proofs, and whether proof terms are enabled. |
583 |
590 |
584 \medskip The \verb|-t| option produces a more detailed |
591 \medskip The \verb|-t| option produces a more detailed |
585 internal timing report of the session. |
592 internal timing report of the session. |
586 |
593 |
587 \medskip The \verb|-v| option causes additional information |
594 \medskip The \verb|-v| option causes additional information |
597 concerning the internal locking and scheduling in multithreaded |
604 concerning the internal locking and scheduling in multithreaded |
598 operation. This may be helpful in isolating performance |
605 operation. This may be helpful in isolating performance |
599 bottle-necks, e.g.\ due to excessive wait states when locking |
606 bottle-necks, e.g.\ due to excessive wait states when locking |
600 critical code sections. |
607 critical code sections. |
601 |
608 |
602 \medskip The \verb|-Q| option tells whether individual proofs |
|
603 should be checked in parallel; the default is \verb|true|. |
|
604 Note that fine-grained proof parallelism requires considerable |
|
605 amounts of extra memory, since full proof context information is |
|
606 maintained for each independent derivation thread, until checking is |
|
607 completed. |
|
608 |
|
609 \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session |
609 \medskip Any \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} session is named by some \emph{session |
610 identifier}. These accumulate, documenting the way sessions depend |
610 identifier}. These accumulate, documenting the way sessions depend |
611 on others. For example, consider \verb|Pure/FOL/ex|, which |
611 on others. For example, consider \verb|Pure/FOL/ex|, which |
612 refers to the examples of FOL, which in turn is built upon Pure. |
612 refers to the examples of FOL, which in turn is built upon Pure. |
613 |
613 |