Admin/isasync
author huffman
Wed Oct 13 10:27:26 2010 -0700 (2010-10-13)
changeset 40010 d7fdd84b959f
parent 36859 51af1657263b
permissions -rwxr-xr-x
edit comments
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/"