haftmann@17671: #!/usr/bin/env bash
haftmann@17671: #
haftmann@17671: # $Id$
haftmann@17671: #
haftmann@17671: # mirror script for Isabelle distribution or website
haftmann@17671: 
haftmann@17671: 
haftmann@17671: ## diagnostics
haftmann@17671: 
haftmann@17671: PRG=`basename "$0"`
haftmann@17671: 
haftmann@17671: usage()
haftmann@17671: {
haftmann@17671:   echo
haftmann@17671:   echo "Usage: $PRG [OPTIONS] DEST"
haftmann@17671:   echo
haftmann@17671:   echo "  Options are:"
haftmann@17671:   echo "    -h    print help message"
haftmann@17671:   echo "    -n    dry run, don't do anything, just report what would happen"
haftmann@17671:   echo "    -w    mirror whole Isabelle website"
haftmann@17671:   echo "    -d    delete files that are not on the server (BEWARE!)"
haftmann@17671:   echo
haftmann@17671:   exit 1
haftmann@17671: }
haftmann@17671: 
haftmann@17671: fail()
haftmann@17671: {
haftmann@17671:   echo "$1" >&2
haftmann@17671:   exit 2
haftmann@17671: }
haftmann@17671: 
haftmann@17671: 
haftmann@17671: ## process command line
haftmann@17671: 
haftmann@17671: # options
haftmann@17671: 
haftmann@17671: HELP=""
haftmann@17671: ARGS=""
haftmann@17671: SRC="isabelle-distribution"
haftmann@17671: 
haftmann@17671: while getopts "hnwd" OPT
haftmann@17671: do
haftmann@17671:   case "$OPT" in
haftmann@17671:     h)
haftmann@17671:       HELP=true
haftmann@17671:       ;;
haftmann@17671:     n)
haftmann@17671:       ARGS="$ARGS -n"
haftmann@17671:       ;;
haftmann@17671:     w)
haftmann@17671:       SRC="isabelle-website"
haftmann@17671:       ;;
haftmann@17671:     d)
haftmann@17671:       ARGS="$ARGS --delete"
haftmann@17671:       ;;
haftmann@17671:     \?)
haftmann@17671:       usage
haftmann@17671:       ;;
haftmann@17671:   esac
haftmann@17671: done
haftmann@17671: 
haftmann@17671: shift `expr $OPTIND - 1`
haftmann@17671: 
haftmann@17671: 
haftmann@17671: # help
haftmann@17671: 
haftmann@17671: if [ -n "$HELP" ]; then
haftmann@17671:   cat <<EOF
haftmann@17671: 
haftmann@17671: Mirroring the Isabelle distribution or website
haftmann@17671: ==============================================
haftmann@17671: 
haftmann@17671: The Munich site maintains an rsync server for the Isabelle
haftmann@17671: distribution or website.
haftmann@17671: 
haftmann@17671: The rsync tool is very smart and efficient in mirroring large
haftmann@17671: directory hierarchies.  See http://rsync.samba.org/ for more
haftmann@17671: information.  The rsync-isabelle script provides a simple front-end
haftmann@17671: for easy access to the Isabelle distribution.
haftmann@17671: 
haftmann@17671: The script can be either run in conservative or clean-sweep mode.
haftmann@17671: 
haftmann@17671: 1) Basic mirroring works like this:
haftmann@17671: 
haftmann@17671:   $PRG /foo/bar
haftmann@17671: 
haftmann@17671: where /foo/bar refers to your local copy of the Isabelle distribution
haftmann@17671: (the base directory has to exist already).  This operation is
haftmann@17671: conservative in the sense that files are never deleted, thus garbage
haftmann@17671: may accumulate over time as our master copy is changed.
haftmann@17671: 
haftmann@17671: Avoiding garbage in your local copy requires some care.  Rsync
haftmann@17671: provides a way to delete all additional local files that are absent in
haftmann@17671: the master copy.  This provides an efficient way to purge large
haftmann@17671: directory hierarchies, even unwillingly in case that a wrong
haftmann@17671: destination is given!
haftmann@17671: 
haftmann@17671: 2a) This will invoke a safe dry-run of clean-sweep mirroring:
haftmann@17671: 
haftmann@17671:   $PRG -dn /foo/bar
haftmann@17671: 
haftmann@17671: where additions and deletions will be printed without any actual
haftmann@17671: changes performed so far.
haftmann@17671: 
haftmann@17671: 2b) Exact mirroring with actual deletion of garbage may be performed
haftmann@17671: like this:
haftmann@17671: 
haftmann@17671:   $PRG -d /foo/bar
haftmann@17671: 
haftmann@17671: 
haftmann@17671: After gaining some confidence in the workings of rsync-isabelle one
haftmann@17671: would usually set up some automatic mirror scheme, e.g. a daily cron
haftmann@17671: job run by the 'nobody' user.
haftmann@17671: 
haftmann@17671: Add -w to the option list in order to mirror the whole Isabelle website
haftmann@17671: 
haftmann@17671: EOF
haftmann@17671:   exit 0
haftmann@17671: fi
haftmann@17671: 
haftmann@17671: 
haftmann@17671: # arguments
haftmann@17671: 
haftmann@17671: [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
haftmann@17671: 
haftmann@17671: DEST="$1"; shift;
haftmann@17671: 
haftmann@17671: 
haftmann@17671: ## main
haftmann@17671: 
haftmann@17671: exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."