src/Pure/Tools/sync.scala

tuned comments;

/*  Title:      Pure/Tools/sync.scala
    Author:     Makarius

Synchronize Isabelle + AFP repositories.
*/

package isabelle


object Sync {
  /* 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 = Store(options)
      val sessions_structure = Sessions.load_structure(options, dirs = dirs)
      sessions_structure.build_requirements(session_images).flatMap { name =>
        val session = store.get_session(name)
        val heap =
          session.heap.map(_.expand).map(path =>
            File.standard_path(path.dir.dir) + "/./" + path.dir.file_name + "/" + path.file_name)
        val log_db =
          session.log_db.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 ::: log_db.toList
      }
    }
  }


  /* sync */

  val DIRS: Path = Path.basic("dirs")
  val DIRS_ROOTS: Path = DIRS + Sessions.ROOTS

  sealed case class Dir(name: String, root: Path, path: Path = Path.current, rev: String = "") {
    lazy val hg: Mercurial.Repository = Mercurial.repository(root)
    def check(): Unit = hg

    def source: Path = root + path
    def target: Path = DIRS + Path.basic(name)
    def roots_entry: String = ((if (name.isEmpty) Path.parent else Path.basic(name)) + path).implode
  }

  def afp_dir(base_dir: Path = AFP.BASE, rev: String = ""): Dir =
    Dir("AFP", base_dir, path = AFP.main_dir(base_dir = Path.current), rev = rev)

  def afp_dirs(root: Option[Path] = None, rev: String = ""): List[Dir] =
    root.toList.map(base_dir => afp_dir(base_dir = base_dir, rev = rev))

  def sync(options: Options, context: Rsync.Context, target: Path,
    thorough: Boolean = false,
    purge_heaps: Boolean = false,
    session_images: List[String] = Nil,
    preserve_jars: Boolean = false,
    dry_run: Boolean = false,
    rev: String = "",
    dirs: List[Dir] = Nil
  ): Unit = {
    val progress = context.progress

    val self = Mercurial.self_repository()
    dirs.foreach(_.check())

    val sync_dirs: List[Dir] = {
      val m =
        Multi_Map.from(
          for (dir <- dirs.iterator if dir.name.nonEmpty) yield dir.name -> dir.root.canonical)
      for ((name, roots) <- m.iterator_list if roots.length > 1) {
        error("Incoherent sync directory " + quote(name) + ":\n" +
          cat_lines(roots.reverse.map(p => "  " + p.toString)))
      }
      Library.distinct(dirs, (d1: Dir, d2: Dir) => d1.name == d2.name)
    }

    val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil

    def synchronize(src: Mercurial.Repository, dest: Path, r: String,
      contents: List[File.Content] = Nil, filter: List[String] = Nil
    ): Unit = {
      src.sync(context, dest, rev = r, thorough = thorough, dry_run = dry_run,
        contents = contents, filter = filter ::: more_filter)
    }

    progress.echo("\n* Isabelle:", verbose = true)
    val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
    val filter_dirs = sync_dirs.map(dir => "protect /" + dir.target.implode)
    synchronize(self, target, rev,
      contents = List(File.content(Path.explode("etc/ISABELLE_ID"), self.id(rev = rev))),
      filter = filter_heaps ::: filter_dirs)

    context.ssh.make_directory(target + DIRS)
    context.ssh.write(target + DIRS_ROOTS, Library.terminate_lines(dirs.map(_.roots_entry)))

    for (dir <- sync_dirs) {
      progress.echo("\n* " + dir.name + ":", verbose = true)
      synchronize(dir.hg, target + dir.target, dir.rev)
    }

    val images = find_images(options, session_images, dirs = dirs.map(_.source))
    if (images.nonEmpty) {
      progress.echo("\n* Session images:", verbose = true)
      val heaps = context.target(target + Path.explode("heaps")) + "/"
      Rsync.exec(context, thorough = thorough, dry_run = dry_run,
        args = List("--relative", "--") ::: images ::: List(heaps)).check
    }
  }

  val isabelle_tool =
    Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories",
      Scala_Project.here, { args =>
        var afp_root: Option[Path] = None
        var purge_heaps = false
        var session_images = List.empty[String]
        var preserve_jars = false
        var thorough = false
        var afp_rev = ""
        var dry_run = false
        var ssh_port = 0
        var rev = ""
        var ssh_host = ""
        var ssh_user = ""
        var verbose = false

        val getopts = Getopts("""
Usage: isabelle sync [OPTIONS] TARGET

  Options are:
    -A ROOT      include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
    -H           purge heaps directory on target
    -I NAME      include session heap image and build database
                 (based on accidental local state)
    -J           preserve *.jar files
    -T           thorough treatment of file content and directory times
    -a REV       explicit AFP revision (default: state of working directory)
    -s HOST      SSH host name for remote target (default: local)
    -u USER      explicit SSH user name
    -n           no changes: dry-run
    -p PORT      explicit SSH port
    -r REV       explicit revision (default: state of working directory)
    -v           verbose

  Synchronize Isabelle + AFP repositories, based on "isabelle hg_sync".
""",
          "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
          "H" -> (_ => purge_heaps = true),
          "I:" -> (arg => session_images = session_images ::: List(arg)),
          "J" -> (_ => preserve_jars = true),
          "T" -> (_ => thorough = true),
          "a:" -> (arg => afp_rev = arg),
          "n" -> (_ => dry_run = true),
          "p:" -> (arg => ssh_port = Value.Int.parse(arg)),
          "r:" -> (arg => rev = arg),
          "s:" -> (arg => ssh_host = arg),
          "u:" -> (arg => ssh_user = arg),
          "v" -> (_ => verbose = true))

        val more_args = getopts(args)
        val target =
          more_args match {
            case List(target) => Path.explode(target)
            case _ => getopts.usage()
          }

        val options = Options.init()
        val progress = new Console_Progress(verbose = verbose)

        using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
          val context = Rsync.Context(progress = progress, ssh = ssh, stats = verbose)
          sync(options, context, target, thorough = thorough, purge_heaps = purge_heaps,
            session_images = session_images, preserve_jars = preserve_jars, dry_run = dry_run,
            rev = rev, dirs = afp_dirs(afp_root, afp_rev))
        }
      }
    )
}