--- a/src/Doc/System/Misc.thy Tue May 31 20:55:51 2022 +0200
+++ b/src/Doc/System/Misc.thy Tue May 31 20:56:09 2022 +0200
@@ -320,6 +320,7 @@
-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)
-v verbose
Synchronize Mercurial repository with TARGET directory,
@@ -352,6 +353,9 @@
\<^medskip> Option \<^verbatim>\<open>-T\<close> indicates thorough treatment of file content and directory
times. The default is to consider files with equal time and size already as
equal, and to ignore time stamps on directories.
+
+ \<^medskip> Option \<^verbatim>\<open>-p\<close> specifies an explicit port for the SSH connection underlying
+ \<^verbatim>\<open>rsync\<close>.
\<close>
subsubsection \<open>Examples\<close>--- a/src/Pure/Admin/afp.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/Admin/afp.scala Tue May 31 20:56:09 2022 +0200
@@ -23,7 +23,9 @@
val force_partition1: List[String] = List("Category3", "HOL-ODE")
- def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
+ val BASE: Path = Path.explode("$AFP_BASE")
+
+ def init(options: Options, base_dir: Path = BASE): AFP =
new AFP(options, base_dir)
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Tue May 31 20:56:09 2022 +0200
@@ -46,7 +46,6 @@
{ logger =>
Isabelle_Devel.make_index()
- Mercurial.setup_repository(Isabelle_System.isabelle_repository.root, isabelle_repos)
Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos)
File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),--- a/src/Pure/Admin/sync_repos.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala Tue May 31 20:56:09 2022 +0200
@@ -10,6 +10,7 @@
object Sync_Repos {
def sync_repos(target: String,
progress: Progress = new Progress,
+ port: Int = SSH.default_port,
verbose: Boolean = false,
thorough: Boolean = false,
preserve_jars: Boolean = false,
@@ -27,8 +28,8 @@
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, verbose = verbose, thorough = thorough,
- dry_run = dry_run, clean = clean, filter = filter ::: more_filter)
+ 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"))
@@ -37,7 +38,7 @@
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(thorough = thorough,
+ Isabelle_System.rsync(port = port, thorough = thorough,
args = List(File.standard_path(id_path), target_dir + "etc/"))
}
}
@@ -58,13 +59,14 @@
var afp_rev = ""
var dry_run = false
var rev = ""
+ var port = SSH.default_port
var verbose = false
val getopts = Getopts("""
Usage: isabelle sync_repos [OPTIONS] TARGET
Options are:
- -A ROOT include AFP with given root directory
+ -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)
@@ -73,6 +75,7 @@
-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 + """)
-v verbose
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
@@ -81,13 +84,13 @@
* quick testing
- isabelle sync_repos -A '$AFP_BASE' -J -C testmachine:test/isabelle_afp
+ isabelle sync_repos -A: -J -C testmachine:test/isabelle_afp
* accurate testing
- isabelle sync_repos -A '$AFP_BASE' -T -C testmachine:test/isabelle_afp
+ isabelle sync_repos -A: -T -C testmachine:test/isabelle_afp
""",
- "A:" -> (arg => afp_root = Some(Path.explode(arg))),
+ "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),
@@ -95,6 +98,7 @@
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"r:" -> (arg => rev = arg),
+ "p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -105,7 +109,7 @@
}
val progress = new Console_Progress
- sync_repos(target, progress = progress, verbose = verbose, thorough = thorough,
+ 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)
}--- a/src/Pure/General/mercurial.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/General/mercurial.scala Tue May 31 20:56:09 2022 +0200
@@ -253,6 +253,7 @@
def sync(target: String,
progress: Progress = new Progress,
+ port: Int = SSH.default_port,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
@@ -279,7 +280,7 @@
(Nil, source)
}
Isabelle_System.rsync(
- progress = progress, verbose = verbose, thorough = thorough,
+ 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))
}
@@ -491,6 +492,7 @@
var thorough = false
var dry_run = false
var rev = ""
+ var port = SSH.default_port
var verbose = false
val getopts = Getopts("""
@@ -506,6 +508,7 @@
-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 + """)
-v verbose
Synchronize Mercurial repository with TARGET directory,
@@ -518,6 +521,7 @@
"f" -> (_ => dry_run = false),
"n" -> (_ => dry_run = true),
"r:" -> (arg => rev = arg),
+ "p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
@@ -533,7 +537,7 @@
case Some(dir) => repository(dir)
case None => the_repository(Path.current)
}
- hg.sync(target, progress = progress, verbose = verbose, thorough = thorough,
+ hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
dry_run = dry_run, clean = clean, filter = filter, rev = rev)
}
)--- a/src/Pure/General/ssh.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/General/ssh.scala Tue May 31 20:56:09 2022 +0200
@@ -40,8 +40,8 @@
val default_port = 22
def make_port(port: Int): Int = if (port > 0) port else default_port
- def port_suffix(port: Int, suffix: String = ":"): String =
- if (port == default_port) "" else suffix + port
+ def port_suffix(port: Int): String =
+ if (port == default_port) "" else ":" + port
def user_prefix(user: String): String =
proper_string(user) match {
@@ -328,6 +328,9 @@
override def hg_url: String =
"ssh://" + user_prefix(nominal_user) + nominal_host + "/"
+ override def rsync_prefix: String =
+ user_prefix(nominal_user) + nominal_host + ":"
+
override def toString: String =
user_prefix(session.getUserName) + host + port_suffix(port) +
(if (session.isConnected) "" else " (disconnected)")
@@ -489,6 +492,9 @@
def hg_url: String = ""
+ def rsync_prefix: String = ""
+ def rsync_path(path: Path): String = rsync_prefix + expand_path(path)
+
def expand_path(path: Path): Path = path.expand
def bash_path(path: Path): String = File.bash_path(path)
def is_dir(path: Path): Boolean = path.is_dir--- a/src/Pure/System/isabelle_system.scala Tue May 31 20:55:51 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue May 31 20:56:09 2022 +0200
@@ -423,6 +423,7 @@
def rsync(
cwd: JFile = null,
progress: Progress = new Progress,
+ port: Int = SSH.default_port,
verbose: Boolean = false,
thorough: Boolean = false,
dry_run: Boolean = false,
@@ -431,7 +432,7 @@
args: List[String] = Nil
): Unit = {
val script =
- "rsync --protect-args --archive" +
+ "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
(if (verbose || dry_run) " --verbose" else "") +
(if (thorough) " --ignore-times" else " --omit-dir-times") +
(if (dry_run) " --dry-run" else "") +