# HG changeset patch
# User wenzelm
# Date 1493812462 -7200
# Node ID 99676834e53c83b436bd5ae039bab224150697cf
# Parent  d1e9155b894caf88c35a4a599e336ac17b3eeea5
clarified pull_date tables;
support for SQLite snapshot;

diff -r d1e9155b894c -r 99676834e53c src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue May 02 23:31:00 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 13:54:22 2017 +0200
@@ -918,16 +918,25 @@
 
     val pull_date = SQL.Column.date("pull_date")
 
-    def pull_date_table(column: SQL.Column): SQL.Table =
-      SQL.Table("isabelle_build_log_" + column.name, List(column, pull_date),
-        view = // for PostgreSQL
-          "SELECT " + column.sql + ", min(" + Prop.build_start.sql + ") AS " + pull_date.sql +
+    def pull_date_table(name: String, version: SQL.Column): SQL.Table =
+      SQL.Table("isabelle_build_log_" + name, List(version.copy(primary_key = true), pull_date),
+        view = // PostgreSQL
+          "SELECT " + version.sql + ", min(" + Prop.build_start.sql + ") AS " + pull_date.sql +
           " FROM " + Meta_Info.table.sql +
-          " WHERE " + column.sql + " IS NOT NULL AND " + Prop.build_start.sql + "IS NOT NULL" +
-          " GROUP BY " + column.sql)
+          " WHERE " + version.sql + " IS NOT NULL AND" + Prop.build_start.sql + " IS NOT NULL" +
+          " GROUP BY " + version.sql)
+
+    val isabelle_pull_date_table = pull_date_table("isabelle_pull_date", Prop.isabelle_version)
+    val afp_pull_date_table = pull_date_table("afp_pull_date", Prop.afp_version)
 
-    val isabelle_version_table = pull_date_table(Prop.isabelle_version)
-    val afp_version_table = pull_date_table(Prop.afp_version)
+    def recent(table: SQL.Table, days: Int): String =
+      table.sql_select(table.columns) +
+      " WHERE " + pull_date(table).sql + " > now() - INTERVAL '" + days.max(0) + " days'"
+
+    def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int): String =
+      table.sql_select(columns) +
+      " INNER JOIN (" + recent(isabelle_pull_date_table, days) + ") AS recent" +
+      " ON " + Prop.isabelle_version(table).sql + " = recent." + Prop.isabelle_version.sql
 
 
     /* main operations */
@@ -937,9 +946,40 @@
       store.write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
 
       if (db.isInstanceOf[PostgreSQL.Database]) {
-        List(full_table, isabelle_version_table, afp_version_table)
+        List(full_table, isabelle_pull_date_table, afp_pull_date_table)
           .foreach(db.create_view(_))
       }
     }
+
+    def snapshot(store: Store, db: PostgreSQL.Database, sqlite_database: Path, days: Int = 100)
+    {
+      Isabelle_System.mkdirs(sqlite_database.dir)
+      sqlite_database.file.delete
+
+      using(SQLite.open_database(sqlite_database))(db2 =>
+      {
+        db.transaction {
+          db2.transaction {
+            // pull_date tables
+            List(isabelle_pull_date_table, afp_pull_date_table).foreach(table =>
+            {
+              db2.create_table(table)
+              using(db2.insert(table))(stmt2 =>
+              {
+                using(db.statement(recent(table, days)))(stmt =>
+                {
+                  val rs = stmt.executeQuery
+                  while (rs.next()) {
+                    for ((c, i) <- table.columns.zipWithIndex)
+                      db2.set_string(stmt2, i + 1, db.get(rs, c, db.string _))
+                    stmt2.execute
+                  }
+                })
+              })
+            })
+          }
+        }
+      })
+    }
   }
 }