Admin/rsync-isabelle

Reorganized, moving many results about the integer dvd relation from IntPrimes
to main HOL (IntDiv)

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