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