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