/* 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,
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, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
rev = r, 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(progress = progress, verbose = verbose,
args = List(File.standard_path(id_path), target_dir + "etc/")).check
}
}
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 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)
-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".
""",
"A:" -> (arg => afp_root = Some(Path.explode(arg))),
"C" -> { _ => clean = true; dry_run = 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, dry_run = dry_run, clean = clean,
rev = rev, afp_root = afp_root, afp_rev = afp_rev)
}
)
}