1#!/usr/bin/env bash 2# 3# Author: Sascha Boehme 4# 5# DESCRIPTION: testing tool for automated proof tools 6 7 8PRG="$(basename "$0")" 9 10function print_action_names() 11{ 12 for TOOL in "$MIRABELLE_HOME/Tools"/mirabelle_*.ML 13 do 14 echo "$TOOL" | perl -w -p -e 's/.*mirabelle_(.*)\.ML/ $1/' 15 done 16} 17 18function print_sledgehammer_options() { 19 grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \ 20 perl -w -p -e 's/val .*K *= *"(.*)" *\(\*(.*)\*\)/ $1$2/' 21} 22 23function usage() { 24 [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None" 25 timeout="$MIRABELLE_TIMEOUT" 26 echo 27 echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES" 28 echo 29 echo " Options are:" 30 echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" 31 echo " -O DIR output directory for test data (default $out)" 32 echo " -S FILE user-provided setup file (no actions required)" 33 echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" 34 echo " -d DIR include session directory" 35 echo " -q be quiet (suppress output of Isabelle process)" 36 echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" 37 echo 38 echo " Apply the given actions (i.e., automated proof tools)" 39 echo " at all proof steps in the given theory files." 40 echo 41 echo " ACTIONS is a colon-separated list of actions, where each action is" 42 echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:" 43 print_action_names 44 echo 45 echo " Available OPTIONs for the ACTION sledgehammer:" 46 print_sledgehammer_options 47 echo 48 echo " FILES is a list of theory files, where each file is either NAME.thy" 49 echo " or NAME.thy[START:END] and START and END are numbers indicating the" 50 echo " range the given actions are to be applied." 51 echo 52 exit 1 53} 54 55function fail() 56{ 57 echo "$1" >&2 58 exit 2 59} 60 61 62## process command line 63 64# options 65 66[ $# -eq 0 ] && usage 67 68MIRABELLE_DIR= 69MIRABELLE_SETUP_FILE= 70 71while getopts "L:T:O:d:t:S:q?" OPT 72do 73 case "$OPT" in 74 L) 75 MIRABELLE_LOGIC="$OPTARG" 76 ;; 77 T) 78 MIRABELLE_THEORY="$OPTARG" 79 ;; 80 O) 81 MIRABELLE_OUTPUT_PATH="$OPTARG" 82 ;; 83 d) 84 MIRABELLE_DIR="$OPTARG" 85 ;; 86 t) 87 MIRABELLE_TIMEOUT="$OPTARG" 88 ;; 89 S) 90 MIRABELLE_SETUP_FILE="$OPTARG" 91 ;; 92 q) 93 MIRABELLE_QUIET="true" 94 ;; 95 \?) 96 usage 97 ;; 98 esac 99done 100 101export MIRABELLE_DIR 102export MIRABELLE_SETUP_FILE 103export MIRABELLE_QUIET 104 105shift $(($OPTIND - 1)) 106 107export MIRABELLE_ACTIONS="$1" 108 109shift 110 111 112# setup 113 114if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then 115 MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$" 116 PURGE_OUTPUT="true" 117fi 118 119mkdir -p "$MIRABELLE_OUTPUT_PATH" 120 121export MIRABELLE_OUTPUT_PATH 122 123 124## main 125 126for FILE in "$@" 127do 128 perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." 129done 130 131 132## cleanup 133 134if [ -n "$PURGE_OUTPUT" ]; then 135 rm -rf "$MIRABELLE_OUTPUT_PATH" 136fi 137