merged
authorwenzelm
Mon Oct 02 16:47:46 2017 +0200 (19 months ago)
changeset 6675478c74f9e960a
parent 66741 c90fb8bee1dd
parent 66753 f7759beab4f2
child 66755 1ceedf710564
merged
     1.1 --- a/NEWS	Mon Oct 02 03:58:55 2017 +0200
     1.2 +++ b/NEWS	Mon Oct 02 16:47:46 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/README_REPOSITORY	Mon Oct 02 03:58:55 2017 +0200
     2.2 +++ b/README_REPOSITORY	Mon Oct 02 16:47:46 2017 +0200
     2.3 @@ -300,7 +300,9 @@
     2.4    ./bin/isabelle build -a -j2 -o threads=4  #test on multiple cores (example)
     2.5  
     2.6  See also the chapter on Isabelle sessions and build management in the
     2.7 -"system" manual.
     2.8 +"system" manual. The build option -S is particularly useful for quick
     2.9 +tests of individual commits, e.g. for each step of a longer chain of
    2.10 +changes, but the final push always requires a full test as above!
    2.11  
    2.12  Note that implicit dependencies on Isabelle components are specified
    2.13  via catalog files in $ISABELLE_HOME/Admin/components/ as part of the
     3.1 --- a/src/Doc/ROOT	Mon Oct 02 03:58:55 2017 +0200
     3.2 +++ b/src/Doc/ROOT	Mon Oct 02 16:47:46 2017 +0200
     3.3 @@ -48,7 +48,6 @@
     3.4    options [document_variants = "corec"]
     3.5    sessions
     3.6      Datatypes
     3.7 -  theories [document = false] Datatypes.Setup
     3.8    theories Corec
     3.9    document_files (in "..")
    3.10      "prepare_document"
    3.11 @@ -248,9 +247,6 @@
    3.12    options [document_variants = "sugar"]
    3.13    sessions
    3.14      "HOL-Library"
    3.15 -  theories [document = false]
    3.16 -    "HOL-Library.LaTeXsugar"
    3.17 -    "HOL-Library.OptionalSugar"
    3.18    theories Sugar
    3.19    document_files (in "..")
    3.20      "prepare_document"
     4.1 --- a/src/Doc/System/Sessions.thy	Mon Oct 02 03:58:55 2017 +0200
     4.2 +++ b/src/Doc/System/Sessions.thy	Mon Oct 02 16:47:46 2017 +0200
     4.3 @@ -284,6 +284,7 @@
     4.4      -D DIR       include session directory and select its sessions
     4.5      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     4.6      -R           operate on requirements of selected sessions
     4.7 +    -S           soft build: only observe changes of sources, not heap images
     4.8      -X NAME      exclude sessions from group NAME and all descendants
     4.9      -a           select all sessions
    4.10      -b           build heap images
    4.11 @@ -350,6 +351,11 @@
    4.12    in the given directories.
    4.13  
    4.14    \<^medskip>
    4.15 +  Option \<^verbatim>\<open>-S\<close> indicates a ``soft build'': the selection is restricted to
    4.16 +  those sessions that have changed sources (according to actually imported
    4.17 +  theories). The status of heap images is ignored.
    4.18 +
    4.19 +  \<^medskip>
    4.20    The build process depends on additional options
    4.21    (\secref{sec:system-options}) that are passed to the prover eventually. The
    4.22    settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
    4.23 @@ -411,6 +417,14 @@
    4.24    @{verbatim [display] \<open>isabelle build -b -g main\<close>}
    4.25  
    4.26    \<^smallskip>
    4.27 +  Build all descendants (and requirements) of \<^verbatim>\<open>FOL\<close> and \<^verbatim>\<open>ZF\<close>:
    4.28 +  @{verbatim [display] \<open>isabelle build -B FOL -B ZF\<close>}
    4.29 +
    4.30 +  \<^smallskip>
    4.31 +  Build all sessions where sources have changed (ignoring heaps):
    4.32 +  @{verbatim [display] \<open>isabelle build -a -S\<close>}
    4.33 +
    4.34 +  \<^smallskip>
    4.35    Provide a general overview of the status of all Isabelle sessions, without
    4.36    building anything:
    4.37    @{verbatim [display] \<open>isabelle build -a -n -v\<close>}
     5.1 --- a/src/HOL/ROOT	Mon Oct 02 03:58:55 2017 +0200
     5.2 +++ b/src/HOL/ROOT	Mon Oct 02 16:47:46 2017 +0200
     5.3 @@ -121,8 +121,6 @@
     5.4      Exp demonstrates the use of iterated inductive definitions to reason about
     5.5      mutually recursive relations.
     5.6    *}
     5.7 -  theories [document = false]
     5.8 -    "HOL-Library.Old_Datatype"
     5.9    theories [quick_and_dirty]
    5.10      Common_Patterns
    5.11    theories
    5.12 @@ -142,12 +140,6 @@
    5.13  
    5.14  session "HOL-IMP" (timing) in IMP = "HOL-Library" +
    5.15    options [document_variants = document]
    5.16 -  theories [document = false]
    5.17 -    "HOL-Library.While_Combinator"
    5.18 -    "HOL-Library.Char_ord"
    5.19 -    "HOL-Library.List_lexord"
    5.20 -    "HOL-Library.Quotient_List"
    5.21 -    "HOL-Library.Extended"
    5.22    theories
    5.23      BExp
    5.24      ASM
    5.25 @@ -200,8 +192,6 @@
    5.26      "HOL-Number_Theory"
    5.27    theories [document = false]
    5.28      Less_False
    5.29 -    "HOL-Library.Multiset"
    5.30 -    "HOL-Number_Theory.Fib"
    5.31    theories
    5.32      Sorting
    5.33      Balance
    5.34 @@ -227,11 +217,6 @@
    5.35    *}
    5.36    sessions
    5.37      "HOL-Algebra"
    5.38 -  theories [document = false]
    5.39 -    "HOL-Library.FuncSet"
    5.40 -    "HOL-Library.Multiset"
    5.41 -    "HOL-Algebra.Ring"
    5.42 -    "HOL-Algebra.FiniteProduct"
    5.43    theories
    5.44      Number_Theory
    5.45    document_files
    5.46 @@ -310,11 +295,6 @@
    5.47  
    5.48      The Isabelle Algebraic Library.
    5.49    *}
    5.50 -  theories [document = false]
    5.51 -    (* Preliminaries from set and number theory *)
    5.52 -    "HOL-Library.FuncSet"
    5.53 -    "HOL-Computational_Algebra.Primes"
    5.54 -    "HOL-Library.Permutation"
    5.55    theories
    5.56      (* Orders and Lattices *)
    5.57      Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
    5.58 @@ -403,10 +383,6 @@
    5.59  
    5.60  session "HOL-Imperative_HOL" in Imperative_HOL = "HOL-Library" +
    5.61    options [print_mode = "iff,no_brackets"]
    5.62 -  theories [document = false]
    5.63 -    "HOL-Library.Countable"
    5.64 -    "HOL-Library.Monad_Syntax"
    5.65 -    "HOL-Library.LaTeXsugar"
    5.66    theories Imperative_HOL_ex
    5.67    document_files "root.bib" "root.tex"
    5.68  
    5.69 @@ -433,13 +409,7 @@
    5.70    *}
    5.71    options [parallel_proofs = 0, quick_and_dirty = false]
    5.72    sessions
    5.73 -    "HOL-Library"
    5.74      "HOL-Computational_Algebra"
    5.75 -  theories [document = false]
    5.76 -    "HOL-Library.Code_Target_Numeral"
    5.77 -    "HOL-Library.Monad_Syntax"
    5.78 -    "HOL-Computational_Algebra.Primes"
    5.79 -    "HOL-Library.Open_State_Syntax"
    5.80    theories
    5.81      Greatest_Common_Divisor
    5.82      Warshall
    5.83 @@ -490,8 +460,6 @@
    5.84    *}
    5.85    sessions
    5.86      "HOL-Eisbach"
    5.87 -  theories [document = false]
    5.88 -    "HOL-Library.While_Combinator"
    5.89    theories
    5.90      MicroJava
    5.91    document_files
    5.92 @@ -555,13 +523,11 @@
    5.93    theories CompleteLattice
    5.94    document_files "root.tex"
    5.95  
    5.96 -session "HOL-ex" (timing) in ex = "HOL-Library" +
    5.97 +session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
    5.98    description {*
    5.99      Miscellaneous examples for Higher-Order Logic.
   5.100    *}
   5.101    options [document = false]
   5.102 -  sessions
   5.103 -    "HOL-Number_Theory"
   5.104    theories
   5.105      Adhoc_Overloading_Examples
   5.106      Antiquote
   5.107 @@ -653,9 +619,6 @@
   5.108      Miscellaneous Isabelle/Isar examples.
   5.109    *}
   5.110    options [quick_and_dirty]
   5.111 -  theories [document = false]
   5.112 -    "HOL-Library.Lattice_Syntax"
   5.113 -    "HOL-Computational_Algebra.Primes"
   5.114    theories
   5.115      Knaster_Tarski
   5.116      Peirce
   5.117 @@ -694,8 +657,6 @@
   5.118    description {*
   5.119      Verification of the SET Protocol.
   5.120    *}
   5.121 -  theories [document = false]
   5.122 -    "HOL-Library.Nat_Bijection"
   5.123    theories
   5.124      SET_Protocol
   5.125    document_files "root.tex"
   5.126 @@ -745,12 +706,6 @@
   5.127      ATP_Problem_Import
   5.128  
   5.129  session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   5.130 -  theories [document = false]
   5.131 -    "HOL-Library.Countable"
   5.132 -    "HOL-Library.Permutation"
   5.133 -    "HOL-Library.Order_Continuity"
   5.134 -    "HOL-Library.Diagonal_Subsequence"
   5.135 -    "HOL-Library.Finite_Map"
   5.136    theories
   5.137      Probability (global)
   5.138    document_files "root.tex"
   5.139 @@ -761,10 +716,8 @@
   5.140      Koepf_Duermuth_Countermeasure
   5.141      Measure_Not_CCC
   5.142  
   5.143 -session "HOL-Nominal" in Nominal = HOL +
   5.144 +session "HOL-Nominal" in Nominal = "HOL-Library" +
   5.145    options [document = false]
   5.146 -  sessions
   5.147 -    "HOL-Library"
   5.148    theories
   5.149      Nominal
   5.150  
   5.151 @@ -1064,18 +1017,13 @@
   5.152      "Examples/Finite"
   5.153      "Examples/T2_Spaces"
   5.154  
   5.155 -session HOLCF (main timing) in HOLCF = HOL +
   5.156 +session HOLCF (main timing) in HOLCF = "HOL-Library" +
   5.157    description {*
   5.158      Author:     Franz Regensburger
   5.159      Author:     Brian Huffman
   5.160  
   5.161      HOLCF -- a semantic extension of HOL by the LCF logic.
   5.162    *}
   5.163 -  sessions
   5.164 -    "HOL-Library"
   5.165 -  theories [document = false]
   5.166 -    "HOL-Library.Nat_Bijection"
   5.167 -    "HOL-Library.Countable"
   5.168    theories
   5.169      HOLCF (global)
   5.170    document_files "root.tex"
     6.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 03:58:55 2017 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 16:47:46 2017 +0200
     6.3 @@ -114,6 +114,7 @@
     6.4      loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     6.5      known: Known = Known.empty,
     6.6      overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     6.7 +    imported_sources: List[(Path, SHA1.Digest)] = Nil,
     6.8      sources: List[(Path, SHA1.Digest)] = Nil,
     6.9      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    6.10      errors: List[String] = Nil,
    6.11 @@ -147,7 +148,12 @@
    6.12    {
    6.13      def is_empty: Boolean = session_bases.isEmpty
    6.14      def apply(name: String): Base = session_bases(name)
    6.15 -    def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)
    6.16 +
    6.17 +    def imported_sources(name: String): List[SHA1.Digest] =
    6.18 +      session_bases(name).imported_sources.map(_._2)
    6.19 +
    6.20 +    def sources(name: String): List[SHA1.Digest] =
    6.21 +      session_bases(name).sources.map(_._2)
    6.22  
    6.23      def errors: List[String] =
    6.24        (for {
    6.25 @@ -172,6 +178,25 @@
    6.26        check_keywords: Set[String] = Set.empty,
    6.27        global_theories: Map[String, String] = Map.empty): Deps =
    6.28    {
    6.29 +    var cache_sources = Map.empty[JFile, SHA1.Digest]
    6.30 +    def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
    6.31 +    {
    6.32 +      for {
    6.33 +        path <- paths
    6.34 +        file = path.file
    6.35 +        if cache_sources.isDefinedAt(file) || file.isFile
    6.36 +      }
    6.37 +      yield {
    6.38 +        cache_sources.get(file) match {
    6.39 +          case Some(digest) => (path, digest)
    6.40 +          case None =>
    6.41 +            val digest = SHA1.digest(file)
    6.42 +            cache_sources = cache_sources + (file -> digest)
    6.43 +            (path, digest)
    6.44 +        }
    6.45 +      }
    6.46 +    }
    6.47 +
    6.48      val session_bases =
    6.49        (Map.empty[String, Base] /: sessions.imports_topological_order)({
    6.50          case (session_bases, info) =>
    6.51 @@ -197,14 +222,9 @@
    6.52              }
    6.53  
    6.54              val thy_deps =
    6.55 -            {
    6.56 -              val root_theories =
    6.57 -                info.theories.flatMap({ case (_, thys) =>
    6.58 -                  thys.map({ case (thy, pos) =>
    6.59 -                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
    6.60 -                })
    6.61 -              resources.thy_info.dependencies(root_theories)
    6.62 -            }
    6.63 +              resources.thy_info.dependencies(
    6.64 +                for { (_, thys) <- info.theories; (thy, pos) <- thys }
    6.65 +                yield (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos))
    6.66  
    6.67              val overall_syntax = thy_deps.overall_syntax
    6.68  
    6.69 @@ -219,13 +239,15 @@
    6.70                }
    6.71                else Nil
    6.72  
    6.73 -            val all_files =
    6.74 +            val session_files =
    6.75                (theory_files ::: loaded_files.flatMap(_._2) :::
    6.76                  info.files.map(file => info.dir + file) :::
    6.77                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    6.78  
    6.79 +            val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    6.80 +
    6.81              if (list_files)
    6.82 -              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    6.83 +              progress.echo(cat_lines(session_files.map(_.implode).sorted.map("  " + _)))
    6.84  
    6.85              if (check_keywords.nonEmpty) {
    6.86                Check_Keywords.check_keywords(
    6.87 @@ -270,10 +292,8 @@
    6.88                  theories = thy_deps.names,
    6.89                  loaded_files = loaded_files)
    6.90  
    6.91 -            val sources =
    6.92 -              for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
    6.93              val sources_errors =
    6.94 -              for (p <- all_files if !p.is_file) yield "No such file: " + p
    6.95 +              for (p <- session_files if !p.is_file) yield "No such file: " + p
    6.96  
    6.97              val base =
    6.98                Base(
    6.99 @@ -282,7 +302,8 @@
   6.100                  loaded_theories = thy_deps.loaded_theories,
   6.101                  known = known,
   6.102                  overall_syntax = overall_syntax,
   6.103 -                sources = sources,
   6.104 +                imported_sources = check_sources(imported_files),
   6.105 +                sources = check_sources(session_files),
   6.106                  session_graph = session_graph,
   6.107                  errors = thy_deps.errors ::: sources_errors,
   6.108                  imports = Some(imports_base))
   6.109 @@ -887,7 +908,7 @@
   6.110            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
   6.111            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
   6.112            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
   6.113 -          stmt.string(7) = cat_lines(build.sources)
   6.114 +          stmt.string(7) = build.sources
   6.115            stmt.string(8) = cat_lines(build.input_heaps)
   6.116            stmt.string(9) = build.output_heap getOrElse ""
   6.117            stmt.int(10) = build.return_code
   6.118 @@ -912,6 +933,7 @@
   6.119        Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
   6.120  
   6.121      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
   6.122 +    {
   6.123        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
   6.124          Session_Info.session_name.where_equal(name)))(stmt =>
   6.125        {
   6.126 @@ -920,11 +942,12 @@
   6.127          else {
   6.128            Some(
   6.129              Build.Session_Info(
   6.130 -              split_lines(res.string(Session_Info.sources)),
   6.131 +              res.string(Session_Info.sources),
   6.132                split_lines(res.string(Session_Info.input_heaps)),
   6.133                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
   6.134                res.int(Session_Info.return_code)))
   6.135          }
   6.136        })
   6.137 +    }
   6.138    }
   6.139  }
     7.1 --- a/src/Pure/Thy/thy_info.scala	Mon Oct 02 03:58:55 2017 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Oct 02 16:47:46 2017 +0200
     7.3 @@ -66,6 +66,17 @@
     7.4            names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     7.5      }
     7.6  
     7.7 +    def imported_files: List[Path] =
     7.8 +    {
     7.9 +      val base = resources.session_base
    7.10 +      val base_theories =
    7.11 +        loaded_theories.all_preds(names.map(_.theory)).
    7.12 +          filter(base.loaded_theories.defined(_))
    7.13 +
    7.14 +      base_theories.map(theory => base.known.theories(theory).path) :::
    7.15 +      base_theories.flatMap(base.known.loaded_files(_))
    7.16 +    }
    7.17 +
    7.18      lazy val overall_syntax: Outer_Syntax =
    7.19        Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    7.20  
     8.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 03:58:55 2017 +0200
     8.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 16:47:46 2017 +0200
     8.3 @@ -24,10 +24,13 @@
     8.4    /* persistent build info */
     8.5  
     8.6    sealed case class Session_Info(
     8.7 -    sources: List[String],
     8.8 +    sources: String,
     8.9      input_heaps: List[String],
    8.10      output_heap: Option[String],
    8.11      return_code: Int)
    8.12 +  {
    8.13 +    def ok: Boolean = return_code == 0
    8.14 +  }
    8.15  
    8.16  
    8.17    /* queue with scheduling information */
    8.18 @@ -352,6 +355,7 @@
    8.19      list_files: Boolean = false,
    8.20      check_keywords: Set[String] = Set.empty,
    8.21      no_build: Boolean = false,
    8.22 +    soft_build: Boolean = false,
    8.23      system_mode: Boolean = false,
    8.24      verbose: Boolean = false,
    8.25      pide: Boolean = false,
    8.26 @@ -364,24 +368,58 @@
    8.27      sessions: List[String] = Nil,
    8.28      selection: Sessions.Selection = Sessions.Selection.empty): Results =
    8.29    {
    8.30 -    /* session selection and dependencies */
    8.31 +    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    8.32  
    8.33 -    val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    8.34 +    val store = Sessions.store(system_mode)
    8.35 +
    8.36 +
    8.37 +    /* session selection and dependencies */
    8.38  
    8.39      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    8.40  
    8.41 -    val (selected, selected_sessions) =
    8.42 -      full_sessions.selection(
    8.43 -          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    8.44 -            exclude_sessions, session_groups, sessions) ++ selection)
    8.45 +    def sources_stamp(deps: Sessions.Deps, name: String): String =
    8.46 +    {
    8.47 +      val digests =
    8.48 +        full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
    8.49 +      SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
    8.50 +    }
    8.51 +
    8.52 +    val (selected, selected_sessions, deps) =
    8.53 +    {
    8.54 +      val (selected0, selected_sessions0) =
    8.55 +        full_sessions.selection(
    8.56 +            Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    8.57 +              exclude_sessions, session_groups, sessions) ++ selection)
    8.58 +
    8.59 +      val deps0 =
    8.60 +        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
    8.61 +          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    8.62 +          global_theories = full_sessions.global_theories).check_errors
    8.63  
    8.64 -    val deps =
    8.65 -      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    8.66 -        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    8.67 -        global_theories = full_sessions.global_theories).check_errors
    8.68 +      if (soft_build) {
    8.69 +        val outdated =
    8.70 +          selected0.flatMap(name =>
    8.71 +            store.find_database(name) match {
    8.72 +              case Some(database) =>
    8.73 +                using(SQLite.open_database(database))(store.read_build(_, name)) match {
    8.74 +                  case Some(build)
    8.75 +                  if build.ok && build.sources == sources_stamp(deps0, name) => None
    8.76 +                  case _ => Some(name)
    8.77 +                }
    8.78 +              case None => Some(name)
    8.79 +            })
    8.80 +        val (selected, selected_sessions) =
    8.81 +          full_sessions.selection(Sessions.Selection(sessions = outdated))
    8.82 +        val deps =
    8.83 +          Sessions.deps(selected_sessions, inlined_files = true,
    8.84 +            global_theories = full_sessions.global_theories).check_errors
    8.85 +        (selected, selected_sessions, deps)
    8.86 +      }
    8.87 +      else (selected0, selected_sessions0, deps0)
    8.88 +    }
    8.89  
    8.90 -    def sources_stamp(name: String): List[String] =
    8.91 -      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    8.92 +
    8.93 +    /* check unknown files */
    8.94  
    8.95      if (check_unknown_files) {
    8.96        val source_files =
    8.97 @@ -399,7 +437,6 @@
    8.98  
    8.99      /* main build process */
   8.100  
   8.101 -    val store = Sessions.store(system_mode)
   8.102      val queue = Queue(progress, selected_sessions, store)
   8.103  
   8.104      store.prepare_output()
   8.105 @@ -501,7 +538,8 @@
   8.106                        parse_session_info(
   8.107                          command_timings = true, ml_statistics = true, task_statistics = true),
   8.108                    build =
   8.109 -                    Session_Info(sources_stamp(name), input_heaps, heap_stamp, process_result.rc)))
   8.110 +                    Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
   8.111 +                      process_result.rc)))
   8.112              }
   8.113  
   8.114              // messages
   8.115 @@ -533,8 +571,8 @@
   8.116                        using(SQLite.open_database(database))(store.read_build(_, name)) match {
   8.117                          case Some(build) =>
   8.118                            val current =
   8.119 -                            build.return_code == 0 &&
   8.120 -                            build.sources == sources_stamp(name) &&
   8.121 +                            build.ok &&
   8.122 +                            build.sources == sources_stamp(deps, name) &&
   8.123                              build.input_heaps == ancestor_heaps &&
   8.124                              build.output_heap == heap_stamp &&
   8.125                              !(do_output && heap_stamp.isEmpty)
   8.126 @@ -633,6 +671,7 @@
   8.127      var numa_shuffling = false
   8.128      var pide = false
   8.129      var requirements = false
   8.130 +    var soft_build = false
   8.131      var exclude_session_groups: List[String] = Nil
   8.132      var all_sessions = false
   8.133      var build_heap = false
   8.134 @@ -657,6 +696,7 @@
   8.135      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
   8.136      -P           build via PIDE protocol
   8.137      -R           operate on requirements of selected sessions
   8.138 +    -S           soft build: only observe changes of sources, not heap images
   8.139      -X NAME      exclude sessions from group NAME and all descendants
   8.140      -a           select all sessions
   8.141      -b           build heap images
   8.142 @@ -680,6 +720,7 @@
   8.143        "N" -> (_ => numa_shuffling = true),
   8.144        "P" -> (_ => pide = true),
   8.145        "R" -> (_ => requirements = true),
   8.146 +      "S" -> (_ => soft_build = true),
   8.147        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   8.148        "a" -> (_ => all_sessions = true),
   8.149        "b" -> (_ => build_heap = true),
   8.150 @@ -721,6 +762,7 @@
   8.151            list_files = list_files,
   8.152            check_keywords = check_keywords,
   8.153            no_build = no_build,
   8.154 +          soft_build = soft_build,
   8.155            system_mode = system_mode,
   8.156            verbose = verbose,
   8.157            pide = pide,
     9.1 --- a/src/ZF/ROOT	Mon Oct 02 03:58:55 2017 +0200
     9.2 +++ b/src/ZF/ROOT	Mon Oct 02 16:47:46 2017 +0200
     9.3 @@ -143,9 +143,10 @@
     9.4      Glynn Winskel. The Formal Semantics of Programming Languages.
     9.5      MIT Press, 1993.
     9.6    *}
     9.7 -  options [document = false]
     9.8    theories Equiv
     9.9 -  document_files "root.tex" "root.bib"
    9.10 +  document_files
    9.11 +    "root.tex"
    9.12 +    "root.bib"
    9.13  
    9.14  session "ZF-Induct" (ZF) in Induct = ZF +
    9.15    description {*