Admin/lib/Tools/components_checksum

tuned proofs;

#!/usr/bin/env bash
#
# Author: Alexander Krauss
#
# DESCRIPTION: compute and validate checksums for component repository


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [DIR]"
  echo
  echo "  Options are:"
  echo "    -u           update the recorded checksums in the repository"
  echo "    -c           compare the actual checksums with the recorded ones"
  echo
  echo "  Compute the checksums of component .tar.gz archives in DIR"
  echo "  (default \"/home/isabelle/components\") and synchronize them"
  echo "  with the Isabelle repository."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

UPDATE=""
CHECK=""
COMPONENTS_DIR="/home/isabelle/components"

while getopts "uc" OPT
do
  case "$OPT" in
    u)
      UPDATE=true
      ;;
    c)
      CHECK=true
      ;;
  esac
done

shift $(($OPTIND - 1))

[ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage


# args

[ "$#" -ge 1 ] && { COMPONENTS_DIR="$1"; shift; }
[ "$#" -ne 0 ] && usage


## compute checksums

CHECKSUM_DIR="$ISABELLE_HOME/Admin/components"
CHECKSUM_FILE="$CHECKSUM_DIR/components.sha1"
CHECKSUM_TMP="$CHECKSUM_DIR/components.sha1.tmp"

(
  cd "$COMPONENTS_DIR"
  sha1sum *.tar.gz | sort -k2 -f > "$CHECKSUM_TMP"
)

[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
[ -n "$CHECK" ] && {
  diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error"
}