sources_stamp refers to full sources;
authorwenzelm
Mon Oct 02 13:33:36 2017 +0200 (18 months ago)
changeset 66746888a51e77c6e
parent 66745 e7ac579b883c
child 66747 f4c6c8a8f645
sources_stamp refers to full sources;
simplified data storage (again);
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 11:43:17 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 13:33:36 2017 +0200
     1.3 @@ -815,12 +815,11 @@
     1.4        List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
     1.5  
     1.6      // Build.Session_Info
     1.7 -    val imported_sources = SQL.Column.string("imported_sources")
     1.8      val sources = SQL.Column.string("sources")
     1.9      val input_heaps = SQL.Column.string("input_heaps")
    1.10      val output_heap = SQL.Column.string("output_heap")
    1.11      val return_code = SQL.Column.int("return_code")
    1.12 -    val build_columns = List(imported_sources, sources, input_heaps, output_heap, return_code)
    1.13 +    val build_columns = List(sources, input_heaps, output_heap, return_code)
    1.14  
    1.15      val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
    1.16    }
    1.17 @@ -909,11 +908,10 @@
    1.18            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    1.19            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    1.20            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    1.21 -          stmt.string(7) = cat_lines(build.imported_sources)
    1.22 -          stmt.string(8) = cat_lines(build.sources)
    1.23 -          stmt.string(9) = cat_lines(build.input_heaps)
    1.24 -          stmt.string(10) = build.output_heap getOrElse ""
    1.25 -          stmt.int(11) = build.return_code
    1.26 +          stmt.string(7) = cat_lines(build.sources)
    1.27 +          stmt.string(8) = cat_lines(build.input_heaps)
    1.28 +          stmt.string(9) = build.output_heap getOrElse ""
    1.29 +          stmt.int(10) = build.return_code
    1.30            stmt.execute()
    1.31          })
    1.32        }
    1.33 @@ -936,34 +934,20 @@
    1.34  
    1.35      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.36      {
    1.37 -      val result0 =
    1.38 -        db.using_statement(Session_Info.table.select(Session_Info.build_columns.tail,
    1.39 -          Session_Info.session_name.where_equal(name)))(stmt =>
    1.40 -        {
    1.41 -          val res = stmt.execute_query()
    1.42 -          if (!res.next()) None
    1.43 -          else {
    1.44 -            Some(
    1.45 -              Build.Session_Info(Nil,
    1.46 -                split_lines(res.string(Session_Info.sources)),
    1.47 -                split_lines(res.string(Session_Info.input_heaps)),
    1.48 -                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.49 -                res.int(Session_Info.return_code)))
    1.50 -          }
    1.51 -        })
    1.52 -      result0.map(info =>
    1.53 -        info.copy(imported_sources =
    1.54 -          try {
    1.55 -            db.using_statement(Session_Info.table.select(List(Session_Info.imported_sources),
    1.56 -              Session_Info.session_name.where_equal(name)))(stmt =>
    1.57 -            {
    1.58 -              val res = stmt.execute_query()
    1.59 -              if (!res.next) Nil else split_lines(res.string(Session_Info.imported_sources))
    1.60 -            })
    1.61 -          } // column "imported_sources" could be missing
    1.62 -          catch { case _: java.sql.SQLException => Nil }
    1.63 -        )
    1.64 -      )
    1.65 +      db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.66 +        Session_Info.session_name.where_equal(name)))(stmt =>
    1.67 +      {
    1.68 +        val res = stmt.execute_query()
    1.69 +        if (!res.next()) None
    1.70 +        else {
    1.71 +          Some(
    1.72 +            Build.Session_Info(
    1.73 +              split_lines(res.string(Session_Info.sources)),
    1.74 +              split_lines(res.string(Session_Info.input_heaps)),
    1.75 +              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.76 +              res.int(Session_Info.return_code)))
    1.77 +        }
    1.78 +      })
    1.79      }
    1.80    }
    1.81  }
     2.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 11:43:17 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 13:33:36 2017 +0200
     2.3 @@ -24,7 +24,6 @@
     2.4    /* persistent build info */
     2.5  
     2.6    sealed case class Session_Info(
     2.7 -    imported_sources: List[String],
     2.8      sources: List[String],
     2.9      input_heaps: List[String],
    2.10      output_heap: Option[String],
    2.11 @@ -375,11 +374,9 @@
    2.12  
    2.13      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    2.14  
    2.15 -    def imported_sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    2.16 -      deps.imported_sources(name).map(_.toString).sorted
    2.17 -
    2.18      def sources_stamp(deps: Sessions.Deps, name: String): List[String] =
    2.19 -      (full_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
    2.20 +      (full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name))
    2.21 +        .map(_.toString).sorted
    2.22  
    2.23      val (selected, selected_sessions, deps) =
    2.24      {
    2.25 @@ -401,7 +398,6 @@
    2.26                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    2.27                    case Some(build)
    2.28                    if build.return_code == 0 &&
    2.29 -                    build.imported_sources == imported_sources_stamp(deps0, name) &&
    2.30                      build.sources == sources_stamp(deps0, name) => None
    2.31                    case _ => Some(name)
    2.32                  }
    2.33 @@ -537,11 +533,7 @@
    2.34                        parse_session_info(
    2.35                          command_timings = true, ml_statistics = true, task_statistics = true),
    2.36                    build =
    2.37 -                    Session_Info(
    2.38 -                      imported_sources_stamp(deps, name),
    2.39 -                      sources_stamp(deps, name),
    2.40 -                      input_heaps,
    2.41 -                      heap_stamp,
    2.42 +                    Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    2.43                        process_result.rc)))
    2.44              }
    2.45