Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: List_Cpo.thy Sprache: Isabelle

Original von: Isabelle^©

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

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

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

function print_sledgehammer_options() {
  grep -e "^val .*K =" "$MIRABELLE_HOME/Tools/mirabelle_sledgehammer.ML" | \
  perl -w -p -e 's/val .*K *= *"(.*)" *$\*(.*)\*$/    $1$2/'
}

function usage() {
  # Do not forget to update the Sledgehammer documentation to reflect changes here.
  [ -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 "    -O DIR       output directory for test data (default $out)"
  echo "    -S FILE      user-provided setup file (no actions required)"
  echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
  echo "    -d DIR       include session directory"
  echo "    -q           be quiet (suppress output of Isabelle process)"
  echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
  echo
  echo "  Apply the given actions 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:"
  print_sledgehammer_options
  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

MIRABELLE_DIR=
MIRABELLE_SETUP_FILE=

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

export MIRABELLE_DIR
export MIRABELLE_SETUP_FILE
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

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.