#!/usr/bin/env bash
#
# Author: Florian Haftmann
# Author: Tjark Weber
#
# DESCRIPTION: download Isabelle components
shopt -s -o errexit
shopt -s -o nounset
## directory layout
: ${TMPDIR:="/tmp"}
LOCAL="${ISABELLE_HOME_USER}/contrib"
REMOTE="http://isabelle.in.tum.de/components"
## diagnostics
PRG="$(basename "$0")"
trap 'echo "Error in ${PRG}" >&2' ERR
function usage()
{
cat <<EOF
Usage: ${PRG} [OPTIONS] [COMPONENTS ...]
Options are:
-c Download current components (as listed in Admin/components).
-q Quiet (do not output diagnostic messages).
-r Replace components already present (default is to skip).
-x Exit on failed download (default is to ignore).
Download and unpack Isabelle components from central component store
(${REMOTE}/).
EOF
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
DOWNLOAD_CURRENT=""
ECHO="echo"
REPLACE_EXISTING=""
EXIT_ON_FAILED_DOWNLOAD=""
function getoptions()
{
OPTIND=1
while getopts "cqrx" OPT
do
case "$OPT" in
c)
DOWNLOAD_CURRENT=true
;;
q)
ECHO=":"
;;
r)
REPLACE_EXISTING=true
;;
x)
EXIT_ON_FAILED_DOWNLOAD=true
;;
\?)
usage
;;
esac
done
}
getoptions "$@"
shift $(($OPTIND - 1))
## download (and unpack) components
function download()
{
if [ -e "${LOCAL}/${COMPONENT}" -a -z "${REPLACE_EXISTING}" ]; then
"${ECHO}" "Skipping existing component ${COMPONENT}"
else
"${ECHO}" "${COMPONENT}"
ARCHIVE="${COMPONENT}.tar.gz"
if curl -s `"${ECHO}" --no-silent` -f -o "${TMPDIR}/${ARCHIVE}" "${REMOTE}/${ARCHIVE}"; then
if [ -n "${REPLACE_EXISTING}" ]; then
tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}" --recursive-unlink
else
tar -xzf "${TMPDIR}/${ARCHIVE}" -C "${LOCAL}"
fi
else
if [ -n "${EXIT_ON_FAILED_DOWNLOAD}" ]; then
fail "Error downloading component ${COMPONENT} (non-free?)"
else
"${ECHO}" "Error downloading component ${COMPONENT} (non-free?)"
fi
fi
fi
}
"${ECHO}" "Unpacking components into ${LOCAL}/"
mkdir -p "${LOCAL}"
# process Admin/components
if [ -n "${DOWNLOAD_CURRENT}" ]; then
while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
do
case "${REPLY}" in
\#* | "")
;;
*)
COMPONENT="$(basename "${REPLY}")"
download "${COMPONENT}"
;;
esac
done < "${ISABELLE_HOME}/Admin/components"
fi
# process args
for COMPONENT in "$@"
do
download "${COMPONENT}"
done