Admin/Release/isasync
changeset 48190 76b6207eb000
parent 36859 51af1657263b
equal deleted inserted replaced
48189:cd0a411b7fc1 48190:76b6207eb000
       
     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/"