src/Pure/Tools/build.scala
changeset 66745 e7ac579b883c
parent 66744 fec1504e5f03
child 66746 888a51e77c6e
     1.1 --- a/src/Pure/Tools/build.scala	Sun Oct 01 20:50:26 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
     1.3 @@ -353,6 +353,7 @@
     1.4      list_files: Boolean = false,
     1.5      check_keywords: Set[String] = Set.empty,
     1.6      no_build: Boolean = false,
     1.7 +    soft_build: Boolean = false,
     1.8      system_mode: Boolean = false,
     1.9      verbose: Boolean = false,
    1.10      pide: Boolean = false,
    1.11 @@ -365,27 +366,59 @@
    1.12      sessions: List[String] = Nil,
    1.13      selection: Sessions.Selection = Sessions.Selection.empty): Results =
    1.14    {
    1.15 -    /* session selection and dependencies */
    1.16 +    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    1.17  
    1.18 -    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    1.19 +    val store = Sessions.store(system_mode)
    1.20 +
    1.21 +
    1.22 +    /* session selection and dependencies */
    1.23  
    1.24      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    1.25  
    1.26 -    val (selected, selected_sessions) =
    1.27 -      full_sessions.selection(
    1.28 -          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    1.29 -            exclude_sessions, session_groups, sessions) ++ selection)
    1.30 -
    1.31 -    val deps =
    1.32 -      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    1.33 -        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    1.34 -        global_theories = full_sessions.global_theories).check_errors
    1.35 -
    1.36 -    def imported_sources_stamp(name: String): List[String] =
    1.37 +    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    1.38        deps.imported_sources(name).map(_.toString).sorted
    1.39  
    1.40 -    def sources_stamp(name: String): List[String] =
    1.41 -      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    1.42 +    def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    1.43 +      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    1.44 +
    1.45 +    val (selected, selected_sessions, deps) =
    1.46 +    {
    1.47 +      val (selected0, selected_sessions0) =
    1.48 +        full_sessions.selection(
    1.49 +            Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    1.50 +              exclude_sessions, session_groups, sessions) ++ selection)
    1.51 +
    1.52 +      val deps0 =
    1.53 +        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
    1.54 +          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    1.55 +          global_theories = full_sessions.global_theories).check_errors
    1.56 +
    1.57 +      if (soft_build) {
    1.58 +        val outdated =
    1.59 +          selected0.flatMap(name =>
    1.60 +            store.find_database(name) match {
    1.61 +              case Some(database) =>
    1.62 +                using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.63 +                  case Some(build)
    1.64 +                  if build.return_code == 0 &&
    1.65 +                    build.imported_sources == imported_sources_stamp(deps0, name) &&
    1.66 +                    build.sources == sources_stamp(deps0, name) => None
    1.67 +                  case _ => Some(name)
    1.68 +                }
    1.69 +              case None => Some(name)
    1.70 +            })
    1.71 +        val (selected, selected_sessions) =
    1.72 +          full_sessions.selection(Sessions.Selection(sessions = outdated))
    1.73 +        val deps =
    1.74 +          Sessions.deps(selected_sessions, inlined_files = true,
    1.75 +            global_theories = full_sessions.global_theories).check_errors
    1.76 +        (selected, selected_sessions, deps)
    1.77 +      }
    1.78 +      else (selected0, selected_sessions0, deps0)
    1.79 +    }
    1.80 +
    1.81 +
    1.82 +    /* check unknown files */
    1.83  
    1.84      if (check_unknown_files) {
    1.85        val source_files =
    1.86 @@ -403,7 +436,6 @@
    1.87  
    1.88      /* main build process */
    1.89  
    1.90 -    val store = Sessions.store(system_mode)
    1.91      val queue = Queue(progress, selected_sessions, store)
    1.92  
    1.93      store.prepare_output()
    1.94 @@ -506,8 +538,8 @@
    1.95                          command_timings = true, ml_statistics = true, task_statistics = true),
    1.96                    build =
    1.97                      Session_Info(
    1.98 -                      imported_sources_stamp(name),
    1.99 -                      sources_stamp(name),
   1.100 +                      imported_sources_stamp(deps, name),
   1.101 +                      sources_stamp(deps, name),
   1.102                        input_heaps,
   1.103                        heap_stamp,
   1.104                        process_result.rc)))
   1.105 @@ -543,7 +575,7 @@
   1.106                          case Some(build) =>
   1.107                            val current =
   1.108                              build.return_code == 0 &&
   1.109 -                            build.sources == sources_stamp(name) &&
   1.110 +                            build.sources == sources_stamp(deps, name) &&
   1.111                              build.input_heaps == ancestor_heaps &&
   1.112                              build.output_heap == heap_stamp &&
   1.113                              !(do_output && heap_stamp.isEmpty)
   1.114 @@ -642,6 +674,7 @@
   1.115      var numa_shuffling = false
   1.116      var pide = false
   1.117      var requirements = false
   1.118 +    var soft_build = false
   1.119      var exclude_session_groups: List[String] = Nil
   1.120      var all_sessions = false
   1.121      var build_heap = false
   1.122 @@ -666,6 +699,7 @@
   1.123      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   1.124      -P           build via PIDE protocol
   1.125      -R           operate on requirements of selected sessions
   1.126 +    -S           soft build: only observe changes of sources, not heap images
   1.127      -X NAME      exclude sessions from group NAME and all descendants
   1.128      -a           select all sessions
   1.129      -b           build heap images
   1.130 @@ -689,6 +723,7 @@
   1.131        "N" -> (_ => numa_shuffling = true),
   1.132        "P" -> (_ => pide = true),
   1.133        "R" -> (_ => requirements = true),
   1.134 +      "S" -> (_ => soft_build = true),
   1.135        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   1.136        "a" -> (_ => all_sessions = true),
   1.137        "b" -> (_ => build_heap = true),
   1.138 @@ -730,6 +765,7 @@
   1.139            list_files = list_files,
   1.140            check_keywords = check_keywords,
   1.141            no_build = no_build,
   1.142 +          soft_build = soft_build,
   1.143            system_mode = system_mode,
   1.144            verbose = verbose,
   1.145            pide = pide,