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