sync session images, based on accidental local state;

--- a/src/Pure/Admin/build_history.scala	Fri Jun 10 15:34:25 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri Jun 10 21:05:31 2022 +0200
@@ -536,7 +536,7 @@
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
       val context = Rsync.Context(progress, port = ssh.nominal_port, protect_args = protect_args)
-      Sync.sync(context, ssh.rsync_path(target),
+      Sync.sync(ssh.options, context, ssh.rsync_path(target),
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
     }

--- a/src/Pure/Admin/sync.scala	Fri Jun 10 15:34:25 2022 +0200
+++ b/src/Pure/Admin/sync.scala	Fri Jun 10 21:05:31 2022 +0200
@@ -8,9 +8,35 @@
 
 
 object Sync {
-  def sync(context: Rsync.Context, target: String,
+  /* session images */
+
+  def find_images(options: Options, session_images: List[String],
+    dirs: List[Path] = Nil
+  ): List[String] = {
+    if (session_images.isEmpty) Nil
+    else {
+      val store = Sessions.store(options)
+      val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+      sessions_structure.build_requirements(session_images).flatMap { session =>
+        val heap =
+          store.find_heap(session).map(_.expand).map(path =>
+            File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
+        val db =
+          store.find_database(session).map(_.expand).map(path =>
+            File.standard_path(path.dir.dir.dir) + "/./" + path.dir.dir.file_name + "/" +
+              path.dir.file_name + "/" + path.file_name)
+        heap.toList ::: db.toList
+      }
+    }
+  }
+
+
+  /* sync */
+
+  def sync(options: Options, context: Rsync.Context, target: String,
     verbose: Boolean = false,
     thorough: Boolean = false,
+    session_images: List[String] = Nil,
     preserve_jars: Boolean = false,
     dry_run: Boolean = false,
     rev: String = "",
@@ -32,18 +58,28 @@
     context.progress.echo_if(verbose, "\n* Isabelle repository:")
     sync(hg, target, rev,
       contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
-      filter = List("protect /AFP"))
+      filter = List("protect /heaps", "protect /heaps/**", "protect /AFP"))
 
     for (hg <- afp_hg) {
       context.progress.echo_if(verbose, "\n* AFP repository:")
       sync(hg, Rsync.append(target, "AFP"), afp_rev)
     }
+
+    val images =
+      find_images(options, session_images,
+        dirs = afp_root.map(_ + Path.explode("thys")).toList)
+    if (images.nonEmpty) {
+      context.progress.echo_if(verbose, "\n* Session images:")
+      Rsync.exec(context, verbose = verbose, thorough = thorough, dry_run = dry_run,
+        args = List("--relative", "--") ::: images ::: List(Rsync.append(target, "heaps/"))).check
+    }
   }
 
   val isabelle_tool =
     Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories",
       Scala_Project.here, { args =>
         var afp_root: Option[Path] = None
+        var session_images = List.empty[String]
         var preserve_jars = false
         var protect_args = false
         var thorough = false
@@ -58,6 +94,8 @@
 
   Options are:
     -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
+    -I NAME      include session heap image and build database
+                 (based on accidental local state)
     -J           preserve *.jar files
     -S           robust (but less portable) treatment of spaces in directory names
     -T           thorough treatment of file content and directory times
@@ -76,8 +114,13 @@
   Example: accurate testing
 
     isabelle sync -A: -T testmachine:test/isabelle_afp
+
+  Example: incremental testing based on session images
+
+    isabelle sync -A: -I HOL-Analysis testmachine:test/isabelle_afp
 """,
           "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
+          "I:" -> (arg => session_images = session_images ::: List(arg)),
           "J" -> (_ => preserve_jars = true),
           "S" -> (_ => protect_args = true),
           "T" -> (_ => thorough = true),
@@ -94,10 +137,12 @@
             case _ => getopts.usage()
           }
 
+        val options = Options.init()
         val progress = new Console_Progress
         val context = Rsync.Context(progress, port = port, protect_args = protect_args)
-        sync(context, target, verbose = verbose, thorough = thorough,
-          preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
+        sync(options, context, target, verbose = verbose, thorough = thorough,
+          session_images = session_images, preserve_jars = preserve_jars,
+          dry_run = dry_run, rev = rev, afp_root = afp_root,
           afp_rev = afp_rev)
       }
     )

--- a/src/Pure/Thy/sessions.scala	Fri Jun 10 15:34:25 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Jun 10 21:05:31 2022 +0200
@@ -1302,6 +1302,9 @@
 
     /* database */
 
+    def find_database(name: String): Option[Path] =
+      input_dirs.map(_ + database(name)).find(_.is_file)
+
     def database_server: Boolean = options.bool("build_database_server")
 
     def open_database_server(): SQL.Database =