--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Sep 02 16:23:53 2009 +0200
@@ -0,0 +1,88 @@
+#!/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
+