added isablle build option -f;
authorwenzelm
Wed Oct 11 20:16:00 2017 +0200 (19 months ago)
changeset 668415c32a072ca8b
parent 66840 0d689d71dbdc
child 66842 7ded55dd2a55
added isablle build option -f;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Mon Oct 09 19:10:52 2017 +0200
     1.2 +++ b/NEWS	Wed Oct 11 20:16:00 2017 +0200
     1.3 @@ -69,6 +69,7 @@
     1.4  * Command-line tool "isabelle build" supports new options:
     1.5    - option -B NAME: include session NAME and all descendants
     1.6    - option -S: only observe changes of sources, not heap images
     1.7 +  - option -f: forces a fresh build
     1.8  
     1.9  
    1.10  New in Isabelle2017 (October 2017)
     2.1 --- a/src/Doc/System/Sessions.thy	Mon Oct 09 19:10:52 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Wed Oct 11 20:16:00 2017 +0200
     2.3 @@ -280,6 +280,7 @@
     2.4      -b           build heap images
     2.5      -c           clean build
     2.6      -d DIR       include session directory
     2.7 +    -f           fresh build
     2.8      -g NAME      select session group NAME
     2.9      -j INT       maximum number of parallel jobs (default 1)
    2.10      -k KEYWORD   check theory sources for conflicts with proposed keywords
    2.11 @@ -365,6 +366,10 @@
    2.12    performing the specified build operation.
    2.13  
    2.14    \<^medskip>
    2.15 +  Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
    2.16 +  requirements.
    2.17 +
    2.18 +  \<^medskip>
    2.19    Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
    2.20    (including optional cleanup). Note that the return code always indicates the
    2.21    status of the set of selected sessions.
     3.1 --- a/src/Pure/Tools/build.scala	Mon Oct 09 19:10:52 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Wed Oct 11 20:16:00 2017 +0200
     3.3 @@ -354,6 +354,7 @@
     3.4      max_jobs: Int = 1,
     3.5      list_files: Boolean = false,
     3.6      check_keywords: Set[String] = Set.empty,
     3.7 +    fresh_build: Boolean = false,
     3.8      no_build: Boolean = false,
     3.9      soft_build: Boolean = false,
    3.10      system_mode: Boolean = false,
    3.11 @@ -396,7 +397,7 @@
    3.12            verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    3.13            global_theories = full_sessions.global_theories).check_errors
    3.14  
    3.15 -      if (soft_build) {
    3.16 +      if (soft_build && !fresh_build) {
    3.17          val outdated =
    3.18            selected0.flatMap(name =>
    3.19              store.find_database(name) match {
    3.20 @@ -571,6 +572,7 @@
    3.21                        using(SQLite.open_database(database))(store.read_build(_, name)) match {
    3.22                          case Some(build) =>
    3.23                            val current =
    3.24 +                            !fresh_build &&
    3.25                              build.ok &&
    3.26                              build.sources == sources_stamp(deps, name) &&
    3.27                              build.input_heaps == ancestor_heaps &&
    3.28 @@ -677,6 +679,7 @@
    3.29      var build_heap = false
    3.30      var clean_build = false
    3.31      var dirs: List[Path] = Nil
    3.32 +    var fresh_build = false
    3.33      var session_groups: List[String] = Nil
    3.34      var max_jobs = 1
    3.35      var check_keywords: Set[String] = Set.empty
    3.36 @@ -702,6 +705,7 @@
    3.37      -b           build heap images
    3.38      -c           clean build
    3.39      -d DIR       include session directory
    3.40 +    -f           fresh build
    3.41      -g NAME      select session group NAME
    3.42      -j INT       maximum number of parallel jobs (default 1)
    3.43      -k KEYWORD   check theory sources for conflicts with proposed keywords
    3.44 @@ -726,6 +730,7 @@
    3.45        "b" -> (_ => build_heap = true),
    3.46        "c" -> (_ => clean_build = true),
    3.47        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    3.48 +      "f" -> (_ => fresh_build = true),
    3.49        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    3.50        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
    3.51        "k:" -> (arg => check_keywords = check_keywords + arg),
    3.52 @@ -761,6 +766,7 @@
    3.53            max_jobs = max_jobs,
    3.54            list_files = list_files,
    3.55            check_keywords = check_keywords,
    3.56 +          fresh_build = fresh_build,
    3.57            no_build = no_build,
    3.58            soft_build = soft_build,
    3.59            system_mode = system_mode,