1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/isasync	Tue Sep 27 15:30:37 2005 +0200
     1.3 @@ -0,0 +1,131 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# $Id$
     1.7 +#
     1.8 +# mirror script for Isabelle distribution or website
     1.9 +
    1.10 +
    1.11 +## diagnostics
    1.12 +
    1.13 +PRG=`basename "$0"`
    1.14 +
    1.15 +usage()
    1.16 +{
    1.17 +  echo
    1.18 +  echo "Usage: $PRG [OPTIONS] DEST"
    1.19 +  echo
    1.20 +  echo "  Options are:"
    1.21 +  echo "    -h    print help message"
    1.22 +  echo "    -n    dry run, don't do anything, just report what would happen"
    1.23 +  echo "    -w    mirror whole Isabelle website"
    1.24 +  echo "    -d    delete files that are not on the server (BEWARE!)"
    1.25 +  echo
    1.26 +  exit 1
    1.27 +}
    1.28 +
    1.29 +fail()
    1.30 +{
    1.31 +  echo "$1" >&2
    1.32 +  exit 2
    1.33 +}
    1.34 +
    1.35 +
    1.36 +## process command line
    1.37 +
    1.38 +# options
    1.39 +
    1.40 +HELP=""
    1.41 +ARGS=""
    1.42 +SRC="isabelle-distribution"
    1.43 +
    1.44 +while getopts "hnwd" OPT
    1.45 +do
    1.46 +  case "$OPT" in
    1.47 +    h)
    1.48 +      HELP=true
    1.49 +      ;;
    1.50 +    n)
    1.51 +      ARGS="$ARGS -n"
    1.52 +      ;;
    1.53 +    w)
    1.54 +      SRC="isabelle-website"
    1.55 +      ;;
    1.56 +    d)
    1.57 +      ARGS="$ARGS --delete"
    1.58 +      ;;
    1.59 +    \?)
    1.60 +      usage
    1.61 +      ;;
    1.62 +  esac
    1.63 +done
    1.64 +
    1.65 +shift `expr $OPTIND - 1`
    1.66 +
    1.67 +
    1.68 +# help
    1.69 +
    1.70 +if [ -n "$HELP" ]; then
    1.71 +  cat <<EOF
    1.72 +
    1.73 +Mirroring the Isabelle distribution or website
    1.74 +==============================================
    1.75 +
    1.76 +The Munich site maintains an rsync server for the Isabelle
    1.77 +distribution or website.
    1.78 +
    1.79 +The rsync tool is very smart and efficient in mirroring large
    1.80 +directory hierarchies.  See http://rsync.samba.org/ for more
    1.81 +information.  The rsync-isabelle script provides a simple front-end
    1.82 +for easy access to the Isabelle distribution.
    1.83 +
    1.84 +The script can be either run in conservative or clean-sweep mode.
    1.85 +
    1.86 +1) Basic mirroring works like this:
    1.87 +
    1.88 +  $PRG /foo/bar
    1.89 +
    1.90 +where /foo/bar refers to your local copy of the Isabelle distribution
    1.91 +(the base directory has to exist already).  This operation is
    1.92 +conservative in the sense that files are never deleted, thus garbage
    1.93 +may accumulate over time as our master copy is changed.
    1.94 +
    1.95 +Avoiding garbage in your local copy requires some care.  Rsync
    1.96 +provides a way to delete all additional local files that are absent in
    1.97 +the master copy.  This provides an efficient way to purge large
    1.98 +directory hierarchies, even unwillingly in case that a wrong
    1.99 +destination is given!
   1.100 +
   1.101 +2a) This will invoke a safe dry-run of clean-sweep mirroring:
   1.102 +
   1.103 +  $PRG -dn /foo/bar
   1.104 +
   1.105 +where additions and deletions will be printed without any actual
   1.106 +changes performed so far.
   1.107 +
   1.108 +2b) Exact mirroring with actual deletion of garbage may be performed
   1.109 +like this:
   1.110 +
   1.111 +  $PRG -d /foo/bar
   1.112 +
   1.113 +
   1.114 +After gaining some confidence in the workings of rsync-isabelle one
   1.115 +would usually set up some automatic mirror scheme, e.g. a daily cron
   1.116 +job run by the 'nobody' user.
   1.117 +
   1.118 +Add -w to the option list in order to mirror the whole Isabelle website
   1.119 +
   1.120 +EOF
   1.121 +  exit 0
   1.122 +fi
   1.123 +
   1.124 +
   1.125 +# arguments
   1.126 +
   1.127 +[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
   1.128 +
   1.129 +DEST="$1"; shift;
   1.130 +
   1.131 +
   1.132 +## main
   1.133 +
   1.134 +exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."