# HG changeset patch # User wenzelm # Date 1654449595 -7200 # Node ID b32fdb67f851413c9203b297834e6afcac3e8693 # Parent 0106c89fb71f849b20adba8c4da2d6c127537f8d provide .hg_sync meta data; always clean target, but guard it wrt. .hg_sync for robustness (no need for dry-run); updated and clarified documentation; diff -r 0106c89fb71f -r b32fdb67f851 src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Sat Jun 04 16:54:24 2022 +0200 +++ b/src/Doc/System/Misc.thy Sun Jun 05 19:19:55 2022 +0200 @@ -304,20 +304,17 @@ text \ The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with - a target directory, using \<^verbatim>\rsync\\<^footnote>\\<^url>\https://linux.die.net/man/1/rsync\\ - notation for destinations. + a target directory. @{verbatim [display] \Usage: isabelle hg_sync [OPTIONS] TARGET Options are: - -C clean all unknown/ignored files on target - (implies -n for testing; use option -f to confirm) - -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) + -F RULE add rsync filter RULE + (e.g. "protect /foo" to avoid deletion) -R ROOT explicit repository root directory (default: implicit from current directory) -T thorough treatment of file content and directory times - -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) -p PORT explicit SSH port (default: 22) @@ -327,21 +324,21 @@ which can be local or remote (using notation of rsync).\} The \<^verbatim>\TARGET\ specification can be a local or remote directory (via ssh), - using \<^verbatim>\rsync\ notation (see examples below). The content is written - directly into the target, \<^emph>\without\ creating a separate sub-directory. + using \<^verbatim>\rsync\\<^footnote>\\<^url>\https://linux.die.net/man/1/rsync\\ notation for + destinations; see also examples below. The content is written directly into + the target, \<^emph>\without\ creating a separate sub-directory. The special + sub-directory \<^verbatim>\.hg_sync\ within the target contains meta data from the + original Mercurial repository. Repeated synchronization is guarded by the + presence of a \<^verbatim>\.hg_sync\ sub-directory: this sanity check prevents + accidental changes (or deletion!) of targets that were not created by @{tool + hg_sync}. \<^medskip> Option \<^verbatim>\-r\ specifies an explicit revision of the repository; the default is the current state of the working directory (which might be uncommitted). \<^medskip> Option \<^verbatim>\-v\ enables verbose mode. Option \<^verbatim>\-n\ enables ``dry-run'' mode: - operations are only simulated and printed as in verbose mode. Option \<^verbatim>\-f\ - disables ``dry-run'' mode and thus forces changes to be applied. - - \<^medskip> Option \<^verbatim>\-C\ causes deletion of all unknown/ignored files on the target. - This is potentially dangerous: giving a wrong target directory will cause - its total destruction! For robustness, option \<^verbatim>\-C\ implies option \<^verbatim>\-n\, - for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\-f\ is required - to force actual deletions on the target. + operations are only simulated; use it with option \<^verbatim>\-v\ to actually see + results. \<^medskip> Option \<^verbatim>\-F\ adds a filter rule to the underlying \<^verbatim>\rsync\ command; multiple \<^verbatim>\-F\ options may be given to accumulate a list of rules. @@ -363,10 +360,7 @@ text \ Synchronize the current repository onto a remote host, with accurate treatment of all content: - @{verbatim [display] \ isabelle hg_sync -T -C remotename:test/repos\} - - So far, this is only a dry run. In a realistic situation, it requires - consecutive options \<^verbatim>\-C -f\ as confirmation. + @{verbatim [display] \ isabelle hg_sync -T remotename:test/repos\} \ diff -r 0106c89fb71f -r b32fdb67f851 src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Sat Jun 04 16:54:24 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Sun Jun 05 19:19:55 2022 +0200 @@ -15,38 +15,30 @@ thorough: Boolean = false, preserve_jars: 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 hg = Mercurial.self_repository() val afp_hg = afp_root.map(Mercurial.repository(_)) val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil - def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit = - hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose || dry_run, - thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter) + def sync(hg: Mercurial.Repository, dest: String, r: String, + contents: List[File.Content] = Nil, filter: List[String] = Nil + ): Unit = { + hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose, + thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter) + } progress.echo("\n* Isabelle repository:") - sync(hg, target, rev, filter = List("protect /AFP", "protect /etc/ISABELLE_ID")) - - if (!dry_run) { - Isabelle_System.with_tmp_dir("sync") { tmp_dir => - val id_path = tmp_dir + Path.explode("ISABELLE_ID") - File.write(id_path, hg.id(rev = rev)) - Isabelle_System.rsync(port = port, thorough = thorough, - args = List(File.standard_path(id_path), target_dir + "etc/") - ).check - } - } + sync(hg, target, rev, + contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))), + filter = List("protect /AFP")) for (hg <- afp_hg) { progress.echo("\n* AFP repository:") - sync(hg, target_dir + "AFP", afp_rev) + sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev) } } @@ -54,7 +46,6 @@ Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories", Scala_Project.here, { args => var afp_root: Option[Path] = None - var clean = false var preserve_jars = false var thorough = false var afp_rev = "" @@ -69,11 +60,8 @@ Options are: -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -J preserve *.jar files - -C clean all unknown/ignored files on target - (implies -n for testing; use option -f to confirm) -T thorough treatment of file content and directory times -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) -p PORT explicit SSH port (default: """ + SSH.default_port + """) @@ -81,22 +69,18 @@ Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync". - Examples (without -f as "dry-run"): + Example: quick testing - * quick testing + isabelle sync_repos -A: -J testmachine:test/isabelle_afp - isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp + Example: accurate testing - * accurate testing - - isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp + isabelle sync_repos -A: -T testmachine:test/isabelle_afp """, "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), "J" -> (_ => preserve_jars = true), - "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), "p:" -> (arg => port = Value.Int.parse(arg)), @@ -111,8 +95,8 @@ val progress = new Console_Progress sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough, - preserve_jars = preserve_jars, dry_run = dry_run, clean = clean, rev = rev, - afp_root = afp_root, afp_rev = afp_rev) + preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root, + afp_rev = afp_rev) } ) } diff -r 0106c89fb71f -r b32fdb67f851 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Jun 04 16:54:24 2022 +0200 +++ b/src/Pure/General/mercurial.scala Sun Jun 05 19:19:55 2022 +0200 @@ -115,6 +115,12 @@ archive_info(root).map(info => info.tags.mkString(" ")) + /* hg_sync meta data */ + + val HG_SYNC: Path = Path.explode(".hg_sync") + val HG_SYNC_ID: Path = HG_SYNC + Path.explode("id") + + /* repository access */ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = @@ -262,13 +268,26 @@ verbose: Boolean = false, thorough: Boolean = false, dry_run: Boolean = false, - clean: Boolean = false, filter: List[String] = Nil, + contents: List[File.Content] = Nil, rev: String = "" ): Unit = { require(ssh == SSH.Local, "local repository required") Isabelle_System.with_tmp_dir("sync") { tmp_dir => + Isabelle_System.rsync_init(target, port = port) + + val list = + Isabelle_System.rsync(port = port, list = true, + args = List("--", Isabelle_System.rsync_dir(target)) + ).check.out_lines.filterNot(_.endsWith(" .")) + if (list.nonEmpty && !list.exists(_.endsWith(" .hg_sync"))) { + error("No .hg_sync meta data in " + quote(target)) + } + + Isabelle_System.rsync_init(target, port = port, + contents = File.Content(HG_SYNC_ID, id(rev = rev)) :: contents) + val (options, source) = if (rev.isEmpty) { val exclude_path = tmp_dir + Path.explode("exclude") @@ -284,10 +303,16 @@ archive(source, rev = rev) (Nil, source) } + + val protect = + (HG_SYNC :: contents.map(_.path)).map(path => "protect /" + File.standard_path(path)) Isabelle_System.rsync( progress = progress, port = port, verbose = verbose, thorough = thorough, - dry_run = dry_run, clean = clean, filter = filter, - args = List("--prune-empty-dirs") ::: options ::: List("--", source + "/.", target) + dry_run = dry_run, + clean = true, + prune_empty_dirs = true, + filter = protect ::: filter, + args = options ::: List("--", Isabelle_System.rsync_dir(source), target) ).check } } @@ -492,7 +517,6 @@ val isabelle_tool2 = Isabelle_Tool("hg_sync", "synchronize Mercurial repository with target directory", Scala_Project.here, { args => - var clean = false var filter: List[String] = Nil var root: Option[Path] = None var thorough = false @@ -505,13 +529,11 @@ Usage: isabelle hg_sync [OPTIONS] TARGET Options are: - -C clean all unknown/ignored files on target - (implies -n for testing; use option -f to confirm) - -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) + -F RULE add rsync filter RULE + (e.g. "protect /foo" to avoid deletion) -R ROOT explicit repository root directory (default: implicit from current directory) -T thorough treatment of file content and directory times - -f force changes: no dry-run -n no changes: dry-run -r REV explicit revision (default: state of working directory) -p PORT explicit SSH port (default: """ + SSH.default_port + """) @@ -520,11 +542,9 @@ Synchronize Mercurial repository with TARGET directory, which can be local or remote (using notation of rsync). """, - "C" -> { _ => clean = true; dry_run = true }, "F:" -> (arg => filter = filter ::: List(arg)), "R:" -> (arg => root = Some(Path.explode(arg))), "T" -> (_ => thorough = true), - "f" -> (_ => dry_run = false), "n" -> (_ => dry_run = true), "r:" -> (arg => rev = arg), "p:" -> (arg => port = Value.Int.parse(arg)), @@ -543,8 +563,8 @@ case Some(dir) => repository(dir) case None => the_repository(Path.current) } - hg.sync(target, progress = progress, port = port, verbose = verbose || dry_run, - thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, rev = rev) + hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough, + dry_run = dry_run, filter = filter, rev = rev) } ) } diff -r 0106c89fb71f -r b32fdb67f851 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Jun 04 16:54:24 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun Jun 05 19:19:55 2022 +0200 @@ -426,8 +426,10 @@ port: Int = SSH.default_port, verbose: Boolean = false, thorough: Boolean = false, + prune_empty_dirs: Boolean = false, dry_run: Boolean = false, clean: Boolean = false, + list: Boolean = false, filter: List[String] = Nil, args: List[String] = Nil ): Process_Result = { @@ -435,13 +437,32 @@ "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + (if (verbose) " --verbose" else "") + (if (thorough) " --ignore-times" else " --omit-dir-times") + + (if (prune_empty_dirs) " --prune-empty-dirs" else "") + (if (dry_run) " --dry-run" else "") + (if (clean) " --delete-excluded" else "") + + (if (list) " --list-only --no-human-readable" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString + (if (args.nonEmpty) " " + Bash.strings(args) else "") progress.bash(script, cwd = cwd, echo = true) } + def rsync_dir(target: String): String = { + if (target.endsWith(":.") || target.endsWith("/.")) target + else if (target.endsWith(":") || target.endsWith("/")) target + "." + else target + "/." + } + + def rsync_init(target: String, + port: Int = SSH.default_port, + contents: List[File.Content] = Nil + ): Unit = + with_tmp_dir("sync") { tmp_dir => + val init_dir = make_directory(tmp_dir + Path.explode("init")) + contents.foreach(_.write(init_dir)) + rsync(port = port, thorough = true, + args = List(File.bash_path(init_dir) + "/.", target)).check + } + def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash(