src/HOL/Mirabelle/lib/Tools/mirabelle

Mirabelle now gives usage info when no arguments given

#!/usr/bin/env bash
#
# Author: Sascha Boehme
#
# DESCRIPTION: testing tool for automated proof tools


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

function print_action_names() {
  ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
  for ACTION in $ACTIONS
  do
    echo $ACTION | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
  done
}

function usage() {
  [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
  timeout="$MIRABELLE_TIMEOUT"
  echo
  echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
  echo
  echo "  Options are:"
  echo "    -L LOGIC     parent logic to use (default $MIRABELLE_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 "    -q           be quiet (suppress output of Isabelle process)"
  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[OPTION,...,OPTION]. Available actions are:"
  print_action_names
  echo
  echo "  Available OPTIONs for the ACTION sledgehammer:"
  echo "    * prover=NAME: name of the external prover to call"
  echo "    * prover_timeout=TIME: timeout for invoked ATP (seconds of process time)"
  echo "    * prover_hard_timeout=TIME: timeout for invoked ATP (seconds of elapsed"
  echo "      time)"
  echo "    * keep=PATH: path where to keep temporary files created by sledgehammer"
  echo "    * full_types: enable fully-typed encoding"
  echo "    * minimize: enable minimization of theorem set found by sledgehammer"
  echo "    * minimize_timeout=TIME: timeout for each minimization step (seconds of"
  echo "      process time)"
  echo "    * metis: apply metis to the theorems found by sledgehammer"
  echo "    * metis_ft: apply metis with fully-typed encoding to the theorems found"
  echo "      by sledgehammer"
  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
}

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


## process command line

# options

[ $# -eq 0 ] && usage

while getopts "L:T:O:t:q?" OPT
do
  case "$OPT" in
    L)
      MIRABELLE_LOGIC="$OPTARG"
      ;;
    T)
      MIRABELLE_THEORY="$OPTARG"
      ;;
    O)
      MIRABELLE_OUTPUT_PATH="$OPTARG"
      ;;
    t)
      MIRABELLE_TIMEOUT="$OPTARG"
      ;;
    q)
      MIRABELLE_QUIET="true"
      ;;
    \?)
      usage
      ;;
  esac
done

export MIRABELLE_QUIET

shift $(($OPTIND - 1))

export MIRABELLE_ACTIONS="$1"

shift


# setup

if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
  MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
  PURGE_OUTPUT="true"
fi

mkdir -p "$MIRABELLE_OUTPUT_PATH"

export MIRABELLE_OUTPUT_PATH

## main

for FILE in "$@"
do
  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
done


## cleanup

if [ -n "$PURGE_OUTPUT" ]; then
  rm -rf "$MIRABELLE_OUTPUT_PATH"
fi