#!/usr/bin/env bash
#
# Author: Sascha Boehme
#
# DESCRIPTION: testing tool for automated proof tools
PRG="$(basename "$0")"
function print_action_names() {
TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
for NAME in $TOOLS
do
echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/ \1/'
done
}
function usage() {
out="$MIRABELLE_OUTPUT_PATH"
timeout="$MIRABELLE_TIMEOUT"
echo
echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
echo
echo " Options are:"
echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)"
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
print_action_names
echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"
echo " range the given actions are to be applied."
echo
exit 1
}
## process command line
# options
while getopts "L:T:O:t:?" OPT
do
case "$OPT" in
L)
MIRABELLE_LOGIC="$OPTARG"
;;
T)
MIRABELLE_THEORY="$OPTARG"
;;
O)
MIRABELLE_OUTPUT_PATH="$OPTARG"
;;
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
ACTIONS="$1"
shift
# setup
mkdir -p "$MIRABELLE_OUTPUT_PATH"
## main
for FILE in "$@"
do
perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
done