449 -d FORMAT build document as FORMAT (default false) |
449 -d FORMAT build document as FORMAT (default false) |
450 -f NAME use ML file NAME (default ROOT.ML) |
450 -f NAME use ML file NAME (default ROOT.ML) |
451 -g BOOL generate session graph image for document (default false) |
451 -g BOOL generate session graph image for document (default false) |
452 -i BOOL generate theory browser information (default false) |
452 -i BOOL generate theory browser information (default false) |
453 -m MODE add print mode for output |
453 -m MODE add print mode for output |
454 -p LEVEL set level of detail for proof objects |
454 -p LEVEL set level of detail for proof objects (default 0) |
|
455 -q LEVEL set level of parallel proof checking (default 1) |
455 -r reset session path |
456 -r reset session path |
456 -s NAME override session NAME |
457 -s NAME override session NAME |
457 -t BOOL internal session timing (default false) |
458 -t BOOL internal session timing (default false) |
458 -v BOOL be verbose (default false) |
459 -v BOOL be verbose (default false) |
459 |
460 |
562 |
563 |
563 \medskip The @{verbatim "-p"} option determines the level of detail |
564 \medskip The @{verbatim "-p"} option determines the level of detail |
564 for internal proof objects, see also the \emph{Isabelle Reference |
565 for internal proof objects, see also the \emph{Isabelle Reference |
565 Manual}~\cite{isabelle-ref}. |
566 Manual}~\cite{isabelle-ref}. |
566 |
567 |
|
568 \medskip The @{verbatim "-q"} option specifies the level of parallel |
|
569 proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel |
|
570 proofs (default), @{verbatim 2} toplevel and nested Isar proofs. |
|
571 The resulting speedup may vary, depending on the number of worker |
|
572 threads, granularity of proofs, and whether proof terms are enabled. |
|
573 |
567 \medskip The @{verbatim "-t"} option produces a more detailed |
574 \medskip The @{verbatim "-t"} option produces a more detailed |
568 internal timing report of the session. |
575 internal timing report of the session. |
569 |
576 |
570 \medskip The @{verbatim "-v"} option causes additional information |
577 \medskip The @{verbatim "-v"} option causes additional information |
571 to be printed while running the session, notably the location of |
578 to be printed while running the session, notably the location of |
581 concerning the internal locking and scheduling in multithreaded |
588 concerning the internal locking and scheduling in multithreaded |
582 operation. This may be helpful in isolating performance |
589 operation. This may be helpful in isolating performance |
583 bottle-necks, e.g.\ due to excessive wait states when locking |
590 bottle-necks, e.g.\ due to excessive wait states when locking |
584 critical code sections. |
591 critical code sections. |
585 |
592 |
586 \medskip The @{verbatim "-Q"} option tells whether individual proofs |
|
587 should be checked in parallel; the default is @{verbatim true}. |
|
588 Note that fine-grained proof parallelism requires considerable |
|
589 amounts of extra memory, since full proof context information is |
|
590 maintained for each independent derivation thread, until checking is |
|
591 completed. |
|
592 |
|
593 \medskip Any @{tool usedir} session is named by some \emph{session |
593 \medskip Any @{tool usedir} session is named by some \emph{session |
594 identifier}. These accumulate, documenting the way sessions depend |
594 identifier}. These accumulate, documenting the way sessions depend |
595 on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
595 on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
596 refers to the examples of FOL, which in turn is built upon Pure. |
596 refers to the examples of FOL, which in turn is built upon Pure. |
597 |
597 |