--- a/NEWS Thu Jan 05 21:14:37 2023 +0100
+++ b/NEWS Thu Jan 05 21:14:53 2023 +0100
@@ -191,6 +191,11 @@
*** System ***
+* The command-line tool "isabelle update" is now directly based on
+"isabelle build" instead of "isabelle dump". Thus it has become more
+scalable, and supports a few additional options from "isabelle build".
+Partial builds are supported as well, e.g. "isabelle update -n -a".
+
* Isabelle/Scala provides generic support for XZ and Zstd compression,
via Compress.Options and Compress.Cache. Bytes.uncompress automatically
detects the compression scheme.
--- a/src/Doc/System/Sessions.thy Thu Jan 05 21:14:37 2023 +0100
+++ b/src/Doc/System/Sessions.thy Thu Jan 05 21:14:53 2023 +0100
@@ -774,8 +774,8 @@
text \<open>
The @{tool_def "update"} tool updates theory sources based on markup that is
- produced from a running PIDE session (similar to @{tool dump}
- \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display]
+ produced by the regular @{tool build} process \secref{sec:tool-build}). Its
+ command-line usage is: @{verbatim [display]
\<open>Usage: isabelle update [OPTIONS] [SESSIONS ...]
Options are:
@@ -784,9 +784,11 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
- -b NAME base logic image (default "Pure")
+ -b NAME additional base logic
-d DIR include session directory
-g NAME select session group NAME
+ -j INT maximum number of parallel jobs (default 1)
+ -n no build -- take existing build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u OPT override "update" option: shortcut for "-o update_OPT"
-v verbose
@@ -796,11 +798,15 @@
\<^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
remaining command-line arguments specify sessions as in @{tool build}
- (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
+ (\secref{sec:tool-build}).
+
+ \<^medskip> Options \<^verbatim>\<open>-N\<close> and \<^verbatim>\<open>-j\<close> specify multicore parameters as in @{tool build}.
- \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies an optional base logic image, for improved
- scalability of the PIDE session. Its theories are only processed if it is
- included in the overall session selection.
+ \<^medskip> Option \<^verbatim>\<open>-n\<close> suppresses the actual build process, but existing build
+ databases are used nonetheless.
+
+ \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies one or more base logics: these sessions and their
+ ancestors are \<^emph>\<open>excluded\<close> from the update.
\<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
@@ -850,20 +856,14 @@
@{verbatim [display] \<open> isabelle update -u mixfix_cartouches HOL-Analysis\<close>}
- \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
- using its image as starting point (for reduced resource requirements):
-
- @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\<close>}
+ \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close>, but
+ do not change the underlying \<^verbatim>\<open>HOL\<close> (and \<^verbatim>\<open>Pure\<close>) session:
- \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
- separately with special options as follows:
+ @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -b HOL -B HOL-Analysis\<close>}
- @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
- -o record_proofs=2\<close>}
+ \<^smallskip> Update all sessions that happen to be properly built beforehand:
- \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing
- Isabelle/ML heap sizes for very big PIDE processes that include many
- sessions, notably from the Archive of Formal Proofs.
+ @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -n -a\<close>}
\<close>