# HG changeset patch
# User wenzelm
# Date 1506937397 -7200
# Node ID e7ac579b883ce27765c5e79fc910045c5aa2fa7a
# Parent  fec1504e5f031a743486bb444030303acaf13449
option -S for "isabelle build";

diff -r fec1504e5f03 -r e7ac579b883c NEWS
--- a/NEWS	Sun Oct 01 20:50:26 2017 +0200
+++ b/NEWS	Mon Oct 02 11:43:17 2017 +0200
@@ -30,8 +30,9 @@
 * Windows and Cygwin is for x86_64 only. Old 32bit platform support has
 been discontinued.
 
-* Command-line tool "isabelle build" supports option -B for base
-sessions: all descendants are included.
+* 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
 
 
 New in Isabelle2017 (October 2017)
diff -r fec1504e5f03 -r e7ac579b883c src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Oct 01 20:50:26 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Oct 02 11:43:17 2017 +0200
@@ -284,6 +284,7 @@
     -D DIR       include session directory and select its sessions
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -R           operate on requirements of selected sessions
+    -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
@@ -350,6 +351,11 @@
   in the given directories.
 
   \<^medskip>
+  Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
+  those sessions that have changed sources (according to actually imported
+  theories). The status of heap images is ignored.
+
+  \<^medskip>
   The build process depends on additional options
   (\secref{sec:system-options}) that are passed to the prover eventually. The
   settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
diff -r fec1504e5f03 -r e7ac579b883c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Oct 01 20:50:26 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
@@ -353,6 +353,7 @@
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
     no_build: Boolean = false,
+    soft_build: Boolean = false,
     system_mode: Boolean = false,
     verbose: Boolean = false,
     pide: Boolean = false,
@@ -365,27 +366,59 @@
     sessions: List[String] = Nil,
     selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
-    /* session selection and dependencies */
+    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
 
-    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+    val store = Sessions.store(system_mode)
+
+
+    /* session selection and dependencies */
 
     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
 
-    val (selected, selected_sessions) =
-      full_sessions.selection(
-          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
-            exclude_sessions, session_groups, sessions) ++ selection)
-
-    val deps =
-      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
-        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
-        global_theories = full_sessions.global_theories).check_errors
-
-    def imported_sources_stamp(name: String): List[String] =
+    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
       deps.imported_sources(name).map(_.toString).sorted
 
-    def sources_stamp(name: String): List[String] =
-      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+    def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
+      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+
+    val (selected, selected_sessions, deps) =
+    {
+      val (selected0, selected_sessions0) =
+        full_sessions.selection(
+            Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
+              exclude_sessions, session_groups, sessions) ++ selection)
+
+      val deps0 =
+        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
+          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
+          global_theories = full_sessions.global_theories).check_errors
+
+      if (soft_build) {
+        val outdated =
+          selected0.flatMap(name =>
+            store.find_database(name) match {
+              case Some(database) =>
+                using(SQLite.open_database(database))(store.read_build(_, name)) match {
+                  case Some(build)
+                  if build.return_code == 0 &&
+                    build.imported_sources == imported_sources_stamp(deps0, name) &&
+                    build.sources == sources_stamp(deps0, name) => None
+                  case _ => Some(name)
+                }
+              case None => Some(name)
+            })
+        val (selected, selected_sessions) =
+          full_sessions.selection(Sessions.Selection(sessions = outdated))
+        val deps =
+          Sessions.deps(selected_sessions, inlined_files = true,
+            global_theories = full_sessions.global_theories).check_errors
+        (selected, selected_sessions, deps)
+      }
+      else (selected0, selected_sessions0, deps0)
+    }
+
+
+    /* check unknown files */
 
     if (check_unknown_files) {
       val source_files =
@@ -403,7 +436,6 @@
 
     /* main build process */
 
-    val store = Sessions.store(system_mode)
     val queue = Queue(progress, selected_sessions, store)
 
     store.prepare_output()
@@ -506,8 +538,8 @@
                         command_timings = true, ml_statistics = true, task_statistics = true),
                   build =
                     Session_Info(
-                      imported_sources_stamp(name),
-                      sources_stamp(name),
+                      imported_sources_stamp(deps, name),
+                      sources_stamp(deps, name),
                       input_heaps,
                       heap_stamp,
                       process_result.rc)))
@@ -543,7 +575,7 @@
                         case Some(build) =>
                           val current =
                             build.return_code == 0 &&
-                            build.sources == sources_stamp(name) &&
+                            build.sources == sources_stamp(deps, name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_stamp &&
                             !(do_output && heap_stamp.isEmpty)
@@ -642,6 +674,7 @@
     var numa_shuffling = false
     var pide = false
     var requirements = false
+    var soft_build = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
     var build_heap = false
@@ -666,6 +699,7 @@
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P           build via PIDE protocol
     -R           operate on requirements of selected sessions
+    -S           soft build: only observe changes of sources, not heap images
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
     -b           build heap images
@@ -689,6 +723,7 @@
       "N" -> (_ => numa_shuffling = true),
       "P" -> (_ => pide = true),
       "R" -> (_ => requirements = true),
+      "S" -> (_ => soft_build = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
       "b" -> (_ => build_heap = true),
@@ -730,6 +765,7 @@
           list_files = list_files,
           check_keywords = check_keywords,
           no_build = no_build,
+          soft_build = soft_build,
           system_mode = system_mode,
           verbose = verbose,
           pide = pide,