|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # mirror script for Isabelle distribution or website |
|
6 |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG=`basename "$0"` |
|
11 |
|
12 usage() |
|
13 { |
|
14 echo |
|
15 echo "Usage: $PRG [OPTIONS] DEST" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -h print help message" |
|
19 echo " -n dry run, don't do anything, just report what would happen" |
|
20 echo " -w mirror whole Isabelle website" |
|
21 echo " -d delete files that are not on the server (BEWARE!)" |
|
22 echo |
|
23 exit 1 |
|
24 } |
|
25 |
|
26 fail() |
|
27 { |
|
28 echo "$1" >&2 |
|
29 exit 2 |
|
30 } |
|
31 |
|
32 |
|
33 ## process command line |
|
34 |
|
35 # options |
|
36 |
|
37 HELP="" |
|
38 ARGS="" |
|
39 SRC="isabelle-distribution" |
|
40 |
|
41 while getopts "hnwd" OPT |
|
42 do |
|
43 case "$OPT" in |
|
44 h) |
|
45 HELP=true |
|
46 ;; |
|
47 n) |
|
48 ARGS="$ARGS -n" |
|
49 ;; |
|
50 w) |
|
51 SRC="isabelle-website" |
|
52 ;; |
|
53 d) |
|
54 ARGS="$ARGS --delete" |
|
55 ;; |
|
56 \?) |
|
57 usage |
|
58 ;; |
|
59 esac |
|
60 done |
|
61 |
|
62 shift `expr $OPTIND - 1` |
|
63 |
|
64 |
|
65 # help |
|
66 |
|
67 if [ -n "$HELP" ]; then |
|
68 cat <<EOF |
|
69 |
|
70 Mirroring the Isabelle distribution or website |
|
71 ============================================== |
|
72 |
|
73 The Munich site maintains an rsync server for the Isabelle |
|
74 distribution or website. |
|
75 |
|
76 The rsync tool is very smart and efficient in mirroring large |
|
77 directory hierarchies. See http://rsync.samba.org/ for more |
|
78 information. The rsync-isabelle script provides a simple front-end |
|
79 for easy access to the Isabelle distribution. |
|
80 |
|
81 The script can be either run in conservative or clean-sweep mode. |
|
82 |
|
83 1) Basic mirroring works like this: |
|
84 |
|
85 $PRG /foo/bar |
|
86 |
|
87 where /foo/bar refers to your local copy of the Isabelle distribution |
|
88 (the base directory has to exist already). This operation is |
|
89 conservative in the sense that files are never deleted, thus garbage |
|
90 may accumulate over time as our master copy is changed. |
|
91 |
|
92 Avoiding garbage in your local copy requires some care. Rsync |
|
93 provides a way to delete all additional local files that are absent in |
|
94 the master copy. This provides an efficient way to purge large |
|
95 directory hierarchies, even unwillingly in case that a wrong |
|
96 destination is given! |
|
97 |
|
98 2a) This will invoke a safe dry-run of clean-sweep mirroring: |
|
99 |
|
100 $PRG -dn /foo/bar |
|
101 |
|
102 where additions and deletions will be printed without any actual |
|
103 changes performed so far. |
|
104 |
|
105 2b) Exact mirroring with actual deletion of garbage may be performed |
|
106 like this: |
|
107 |
|
108 $PRG -d /foo/bar |
|
109 |
|
110 |
|
111 After gaining some confidence in the workings of rsync-isabelle one |
|
112 would usually set up some automatic mirror scheme, e.g. a daily cron |
|
113 job run by the 'nobody' user. |
|
114 |
|
115 Add -w to the option list in order to mirror the whole Isabelle website |
|
116 |
|
117 EOF |
|
118 exit 0 |
|
119 fi |
|
120 |
|
121 |
|
122 # arguments |
|
123 |
|
124 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } |
|
125 |
|
126 DEST="$1"; shift; |
|
127 |
|
128 |
|
129 ## main |
|
130 |
|
131 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/." |