--- 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 \<open>
The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with
- a target directory, using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close>
- notation for destinations.
+ a target directory.
@{verbatim [display]
\<open>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).\<close>}
The \<^verbatim>\<open>TARGET\<close> specification can be a local or remote directory (via ssh),
- using \<^verbatim>\<open>rsync\<close> notation (see examples below). The content is written
- directly into the target, \<^emph>\<open>without\<close> creating a separate sub-directory.
+ using \<^verbatim>\<open>rsync\<close>\<^footnote>\<open>\<^url>\<open>https://linux.die.net/man/1/rsync\<close>\<close> notation for
+ destinations; see also examples below. The content is written directly into
+ the target, \<^emph>\<open>without\<close> creating a separate sub-directory. The special
+ sub-directory \<^verbatim>\<open>.hg_sync\<close> within the target contains meta data from the
+ original Mercurial repository. Repeated synchronization is guarded by the
+ presence of a \<^verbatim>\<open>.hg_sync\<close> sub-directory: this sanity check prevents
+ accidental changes (or deletion!) of targets that were not created by @{tool
+ hg_sync}.
\<^medskip> Option \<^verbatim>\<open>-r\<close> specifies an explicit revision of the repository; the default
is the current state of the working directory (which might be uncommitted).
\<^medskip> Option \<^verbatim>\<open>-v\<close> enables verbose mode. Option \<^verbatim>\<open>-n\<close> enables ``dry-run'' mode:
- operations are only simulated and printed as in verbose mode. Option \<^verbatim>\<open>-f\<close>
- disables ``dry-run'' mode and thus forces changes to be applied.
-
- \<^medskip> Option \<^verbatim>\<open>-C\<close> 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>\<open>-C\<close> implies option \<^verbatim>\<open>-n\<close>,
- for ``dry-run'' with verbose output. A subsequent option \<^verbatim>\<open>-f\<close> is required
- to force actual deletions on the target.
+ operations are only simulated; use it with option \<^verbatim>\<open>-v\<close> to actually see
+ results.
\<^medskip> Option \<^verbatim>\<open>-F\<close> adds a filter rule to the underlying \<^verbatim>\<open>rsync\<close> command;
multiple \<^verbatim>\<open>-F\<close> options may be given to accumulate a list of rules.
@@ -363,10 +360,7 @@
text \<open>
Synchronize the current repository onto a remote host, with accurate
treatment of all content:
- @{verbatim [display] \<open> isabelle hg_sync -T -C remotename:test/repos\<close>}
-
- So far, this is only a dry run. In a realistic situation, it requires
- consecutive options \<^verbatim>\<open>-C -f\<close> as confirmation.
+ @{verbatim [display] \<open> isabelle hg_sync -T remotename:test/repos\<close>}
\<close>
--- 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)
--- 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) }
--- 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)
}
)
}
--- 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) {
--- 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)
}
)
}
--- 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) => (),
--- 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(