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,
|
|
13 |
verbose: Boolean = false,
|
|
14 |
dry_run: Boolean = false,
|
|
15 |
clean: Boolean = false,
|
|
16 |
rev: String = "",
|
|
17 |
afp_root: Option[Path] = None,
|
|
18 |
afp_rev: String = ""
|
|
19 |
): Unit = {
|
|
20 |
val target_dir = if (target.endsWith(":") || target.endsWith("/")) target else target + "/"
|
|
21 |
|
|
22 |
val isabelle_hg = Mercurial.repository(Path.ISABELLE_HOME)
|
|
23 |
val afp_hg = afp_root.map(Mercurial.repository(_))
|
|
24 |
|
|
25 |
def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
|
|
26 |
hg.sync(dest, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
|
|
27 |
rev = r, filter = filter)
|
|
28 |
|
|
29 |
progress.echo("\n* Isabelle repository:")
|
|
30 |
sync(isabelle_hg, target, rev, filter = List("protect /AFP", "protect etc/ISABELLE_ID"))
|
|
31 |
|
|
32 |
if (!dry_run) {
|
|
33 |
Isabelle_System.with_tmp_dir("sync_repos") { tmp_dir =>
|
|
34 |
val id_path = tmp_dir + Path.explode("ISABELLE_ID")
|
|
35 |
File.write(id_path, isabelle_hg.id(rev = rev))
|
75485
|
36 |
Isabelle_System.rsync(args = List(File.standard_path(id_path), target_dir + "etc/"))
|
75481
|
37 |
}
|
|
38 |
}
|
|
39 |
|
|
40 |
for (hg <- afp_hg) {
|
|
41 |
progress.echo("\n* AFP repository:")
|
|
42 |
sync(hg, target_dir + "AFP", afp_rev)
|
|
43 |
}
|
|
44 |
}
|
|
45 |
|
|
46 |
val isabelle_tool =
|
|
47 |
Isabelle_Tool("sync_repos", "synchronize Isabelle + AFP repositories",
|
|
48 |
Scala_Project.here, { args =>
|
|
49 |
var afp_root: Option[Path] = None
|
|
50 |
var clean = false
|
|
51 |
var afp_rev = ""
|
|
52 |
var dry_run = false
|
|
53 |
var rev = ""
|
|
54 |
var verbose = false
|
|
55 |
|
|
56 |
val getopts = Getopts("""
|
|
57 |
Usage: isabelle sync_repos [OPTIONS] TARGET
|
|
58 |
|
|
59 |
Options are:
|
|
60 |
-A ROOT include AFP with given root directory
|
|
61 |
-C clean all unknown/ignored files on target
|
|
62 |
(implies -n for testing; use option -f to confirm)
|
|
63 |
-a REV explicit AFP revision (default: state of working directory)
|
|
64 |
-f force changes: no dry-run
|
|
65 |
-n no changes: dry-run
|
|
66 |
-r REV explicit revision (default: state of working directory)
|
|
67 |
-v verbose
|
|
68 |
|
|
69 |
Synchronize Isabelle + AFP repositories; see also "isabelle hg_sync".
|
75486
|
70 |
|
|
71 |
Example (without -f as "dry-run"):
|
|
72 |
|
|
73 |
isabelle sync_repos -A '$AFP_BASE' -C testmachine:test/isabelle_afp
|
75481
|
74 |
""",
|
|
75 |
"A:" -> (arg => afp_root = Some(Path.explode(arg))),
|
|
76 |
"C" -> { _ => clean = true; dry_run = true },
|
|
77 |
"a:" -> (arg => afp_rev = arg),
|
|
78 |
"f" -> (_ => dry_run = false),
|
|
79 |
"n" -> (_ => dry_run = true),
|
|
80 |
"r:" -> (arg => rev = arg),
|
|
81 |
"v" -> (_ => verbose = true))
|
|
82 |
|
|
83 |
val more_args = getopts(args)
|
|
84 |
val target =
|
|
85 |
more_args match {
|
|
86 |
case List(target) => target
|
|
87 |
case _ => getopts.usage()
|
|
88 |
}
|
|
89 |
|
|
90 |
val progress = new Console_Progress
|
|
91 |
sync_repos(target, progress = progress, verbose = verbose, dry_run = dry_run, clean = clean,
|
|
92 |
rev = rev, afp_root = afp_root, afp_rev = afp_rev)
|
|
93 |
}
|
|
94 |
)
|
|
95 |
}
|