/* Title: Pure/Admin/sync_repos.scala
Author: Makarius
Synchronize Isabelle + AFP repositories.
*/
package isabelle
object Sync_Repos {
def sync_repos(target: String,
progress: Progress = new Progress,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
clean: Boolean = false,
rev: String = "",
afp_root: Option[Path] = None,
afp_rev: String = ""
): Unit = {
val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
val afp_hg = afp_root.map(Mercurial.repository(_))
def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
hg.sync(dest, rev = r, progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, filter = filter)
progress.echo("\n* Isabelle repository:")
sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID"))
if (!dry_run) {
Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
val id_path = tmp_dir + Path.explode("ISABELLE_ID")
File.write(id_path, isabelle_hg.id(rev = rev))
Isabelle_System.rsync(thorough = thorough,
args = List(File.standard_path(id_path), target_dir + "etc/"))
}
}
for (hg <- afp_hg) {
progress.echo("\n* AFP repository:")
sync(hg, target_dir + "AFP", afp_rev)
}
}
val isabelle_tool =
Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
Scala_Project.here, { args =>
var afp_root: Option[Path] = None
var clean = false
var thorough = false
var afp_rev = ""
var dry_run = false
var rev = ""
var verbose = false
val getopts = Getopts("""
Usage: isabelle sync_repos [OPTIONS] TARGET
Options are:
-A ROOT include AFP with given root directory
-C clean all unknown/ignored files on target
(implies -n for testing; use option -f to confirm)
-T thorough check of file content (default: time and size)
-a REV explicit AFP revision (default: state of working directory)
-f force changes: no dry-run
-n no changes: dry-run
-r REV explicit revision (default: state of working directory)
-v verbose
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
Example (without -f as "dry-run"):
isabelle sync_repos -A '$AFP_BASE' -C testmachine:test/isabelle_afp
""",
"A:" -> (arg => afp_root = Some(Path.explode(arg))),
"C" -> { _ => clean = true; dry_run = true },
"T" -> (_ => thorough = true),
"a:" -> (arg => afp_rev = arg),
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"r:" -> (arg => rev = arg),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
val target =
more_args match {
case List(target) => target
case _ => getopts.usage()
}
val progress = new Console_Progress
sync_repos(target, progress = progress, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, rev = rev, afp_root = afp_root, afp_rev = afp_rev)
}
)
}