option -S for "isabelle build";
authorwenzelm
Mon Oct 02 11:43:17 2017 +0200 (18 months ago)
changeset 66745e7ac579b883c
parent 66744 fec1504e5f03
child 66746 888a51e77c6e
option -S for "isabelle build";
NEWS
src/Doc/System/Sessions.thy
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Sun Oct 01 20:50:26 2017 +0200
     1.2 +++ b/NEWS	Mon Oct 02 11:43:17 2017 +0200
     1.3 @@ -30,8 +30,9 @@
     1.4  * Windows and Cygwin is for x86_64 only. Old 32bit platform support has
     1.5  been discontinued.
     1.6  
     1.7 -* Command-line tool "isabelle build" supports option -B for base
     1.8 -sessions: all descendants are included.
     1.9 +* Command-line tool "isabelle build" supports new options:
    1.10 +  - option -B NAME: include session NAME and all descendants
    1.11 +  - option -S: only observe changes of sources, not heap images
    1.12  
    1.13  
    1.14  New in Isabelle2017 (October 2017)
     2.1 --- a/src/Doc/System/Sessions.thy	Sun Oct 01 20:50:26 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Mon Oct 02 11:43:17 2017 +0200
     2.3 @@ -284,6 +284,7 @@
     2.4      -D DIR       include session directory and select its sessions
     2.5      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     2.6      -R           operate on requirements of selected sessions
     2.7 +    -S           soft build: only observe changes of sources, not heap images
     2.8      -X NAME      exclude sessions from group NAME and all descendants
     2.9      -a           select all sessions
    2.10      -b           build heap images
    2.11 @@ -350,6 +351,11 @@
    2.12    in the given directories.
    2.13  
    2.14    \<^medskip>
    2.15 +  Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
    2.16 +  those sessions that have changed sources (according to actually imported
    2.17 +  theories). The status of heap images is ignored.
    2.18 +
    2.19 +  \<^medskip>
    2.20    The build process depends on additional options
    2.21    (\secref{sec:system-options}) that are passed to the prover eventually. The
    2.22    settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
     3.1 --- a/src/Pure/Tools/build.scala	Sun Oct 01 20:50:26 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
     3.3 @@ -353,6 +353,7 @@
     3.4      list_files: Boolean = false,
     3.5      check_keywords: Set[String] = Set.empty,
     3.6      no_build: Boolean = false,
     3.7 +    soft_build: Boolean = false,
     3.8      system_mode: Boolean = false,
     3.9      verbose: Boolean = false,
    3.10      pide: Boolean = false,
    3.11 @@ -365,27 +366,59 @@
    3.12      sessions: List[String] = Nil,
    3.13      selection: Sessions.Selection = Sessions.Selection.empty): Results =
    3.14    {
    3.15 -    /* session selection and dependencies */
    3.16 +    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    3.17  
    3.18 -    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    3.19 +    val store = Sessions.store(system_mode)
    3.20 +
    3.21 +
    3.22 +    /* session selection and dependencies */
    3.23  
    3.24      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    3.25  
    3.26 -    val (selected, selected_sessions) =
    3.27 -      full_sessions.selection(
    3.28 -          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    3.29 -            exclude_sessions, session_groups, sessions) ++ selection)
    3.30 -
    3.31 -    val deps =
    3.32 -      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    3.33 -        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    3.34 -        global_theories = full_sessions.global_theories).check_errors
    3.35 -
    3.36 -    def imported_sources_stamp(name: String): List[String] =
    3.37 +    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    3.38        deps.imported_sources(name).map(_.toString).sorted
    3.39  
    3.40 -    def sources_stamp(name: String): List[String] =
    3.41 -      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    3.42 +    def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    3.43 +      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    3.44 +
    3.45 +    val (selected, selected_sessions, deps) =
    3.46 +    {
    3.47 +      val (selected0, selected_sessions0) =
    3.48 +        full_sessions.selection(
    3.49 +            Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    3.50 +              exclude_sessions, session_groups, sessions) ++ selection)
    3.51 +
    3.52 +      val deps0 =
    3.53 +        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
    3.54 +          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    3.55 +          global_theories = full_sessions.global_theories).check_errors
    3.56 +
    3.57 +      if (soft_build) {
    3.58 +        val outdated =
    3.59 +          selected0.flatMap(name =>
    3.60 +            store.find_database(name) match {
    3.61 +              case Some(database) =>
    3.62 +                using(SQLite.open_database(database))(store.read_build(_, name)) match {
    3.63 +                  case Some(build)
    3.64 +                  if build.return_code == 0 &&
    3.65 +                    build.imported_sources == imported_sources_stamp(deps0, name) &&
    3.66 +                    build.sources == sources_stamp(deps0, name) => None
    3.67 +                  case _ => Some(name)
    3.68 +                }
    3.69 +              case None => Some(name)
    3.70 +            })
    3.71 +        val (selected, selected_sessions) =
    3.72 +          full_sessions.selection(Sessions.Selection(sessions = outdated))
    3.73 +        val deps =
    3.74 +          Sessions.deps(selected_sessions, inlined_files = true,
    3.75 +            global_theories = full_sessions.global_theories).check_errors
    3.76 +        (selected, selected_sessions, deps)
    3.77 +      }
    3.78 +      else (selected0, selected_sessions0, deps0)
    3.79 +    }
    3.80 +
    3.81 +
    3.82 +    /* check unknown files */
    3.83  
    3.84      if (check_unknown_files) {
    3.85        val source_files =
    3.86 @@ -403,7 +436,6 @@
    3.87  
    3.88      /* main build process */
    3.89  
    3.90 -    val store = Sessions.store(system_mode)
    3.91      val queue = Queue(progress, selected_sessions, store)
    3.92  
    3.93      store.prepare_output()
    3.94 @@ -506,8 +538,8 @@
    3.95                          command_timings = true, ml_statistics = true, task_statistics = true),
    3.96                    build =
    3.97                      Session_Info(
    3.98 -                      imported_sources_stamp(name),
    3.99 -                      sources_stamp(name),
   3.100 +                      imported_sources_stamp(deps, name),
   3.101 +                      sources_stamp(deps, name),
   3.102                        input_heaps,
   3.103                        heap_stamp,
   3.104                        process_result.rc)))
   3.105 @@ -543,7 +575,7 @@
   3.106                          case Some(build) =>
   3.107                            val current =
   3.108                              build.return_code == 0 &&
   3.109 -                            build.sources == sources_stamp(name) &&
   3.110 +                            build.sources == sources_stamp(deps, name) &&
   3.111                              build.input_heaps == ancestor_heaps &&
   3.112                              build.output_heap == heap_stamp &&
   3.113                              !(do_output && heap_stamp.isEmpty)
   3.114 @@ -642,6 +674,7 @@
   3.115      var numa_shuffling = false
   3.116      var pide = false
   3.117      var requirements = false
   3.118 +    var soft_build = false
   3.119      var exclude_session_groups: List[String] = Nil
   3.120      var all_sessions = false
   3.121      var build_heap = false
   3.122 @@ -666,6 +699,7 @@
   3.123      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   3.124      -P           build via PIDE protocol
   3.125      -R           operate on requirements of selected sessions
   3.126 +    -S           soft build: only observe changes of sources, not heap images
   3.127      -X NAME      exclude sessions from group NAME and all descendants
   3.128      -a           select all sessions
   3.129      -b           build heap images
   3.130 @@ -689,6 +723,7 @@
   3.131        "N" -> (_ => numa_shuffling = true),
   3.132        "P" -> (_ => pide = true),
   3.133        "R" -> (_ => requirements = true),
   3.134 +      "S" -> (_ => soft_build = true),
   3.135        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   3.136        "a" -> (_ => all_sessions = true),
   3.137        "b" -> (_ => build_heap = true),
   3.138 @@ -730,6 +765,7 @@
   3.139            list_files = list_files,
   3.140            check_keywords = check_keywords,
   3.141            no_build = no_build,
   3.142 +          soft_build = soft_build,
   3.143            system_mode = system_mode,
   3.144            verbose = verbose,
   3.145            pide = pide,