changeset 70863 | d1299774543d |
parent 70862 | a4ccd277e9c4 |
child 71807 | cdfa8f027bb9 |
70862:a4ccd277e9c4 | 70863:d1299774543d |
---|---|
625 -B NAME include session NAME and all descendants |
625 -B NAME include session NAME and all descendants |
626 -D DIR include session directory and select its sessions |
626 -D DIR include session directory and select its sessions |
627 -R operate on requirements of selected sessions |
627 -R operate on requirements of selected sessions |
628 -X NAME exclude sessions from group NAME and all descendants |
628 -X NAME exclude sessions from group NAME and all descendants |
629 -a select all sessions |
629 -a select all sessions |
630 -b NAME base logic image (default "Pure") |
|
630 -d DIR include session directory |
631 -d DIR include session directory |
631 -g NAME select session group NAME |
632 -g NAME select session group NAME |
632 -l NAME logic session name (default ISABELLE_LOGIC="HOL") |
|
633 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
633 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
634 -u OPT overide update option: shortcut for "-o update_OPT" |
634 -u OPT overide update option: shortcut for "-o update_OPT" |
635 -v verbose |
635 -v verbose |
636 -x NAME exclude session NAME and all descendants |
636 -x NAME exclude session NAME and all descendants |
637 |
637 |
639 |
639 |
640 \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the |
640 \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the |
641 remaining command-line arguments specify sessions as in @{tool build} |
641 remaining command-line arguments specify sessions as in @{tool build} |
642 (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}). |
642 (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}). |
643 |
643 |
644 \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies the underlying logic image. |
644 \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies an optional base logic image, for improved |
645 scalability of the PIDE session. Its theories are only processed if it is |
|
646 included in the overall session selection. |
|
645 |
647 |
646 \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
648 \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
647 |
649 |
648 \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
650 \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
649 (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> |
651 (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> |
685 |
687 |
686 subsubsection \<open>Examples\<close> |
688 subsubsection \<open>Examples\<close> |
687 |
689 |
688 text \<open> |
690 text \<open> |
689 Update some cartouche notation in all theory sources required for session |
691 Update some cartouche notation in all theory sources required for session |
690 \<^verbatim>\<open>HOL-Analysis\<close>: |
692 \<^verbatim>\<open>HOL-Analysis\<close> (and ancestors): |
691 |
693 |
692 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>} |
694 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches HOL-Analysis\<close>} |
693 |
695 |
694 \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> --- |
696 \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> --- |
695 its image is taken as starting point and its sources are not touched: |
697 using its image is taken starting point (for reduced resource requirements): |
696 |
698 |
697 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>} |
699 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\<close>} |
698 |
|
699 \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE |
|
700 session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is |
|
701 more compact than importing all required theory (and ML) source files from |
|
702 \<^verbatim>\<open>Pure\<close>. |
|
703 |
700 |
704 \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run |
701 \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run |
705 separately with special options as follows: |
702 separately with special options as follows: |
706 |
703 |
707 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs |
704 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs |