672 for such ambitious applications: |
672 for such ambitious applications: |
673 @{verbatim [display] |
673 @{verbatim [display] |
674 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m" |
674 \<open>ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m" |
675 ML_OPTIONS="--minheap 4G --maxheap 32G" |
675 ML_OPTIONS="--minheap 4G --maxheap 32G" |
676 \<close>} |
676 \<close>} |
677 |
677 \<close> |
|
678 |
|
679 |
|
680 section \<open>Update theory sources based on PIDE markup \label{sec:tool-update}\<close> |
|
681 |
|
682 text \<open> |
|
683 The @{tool_def "update"} tool updates theory sources based on markup that is |
|
684 produced from a running PIDE session (similar to @{tool dump} |
|
685 \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display] |
|
686 \<open>Usage: isabelle update [OPTIONS] [SESSIONS ...] |
|
687 |
|
688 Options are: |
|
689 -B NAME include session NAME and all descendants |
|
690 -D DIR include session directory and select its sessions |
|
691 -R operate on requirements of selected sessions |
|
692 -X NAME exclude sessions from group NAME and all descendants |
|
693 -a select all sessions |
|
694 -d DIR include session directory |
|
695 -g NAME select session group NAME |
|
696 -l NAME logic session name (default ISABELLE_LOGIC="HOL") |
|
697 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
698 -s system build mode for logic image |
|
699 -u OPT overide update option: shortcut for "-o update_OPT" |
|
700 -v verbose |
|
701 -x NAME exclude session NAME and all descendants |
|
702 |
|
703 Update theory sources based on PIDE markup.\<close>} |
|
704 |
|
705 \<^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 |
|
706 remaining command-line arguments specify sessions as in @{tool build} |
|
707 (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}). |
|
708 |
|
709 \<^medskip> Options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-s\<close> specify the underlying logic image is in @{tool |
|
710 dump} (\secref{sec:tool-dump}). |
|
711 |
|
712 \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. |
|
713 |
|
714 \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build} |
|
715 (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> |
|
716 options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for |
|
717 ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''. |
|
718 |
|
719 \<^medskip> The following update options are supported: |
|
720 |
|
721 \<^item> @{system_option update_inner_syntax_cartouches} to update inner syntax |
|
722 (types, terms, etc.)~to use cartouches, instead of double-quoted strings |
|
723 or atomic identifiers. For example, ``\<^theory_text>\<open>lemma \<doublequote>x = |
|
724 x\<doublequote>\<close>'' is replaced by ``\<^theory_text>\<open>lemma \<open>x = x\<close>\<close>'', and ``\<^theory_text>\<open>fix x\<close>'' |
|
725 is replaced by ``\<^theory_text>\<open>fix \<open>x\<close>\<close>''. |
|
726 |
|
727 \<^item> @{system_option update_mixfix_cartouches} to update mixfix templates to |
|
728 use cartouches instead of double-quoted strings. For example, ``\<^theory_text>\<open>(infixl |
|
729 \<doublequote>+\<doublequote> 65)\<close>'' is replaced by ``\<^theory_text>\<open>(infixl \<open>+\<close> |
|
730 65)\<close>''. |
|
731 |
|
732 \<^item> @{system_option update_control_cartouches} to update antiquotations to |
|
733 use the compact form with control symbol and cartouche argument. For |
|
734 example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by |
|
735 ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.) |
|
736 |
|
737 It is also possible to produce custom updates in Isabelle/ML, by reporting |
|
738 \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement |
|
739 text. This operation should be made conditional on specific system options, |
|
740 similar to the ones above. Searching the above option names in ML sources of |
|
741 \<^dir>\<open>$ISABELLE_HOME/src/Pure\<close> provides some examples. |
|
742 |
|
743 Different update options can be in conflict by producing overlapping edits: |
|
744 this may require to run @{tool update} multiple times, but it is often |
|
745 better to enable particular update options separately and commit the changes |
|
746 one-by-one. |
|
747 \<close> |
|
748 |
|
749 |
|
750 subsubsection \<open>Examples\<close> |
|
751 |
|
752 text \<open> |
|
753 Update some cartouche notation in all theory sources required for session |
|
754 \<^verbatim>\<open>HOL-Analysis\<close>: |
|
755 |
|
756 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>} |
|
757 |
|
758 \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> --- |
|
759 its image is taken as starting point and its sources are not touched: |
|
760 |
|
761 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>} |
|
762 |
|
763 \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE |
|
764 session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is |
|
765 more compact than importing all required theory (and ML) source files from |
|
766 \<^verbatim>\<open>Pure\<close>. |
|
767 |
|
768 \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run |
|
769 separately with special options as follows: |
|
770 |
|
771 @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs |
|
772 -o record_proofs=2 -o parallel_proofs=0\<close>} |
|
773 |
|
774 \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing |
|
775 Isabelle/ML heap sizes for very big PIDE processes that include many |
|
776 sessions, notably from the Archive of Formal Proofs. |
678 \<close> |
777 \<close> |
679 |
778 |
680 end |
779 end |