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