--- a/NEWS Mon Oct 09 19:10:52 2017 +0200
+++ b/NEWS Wed Oct 11 20:16:00 2017 +0200
@@ -69,6 +69,7 @@
* Command-line tool "isabelle build" supports new options:
- option -B NAME: include session NAME and all descendants
- option -S: only observe changes of sources, not heap images
+ - option -f: forces a fresh build
New in Isabelle2017 (October 2017)
--- a/src/Doc/System/Sessions.thy Mon Oct 09 19:10:52 2017 +0200
+++ b/src/Doc/System/Sessions.thy Wed Oct 11 20:16:00 2017 +0200
@@ -280,6 +280,7 @@
-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)
-k KEYWORD check theory sources for conflicts with proposed keywords
@@ -365,6 +366,10 @@
performing the specified build operation.
\<^medskip>
+ 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.
--- a/src/Pure/Tools/build.scala Mon Oct 09 19:10:52 2017 +0200
+++ b/src/Pure/Tools/build.scala Wed Oct 11 20:16:00 2017 +0200
@@ -354,6 +354,7 @@
max_jobs: Int = 1,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
+ fresh_build: Boolean = false,
no_build: Boolean = false,
soft_build: Boolean = false,
system_mode: Boolean = false,
@@ -396,7 +397,7 @@
verbose = verbose, list_files = list_files, check_keywords = check_keywords,
global_theories = full_sessions.global_theories).check_errors
- if (soft_build) {
+ if (soft_build && !fresh_build) {
val outdated =
selected0.flatMap(name =>
store.find_database(name) match {
@@ -571,6 +572,7 @@
using(SQLite.open_database(database))(store.read_build(_, name)) match {
case Some(build) =>
val current =
+ !fresh_build &&
build.ok &&
build.sources == sources_stamp(deps, name) &&
build.input_heaps == ancestor_heaps &&
@@ -677,6 +679,7 @@
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 check_keywords: Set[String] = Set.empty
@@ -702,6 +705,7 @@
-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)
-k KEYWORD check theory sources for conflicts with proposed keywords
@@ -726,6 +730,7 @@
"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)),
"k:" -> (arg => check_keywords = check_keywords + arg),
@@ -761,6 +766,7 @@
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
+ fresh_build = fresh_build,
no_build = no_build,
soft_build = soft_build,
system_mode = system_mode,