--- a/etc/build.props Fri Jun 10 13:48:37 2022 +0200
+++ b/etc/build.props Fri Jun 10 13:53:43 2022 +0200
@@ -38,7 +38,7 @@
src/Pure/Admin/isabelle_devel.scala \
src/Pure/Admin/jenkins.scala \
src/Pure/Admin/other_isabelle.scala \
- src/Pure/Admin/sync_repos.scala \
+ src/Pure/Admin/sync.scala \
src/Pure/Concurrent/consumer_thread.scala \
src/Pure/Concurrent/counter.scala \
src/Pure/Concurrent/delay.scala \
--- a/src/Pure/Admin/build_history.scala Fri Jun 10 13:48:37 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Fri Jun 10 13:53:43 2022 +0200
@@ -89,7 +89,7 @@
- /** local build --- from sync_repos directory **/
+ /** local build **/
private val default_user_home = Path.USER_HOME
private val default_multicore = (1, 1)
@@ -142,7 +142,7 @@
}
- /* Isabelle + AFP directory (produced via sync_repos) */
+ /* Isabelle + AFP directory */
def directory(dir: Path): Mercurial.Hg_Sync.Directory = {
val directory = Mercurial.Hg_Sync.directory(dir)
@@ -532,11 +532,11 @@
): List[(String, Bytes)] = {
/* synchronize Isabelle + AFP repositories */
- def sync_repos(target: Path, accurate: Boolean = false,
+ def sync(target: Path, accurate: Boolean = false,
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
val context = Rsync.Context(progress, port = ssh.nominal_port, protect_args = protect_args)
- Sync_Repos.sync_repos(context, ssh.rsync_path(target),
+ Sync.sync(context, ssh.rsync_path(target),
thorough = accurate, preserve_jars = !accurate,
rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
}
@@ -552,12 +552,12 @@
progress_stderr = progress.echo_if(echo, _),
strict = strict).check
- sync_repos(isabelle_self)
+ sync(isabelle_self)
execute("bin/isabelle", "components -I")
execute("bin/isabelle", "components -a", echo = true)
execute("bin/isabelle", "jedit -bf")
- sync_repos(isabelle_other, accurate = true,
+ sync(isabelle_other, accurate = true,
rev = proper_string(rev) getOrElse "tip",
afp_rev = proper_string(afp_rev) getOrElse "tip",
afp = true)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/sync.scala Fri Jun 10 13:53:43 2022 +0200
@@ -0,0 +1,104 @@
+/* Title: Pure/Admin/sync.scala
+ Author: Makarius
+
+Synchronize Isabelle + AFP repositories.
+*/
+
+package isabelle
+
+
+object Sync {
+ def sync(context: Rsync.Context, target: String,
+ verbose: Boolean = false,
+ thorough: Boolean = false,
+ preserve_jars: Boolean = false,
+ dry_run: Boolean = false,
+ rev: String = "",
+ afp_root: Option[Path] = None,
+ afp_rev: String = ""
+ ): Unit = {
+ 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,
+ contents: List[File.Content] = Nil, filter: List[String] = Nil
+ ): Unit = {
+ hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
+ contents = contents, filter = filter ::: more_filter)
+ }
+
+ context.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) {
+ context.progress.echo_if(verbose, "\n* AFP repository:")
+ sync(hg, Rsync.append(target, "AFP"), afp_rev)
+ }
+ }
+
+ val isabelle_tool =
+ Isabelle_Tool("sync", "synchronize Isabelle + AFP repositories",
+ Scala_Project.here, { args =>
+ var afp_root: Option[Path] = None
+ var preserve_jars = false
+ var protect_args = false
+ var thorough = false
+ var afp_rev = ""
+ var dry_run = false
+ var rev = ""
+ var port = SSH.default_port
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle sync [OPTIONS] TARGET
+
+ Options are:
+ -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
+ -J preserve *.jar files
+ -S robust (but less portable) treatment of spaces in directory names
+ -T thorough treatment of file content and directory times
+ -a REV explicit AFP revision (default: state of working directory)
+ -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".
+
+ Example: quick testing
+
+ isabelle sync -A: -J testmachine:test/isabelle_afp
+
+ Example: accurate testing
+
+ isabelle sync -A: -T testmachine:test/isabelle_afp
+""",
+ "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
+ "J" -> (_ => preserve_jars = true),
+ "S" -> (_ => protect_args = true),
+ "T" -> (_ => thorough = true),
+ "a:" -> (arg => afp_rev = arg),
+ "n" -> (_ => dry_run = true),
+ "r:" -> (arg => rev = arg),
+ "p:" -> (arg => port = Value.Int.parse(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
+ val context = Rsync.Context(progress, port = port, protect_args = protect_args)
+ sync(context, target, verbose = verbose, thorough = thorough,
+ preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
+ afp_rev = afp_rev)
+ }
+ )
+}
--- a/src/Pure/Admin/sync_repos.scala Fri Jun 10 13:48:37 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,104 +0,0 @@
-/* Title: Pure/Admin/sync_repos.scala
- Author: Makarius
-
-Synchronize Isabelle + AFP repositories.
-*/
-
-package isabelle
-
-
-object Sync_Repos {
- def sync_repos(context: Rsync.Context, target: String,
- verbose: Boolean = false,
- thorough: Boolean = false,
- preserve_jars: Boolean = false,
- dry_run: Boolean = false,
- rev: String = "",
- afp_root: Option[Path] = None,
- afp_rev: String = ""
- ): Unit = {
- 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,
- contents: List[File.Content] = Nil, filter: List[String] = Nil
- ): Unit = {
- hg.sync(context, dest, rev = r, verbose = verbose, thorough = thorough, dry_run = dry_run,
- contents = contents, filter = filter ::: more_filter)
- }
-
- context.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) {
- context.progress.echo_if(verbose, "\n* AFP repository:")
- sync(hg, Rsync.append(target, "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 preserve_jars = false
- var protect_args = false
- var thorough = false
- 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 (":" for """ + AFP.BASE.implode + """)
- -J preserve *.jar files
- -S robust (but less portable) treatment of spaces in directory names
- -T thorough treatment of file content and directory times
- -a REV explicit AFP revision (default: state of working directory)
- -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".
-
- Example: quick testing
-
- isabelle sync_repos -A: -J testmachine:test/isabelle_afp
-
- Example: accurate testing
-
- 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),
- "S" -> (_ => protect_args = true),
- "T" -> (_ => thorough = true),
- "a:" -> (arg => afp_rev = arg),
- "n" -> (_ => dry_run = true),
- "r:" -> (arg => rev = arg),
- "p:" -> (arg => port = Value.Int.parse(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
- val context = Rsync.Context(progress, port = port, protect_args = protect_args)
- sync_repos(context, target, verbose = verbose, thorough = thorough,
- preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
- afp_rev = afp_rev)
- }
- )
-}
--- a/src/Pure/System/isabelle_tool.scala Fri Jun 10 13:48:37 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala Fri Jun 10 13:53:43 2022 +0200
@@ -226,7 +226,7 @@
Build_Zipperposition.isabelle_tool,
Check_Sources.isabelle_tool,
Components.isabelle_tool,
- Sync_Repos.isabelle_tool,
+ Sync.isabelle_tool,
isabelle.vscode.Build_VSCode.isabelle_tool,
isabelle.vscode.Build_VSCodium.isabelle_tool1,
isabelle.vscode.Build_VSCodium.isabelle_tool2,