75481
|
1 |
/* Title: Pure/Admin/sync_repos.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Synchronize Isabelle + AFP repositories.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
object Sync_Repos {
|
|
11 |
def sync_repos(target: String,
|
|
12 |
progress: Progress = new Progress,
|
75499
|
13 |
port: Int = SSH.default_port,
|
75481
|
14 |
verbose: Boolean = false,
|
75487
|
15 |
thorough: Boolean = false,
|
75492
|
16 |
preserve_jars: Boolean = false,
|
75481
|
17 |
dry_run: Boolean = false,
|
|
18 |
rev: String = "",
|
|
19 |
afp_root: Option[Path] = None,
|
|
20 |
afp_rev: String = ""
|
|
21 |
): Unit = {
|
75506
|
22 |
val hg = Mercurial.self_repository()
|
75481
|
23 |
val afp_hg = afp_root.map(Mercurial.repository(_))
|
|
24 |
|
75492
|
25 |
val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
|
|
26 |
|
75511
|
27 |
def sync(hg: Mercurial.Repository, dest: String, r: String,
|
|
28 |
contents: List[File.Content] = Nil, filter: List[String] = Nil
|
|
29 |
): Unit = {
|
|
30 |
hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose,
|
|
31 |
thorough = thorough, dry_run = dry_run, contents = contents, filter = filter ::: more_filter)
|
|
32 |
}
|
75481
|
33 |
|
|
34 |
progress.echo("\n* Isabelle repository:")
|
75511
|
35 |
sync(hg, target, rev,
|
|
36 |
contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
|
|
37 |
filter = List("protect /AFP"))
|
75481
|
38 |
|
|
39 |
for (hg <- afp_hg) {
|
|
40 |
progress.echo("\n* AFP repository:")
|
75511
|
41 |
sync(hg, Isabelle_System.rsync_dir(target) + "/AFP", afp_rev)
|
75481
|
42 |
}
|
|
43 |
}
|
|
44 |
|
|
45 |
val isabelle_tool =
|
|
46 |
Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
|
|
47 |
Scala_Project.here, { args =>
|
|
48 |
var afp_root: Option[Path] = None
|
75492
|
49 |
var preserve_jars = false
|
75487
|
50 |
var thorough = false
|
75481
|
51 |
var afp_rev = ""
|
|
52 |
var dry_run = false
|
|
53 |
var rev = ""
|
75499
|
54 |
var port = SSH.default_port
|
75481
|
55 |
var verbose = false
|
|
56 |
|
|
57 |
val getopts = Getopts("""
|
|
58 |
Usage: isabelle sync_repos [OPTIONS] TARGET
|
|
59 |
|
|
60 |
Options are:
|
75497
|
61 |
-A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
|
75492
|
62 |
-J preserve *.jar files
|
75493
|
63 |
-T thorough treatment of file content and directory times
|
75481
|
64 |
-a REV explicit AFP revision (default: state of working directory)
|
|
65 |
-n no changes: dry-run
|
|
66 |
-r REV explicit revision (default: state of working directory)
|
75499
|
67 |
-p PORT explicit SSH port (default: """ + SSH.default_port + """)
|
75481
|
68 |
-v verbose
|
|
69 |
|
|
70 |
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
|
75486
|
71 |
|
75511
|
72 |
Example: quick testing
|
75492
|
73 |
|
75511
|
74 |
isabelle sync_repos -A: -J testmachine:test/isabelle_afp
|
75486
|
75 |
|
75511
|
76 |
Example: accurate testing
|
75492
|
77 |
|
75511
|
78 |
isabelle sync_repos -A: -T testmachine:test/isabelle_afp
|
75481
|
79 |
""",
|
75497
|
80 |
"A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
|
75492
|
81 |
"J" -> (_ => preserve_jars = true),
|
75487
|
82 |
"T" -> (_ => thorough = true),
|
75481
|
83 |
"a:" -> (arg => afp_rev = arg),
|
|
84 |
"n" -> (_ => dry_run = true),
|
|
85 |
"r:" -> (arg => rev = arg),
|
75499
|
86 |
"p:" -> (arg => port = Value.Int.parse(arg)),
|
75481
|
87 |
"v" -> (_ => verbose = true))
|
|
88 |
|
|
89 |
val more_args = getopts(args)
|
|
90 |
val target =
|
|
91 |
more_args match {
|
|
92 |
case List(target) => target
|
|
93 |
case _ => getopts.usage()
|
|
94 |
}
|
|
95 |
|
|
96 |
val progress = new Console_Progress
|
75499
|
97 |
sync_repos(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
|
75511
|
98 |
preserve_jars = preserve_jars, dry_run = dry_run, rev = rev, afp_root = afp_root,
|
|
99 |
afp_rev = afp_rev)
|
75481
|
100 |
}
|
|
101 |
)
|
|
102 |
}
|