more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
authorwenzelm
Mon Oct 02 15:37:46 2017 +0200 (21 months ago)
changeset 667490445cfaf6132
parent 66748 3efac90a11a7
child 66750 41fbe4a3aac9
more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 13:45:36 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 15:37:46 2017 +0200
     1.3 @@ -908,7 +908,7 @@
     1.4            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
     1.5            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
     1.6            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
     1.7 -          stmt.string(7) = cat_lines(build.sources)
     1.8 +          stmt.string(7) = build.sources
     1.9            stmt.string(8) = cat_lines(build.input_heaps)
    1.10            stmt.string(9) = build.output_heap getOrElse ""
    1.11            stmt.int(10) = build.return_code
    1.12 @@ -942,7 +942,7 @@
    1.13          else {
    1.14            Some(
    1.15              Build.Session_Info(
    1.16 -              split_lines(res.string(Session_Info.sources)),
    1.17 +              res.string(Session_Info.sources),
    1.18                split_lines(res.string(Session_Info.input_heaps)),
    1.19                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.20                res.int(Session_Info.return_code)))
     2.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 13:45:36 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 15:37:46 2017 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    /* persistent build info */
     2.5  
     2.6    sealed case class Session_Info(
     2.7 -    sources: List[String],
     2.8 +    sources: String,
     2.9      input_heaps: List[String],
    2.10      output_heap: Option[String],
    2.11      return_code: Int)
    2.12 @@ -377,9 +377,12 @@
    2.13  
    2.14      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    2.15  
    2.16 -    def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    2.17 -      (full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name))
    2.18 -        .map(_.toString).sorted
    2.19 +    def sources_stamp(deps: Sessions.Deps, name: String): String =
    2.20 +    {
    2.21 +      val digests =
    2.22 +        full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name)
    2.23 +      SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
    2.24 +    }
    2.25  
    2.26      val (selected, selected_sessions, deps) =
    2.27      {