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