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