--- a/NEWS Thu Jan 05 22:30:20 2023 +0100
+++ b/NEWS Fri Jan 06 12:05:32 2023 +0100
@@ -193,8 +193,8 @@
* 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".
+scalable, and supports most 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
--- a/src/Doc/System/Sessions.thy Thu Jan 05 22:30:20 2023 +0100
+++ b/src/Doc/System/Sessions.thy Fri Jan 06 12:05:32 2023 +0100
@@ -476,10 +476,10 @@
Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
requirements.
- \<^medskip>
- Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
- (including optional cleanup). Note that the return code always indicates the
- status of the set of selected sessions.
+ \<^medskip> Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
+ (including optional cleanup). The overall return code always the status of
+ the set of selected sessions. Add-on builds (like presentation) are run for
+ successful sessions, i.e.\ already finished ones.
\<^medskip>
Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
@@ -784,7 +784,10 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
+ -b build heap images
+ -c clean build
-d DIR include session directory
+ -f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-l NAME additional base logic
@@ -794,26 +797,15 @@
-v verbose
-x NAME exclude session NAME and all descendants
- Update theory sources based on PIDE markup.\<close>}
+ Update theory sources based on PIDE markup produced by "isabelle build".\<close>}
- \<^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}).
-
- \<^medskip> Options \<^verbatim>\<open>-N\<close> and \<^verbatim>\<open>-j\<close> specify multicore parameters as in @{tool build}.
-
- \<^medskip> Option \<^verbatim>\<open>-n\<close> suppresses the actual build process, but existing build
- databases are used nonetheless.
+ \<^medskip> Most options are the same as for @{tool build} (\secref{sec:tool-build}).
\<^medskip> Option \<^verbatim>\<open>-l\<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.
-
- \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
- (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
- options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
- ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
+ \<^medskip> Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> options, by relying on naming
+ convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
\<^medskip> The following \<^verbatim>\<open>update\<close> options are supported:
--- a/src/Pure/Tools/update.scala Thu Jan 05 22:30:20 2023 +0100
+++ b/src/Pure/Tools/update.scala Fri Jan 06 12:05:32 2023 +0100
@@ -12,10 +12,13 @@
selection: Sessions.Selection = Sessions.Selection.empty,
base_logics: List[String] = Nil,
progress: Progress = new Progress,
+ build_heap: Boolean = false,
+ clean_build: Boolean = false,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
numa_shuffling: Boolean = false,
max_jobs: Int = 1,
+ fresh_build: Boolean = false,
no_build: Boolean = false,
verbose: Boolean = false
): Build.Results = {
@@ -117,7 +120,10 @@
var requirements = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
+ var build_heap = false
+ var clean_build = false
var dirs: List[Path] = Nil
+ var fresh_build = false
var session_groups: List[String] = Nil
var max_jobs = 1
var base_logics: List[String] = Nil
@@ -135,7 +141,10 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
+ -b build heap images
+ -c clean build
-d DIR include session directory
+ -f fresh build
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
-l NAME additional base logic
@@ -145,7 +154,7 @@
-v verbose
-x NAME exclude session NAME and all descendants
- Update theory sources based on PIDE markup.
+ Update theory sources based on PIDE markup produced by "isabelle build".
""",
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
@@ -153,7 +162,10 @@
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
+ "b" -> (_ => build_heap = true),
+ "c" -> (_ => clean_build = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "f" -> (_ => fresh_build = true),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
"l:" -> (arg => base_logics ::= arg),
@@ -180,10 +192,13 @@
sessions = sessions),
base_logics = base_logics,
progress = progress,
+ build_heap,
+ clean_build,
dirs = dirs,
select_dirs = select_dirs,
numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
max_jobs = max_jobs,
+ fresh_build,
no_build = no_build,
verbose = verbose)
}