1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Sep 02 16:23:53 2009 +0200
     1.3 @@ -0,0 +1,88 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Author: Sascha Boehme
     1.7 +#
     1.8 +# DESCRIPTION: testing tool for automated proof tools
     1.9 +
    1.10 +
    1.11 +PRG="$(basename "$0")"
    1.12 +
    1.13 +function print_action_names() {
    1.14 +  TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
    1.15 +  for NAME in $TOOLS
    1.16 +  do
    1.17 +    echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
    1.18 +  done
    1.19 +}
    1.20 +
    1.21 +function usage() {
    1.22 +  out="$MIRABELLE_OUTPUT_PATH"
    1.23 +  timeout="$MIRABELLE_TIMEOUT"
    1.24 +  echo
    1.25 +  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
    1.26 +  echo
    1.27 +  echo "  Options are:"
    1.28 +  echo "    -L LOGIC     parent logic to use (default $ISABELLE_LOGIC)"
    1.29 +  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
    1.30 +  echo "    -O DIR       output directory for test data (default $out)"
    1.31 +  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
    1.32 +  echo
    1.33 +  echo "  Apply the given actions (i.e., automated proof tools)"
    1.34 +  echo "  at all proof steps in the given theory files."
    1.35 +  echo
    1.36 +  echo "  ACTIONS is a colon-separated list of actions, where each action is"
    1.37 +  echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
    1.38 +  print_action_names
    1.39 +  echo
    1.40 +  echo "  FILES is a list of theory files, where each file is either NAME.thy"
    1.41 +  echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
    1.42 +  echo "  range the given actions are to be applied."
    1.43 +  echo
    1.44 +  exit 1
    1.45 +}
    1.46 +
    1.47 +
    1.48 +## process command line
    1.49 +
    1.50 +# options
    1.51 +
    1.52 +while getopts "L:T:O:t:?" OPT
    1.53 +do
    1.54 +  case "$OPT" in
    1.55 +    L)
    1.56 +      MIRABELLE_LOGIC="$OPTARG"
    1.57 +      ;;
    1.58 +    T)
    1.59 +      MIRABELLE_THEORY="$OPTARG"
    1.60 +      ;;
    1.61 +    O)
    1.62 +      MIRABELLE_OUTPUT_PATH="$OPTARG"
    1.63 +      ;;
    1.64 +    t)
    1.65 +      MIRABELLE_TIMEOUT="$OPTARG"
    1.66 +      ;;
    1.67 +    \?)
    1.68 +      usage
    1.69 +      ;;
    1.70 +  esac
    1.71 +done
    1.72 +
    1.73 +shift $(($OPTIND - 1))
    1.74 +
    1.75 +ACTIONS="$1"
    1.76 +
    1.77 +shift
    1.78 +
    1.79 +
    1.80 +# setup
    1.81 +
    1.82 +mkdir -p "$MIRABELLE_OUTPUT_PATH"
    1.83 +
    1.84 +
    1.85 +## main
    1.86 +
    1.87 +for FILE in "$@"
    1.88 +do
    1.89 +  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
    1.90 +done
    1.91 +