# HG changeset patch # User wenzelm # Date 1654453008 -7200 # Node ID 8c32f0210a1aa37ed5a5b4fbe05dcff5c7377bd4 # Parent a7c6722fbaf1769a379af9ebfdda2a8841a93e48# Parent 0c2ff768caf51dd8f7761e1947db1f57baf4cc01 merged diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Doc/System/Misc.thy Sun Jun 05 20:16:48 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 a7c6722fbaf1 -r 8c32f0210a1a src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/Admin/build_history.scala Sun Jun 05 20:16:48 2022 +0200 @@ -551,7 +551,7 @@ strict = strict).check if (self_update) { - val hg = Mercurial.repository(Path.ISABELLE_HOME) + val hg = Mercurial.self_repository() hg.push(self_hg.root_url, force = true) self_hg.update(rev = hg.parent(), clean = true) diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/Admin/build_release.scala Sun Jun 05 20:16:48 2022 +0200 @@ -398,7 +398,7 @@ ): Unit = { val progress = context.progress - val hg = Mercurial.repository(Path.ISABELLE_HOME) + val hg = Mercurial.self_repository() val id = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Pure/Admin/sync_repos.scala --- a/src/Pure/Admin/sync_repos.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/Admin/sync_repos.scala Sun Jun 05 20:16:48 2022 +0200 @@ -15,37 +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 isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME) + 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 = + 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, clean = clean, filter = filter ::: more_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") { tmp_dir => - val id_path = tmp_dir + Path.explode("ISABELLE_ID") - File.write(id_path, isabelle_hg.id(rev = rev)) - Isabelle_System.rsync(port = port, thorough = thorough, - args = List(File.standard_path(id_path), target_dir + "etc/")) - } + thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter) } + 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")) + for (hg <- afp_hg) { - progress.echo("\n* AFP repository:") - sync(hg, target_dir + "AFP", afp_rev) + progress.echo_if(verbose, "\n* AFP repository:") + sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev) } } @@ -53,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 = "" @@ -68,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 + """) @@ -80,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)), @@ -110,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 a7c6722fbaf1 -r 8c32f0210a1a src/Pure/General/file.scala --- a/src/Pure/General/file.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/General/file.scala Sun Jun 05 20:16:48 2022 +0200 @@ -307,11 +307,19 @@ } final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content { - def write(dir: Path): Unit = Bytes.write(dir + path, content) + def write(dir: Path): Unit = { + val full_path = dir + path + Isabelle_System.make_directory(full_path.expand.dir) + Bytes.write(full_path, content) + } } final class Content_String private[File](val path: Path, content: String) extends Content { - def write(dir: Path): Unit = File.write(dir + path, content) + def write(dir: Path): Unit = { + val full_path = dir + path + Isabelle_System.make_directory(full_path.expand.dir) + File.write(full_path, content) + } } final class Content_XML private[File](val path: Path, content: XML.Body) { diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/General/mercurial.scala Sun Jun 05 20:16:48 2022 +0200 @@ -115,18 +115,57 @@ archive_info(root).map(info => info.tags.mkString(" ")) + /* hg_sync meta data */ + + object Hg_Sync { + val NAME = ".hg_sync" + val _NAME: String = " " + NAME + val PATH: Path = Path.explode(NAME) + val PATH_ID: Path = PATH + Path.explode("id") + val PATH_LOG: Path = PATH + Path.explode("log") + val PATH_DIFF: Path = PATH + Path.explode("diff") + val PATH_STAT: Path = PATH + Path.explode("stat") + + def is_directory(root: Path, ssh: SSH.System = SSH.Local): Boolean = + ssh.is_dir(root + PATH) + + def directory(root: Path, ssh: SSH.System = SSH.Local): Directory = { + if (is_directory(root, ssh = ssh)) new Directory(root, ssh) + else error("No .hg_sync directory found in " + ssh.rsync_path(root)) + } + + class Directory private [Hg_Sync](val root: Path, val ssh: SSH.System) + { + override def toString: String = ssh.rsync_path(root) + + def read(path: Path): String = ssh.read(root + path) + lazy val id: String = read(PATH_ID) + lazy val log: String = read(PATH_LOG) + lazy val diff: String = read(PATH_DIFF) + lazy val stat: String = read(PATH_STAT) + + def changed: Boolean = id.endsWith("+") + } + } + + /* repository access */ def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean = ssh.is_dir(root + Path.explode(".hg")) && new Repository(root, ssh).command("root").ok + def id_repository(root: Path, ssh: SSH.System = SSH.Local, rev: String = "tip"): Option[String] = + if (is_repository(root, ssh = ssh)) Some(repository(root, ssh = ssh).id(rev = rev)) else None + def repository(root: Path, ssh: SSH.System = SSH.Local): Repository = { val hg = new Repository(root, ssh) hg.command("root").check hg } + def self_repository(): Repository = repository(Path.ISABELLE_HOME) + def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] = { @tailrec def find(root: Path): Option[Repository] = if (is_repository(root, ssh)) Some(repository(root, ssh = ssh)) @@ -221,6 +260,9 @@ def log(rev: String = "", template: String = "", options: String = ""): String = hg.command("log", opt_rev(rev) + opt_template(template), options).check.out + def diff(rev: String = "", options: String = ""): String = + hg.command("diff", opt_rev(rev), options).check.out + def parent(): String = log(rev = "p1()", template = "{node|short}") def push( @@ -257,13 +299,36 @@ 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._NAME))) { + error("No .hg_sync meta data in " + quote(target)) + } + + val id_content = id(rev = rev) + val is_changed = id_content.endsWith("+") + val log_content = if (is_changed) "" else log(rev = rev, options = "-l1") + val diff_content = if (is_changed) diff(rev = rev, options = "--git") else "" + val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else "" + + Isabelle_System.rsync_init(target, port = port, + contents = + File.Content(Hg_Sync.PATH_ID, id_content) :: + File.Content(Hg_Sync.PATH_LOG, log_content) :: + File.Content(Hg_Sync.PATH_DIFF, diff_content) :: + File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents) + val (options, source) = if (rev.isEmpty) { val exclude_path = tmp_dir + Path.explode("exclude") @@ -279,10 +344,18 @@ archive(source, rev = rev) (Nil, source) } + + val protect = + (Hg_Sync.PATH :: 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 } } @@ -486,7 +559,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 @@ -499,13 +571,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 + """) @@ -514,11 +584,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)), @@ -538,7 +606,7 @@ case None => the_repository(Path.current) } hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough, - dry_run = dry_run, clean = clean, filter = filter, rev = rev) + dry_run = dry_run, filter = filter, rev = rev) } ) } diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/General/ssh.scala Sun Jun 05 20:16:48 2022 +0200 @@ -439,8 +439,8 @@ override def read_file(path: Path, local_path: Path): Unit = sftp.get(remote_path(path), File.platform_path(local_path)) - def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) - def read(path: Path): String = using(open_input(path))(File.read_stream) + override def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) + override def read(path: Path): String = using(open_input(path))(File.read_stream) override def write_file(path: Path, local_path: Path): Unit = sftp.put(File.platform_path(local_path), remote_path(path)) @@ -503,6 +503,8 @@ def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) + def read_bytes(path: Path): Bytes = Bytes.read(path) + def read(path: Path): String = File.read(path) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), diff -r a7c6722fbaf1 -r 8c32f0210a1a src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Jun 04 15:59:24 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun Jun 05 20:16:48 2022 +0200 @@ -102,10 +102,10 @@ /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = - getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { - if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() - else error("Failed to identify Isabelle distribution " + root.expand) - } + getetc("ISABELLE_ID", root = root) orElse + Mercurial.archive_id(root) orElse + Mercurial.id_repository(root, rev = "") getOrElse + error("Failed to identify Isabelle distribution " + root.expand) object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here @@ -426,22 +426,43 @@ 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 - ): Unit = { + ): Process_Result = { val script = "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) + - (if (verbose || dry_run) " --verbose" else "") + + (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).check + 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(