src/Pure/Admin/build_log.scala

 
     val ml_statistics_table =
       build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
 
 
+    /* AFP versions */
+
+    val isabelle_afp_versions_table: SQL.Table =
+    {
+      val version1 = Prop.isabelle_version
+      val version2 = Prop.afp_version
+      build_log_table("isabelle_afp_versions", List(version1.copy(primary_key = true), version2),
+        SQL.select(List(version1, version2), distinct = true) + meta_info_table +
+        " WHERE " + version1 + " IS NOT NULL AND " + version2 + " IS NOT NULL")
+    }
+
+
     /* earliest pull date for repository version (PostgreSQL queries) */
 
     val pull_date = SQL.Column.date("pull_date")
 
     val pull_date_table: SQL.Table =

         "SELECT " + version + ", min(" + Prop.build_start + ") AS " + pull_date +
         " FROM " + meta_info_table +
         " WHERE " + version + " IS NOT NULL AND " + Prop.build_start + " IS NOT NULL" +
         " GROUP BY " + version)
     }
+
+    val afp_pull_date_table: SQL.Table =
+    {
+      val version1 = Prop.isabelle_version
+      val version2 = Prop.afp_version
+      val table1 = pull_date_table
+      val table2 = isabelle_afp_versions_table
+      build_log_table("afp_pull_date", List(version1.copy(primary_key = true), version2, pull_date),
+        table1.select(List(version1(table1), version2(table2), pull_date(table1))) +
+        SQL.join_inner + table2.query_named + " ON " + version1(table1) + " = " + version1(table2))
+    }
+
+
+    /* recent entries */
 
     def recent_time(days: Int): SQL.Source =
       "now() - INTERVAL '" + days.max(0) + " days'"
 
     def recent_pull_date_table(days: Int, rev: String = ""): SQL.Table =

     def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
     {
       write_info(db, Log_File.find_files(dirs), ml_statistics = ml_statistics)
 
       db.create_view(Data.pull_date_table)
+      db.create_view(Data.afp_pull_date_table)
       db.create_view(Data.universal_table)
     }
 
     def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
       days: Int = 100, ml_statistics: Boolean = false)