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