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