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