proveit.in

#!/bin/sh
#
# proveit.in
# Release: ProofLite-7.1.0 (11/06/20)
#
# Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
# NASA Langley Research Center
# http://shemesh.larc.nasa.gov/people/cam/ProofLite
#
# Copyright (c) 2011-2012 United States Government as represented by
# the National Aeronautics and Space Administration.  No copyright
# is claimed in the United States under Title 17, U.S.Code. All Other
# Rights Reserved.
#
# Mariano Moscato (04/26/2021)
# National Institute of Aerospace
#
# Script for batch proving in PVS 
#  

PVSPATH=@PVSPATH@

#-------------------------------------------------
# Nothing below this line should need modification
#

readVersion() {
    if ! type "$PVSPATH/pvs" > /dev/null 2>&1  || ! VERSION=$($PVSPATH/pvs -raw -E '(format t "~&~%PVSIOVERSION ~a~%~%" *prooflite-version*)(bye)' 2> /dev/null | grep PVSIOVERSION | sed 's/^.*PVSIOVERSION \(.*\)$/\1/g') ; then
	printf "PVS could not be located. Please double check PVS installation.\n"
	exit 1;
    fi
}


EXT=.summary # Extension for proof status summary file

PVSBIN=pvsbin # PVS directory of binary files
LISPFORCE=t
LISPIMPORT=nil
LISPSCRIPTS=t
LISPWRITESCRIPTS=nil
LISPAUTOTOP=nil
LISPTRACES=nil
LISPTXTPROOFS=nil
LISPTEXPROOFS=nil
LISPTYPECHECK=nil
LISPDEPENDENCIES=nil
LISPAUTOFIX=nil
LISPRETRYWITHTCCS=nil
PVSTIMEOUT=
LISPDEFAULTPROOFSCRIPT=nil
PRELUDEXT=
DISABLE=
ENABLE=
CLEAN=
LOG=
QUIET=
DEBUG=
OUTDIR=
TOP=top
NOFILE=yes
BINARIESONLY=t

reset_vars() {
  FILENOTFOUND=
  ARG=
  OPTS=  
  OUTFILE=
  LOGFILE=
  PVSCONTEXT=
  PVSFILE=
  THFS=
  THEORIES=  
  LISPDEPENDENCIES=nil
  LISPAUTOFIX=nil
  LISPRETRYWITHTCCS=nil
  PVSTIMEOUT=
  LISPDEFAULTPROOFSCRIPT=nil
}

all_opt() {
  if [ -z "$FILENOTFOUND" ]; then
    QUIET=yes
    if [ -z "$CLEAN" ]; then
	CLEAN=yes
    fi
    if [ "$CLEAN" = "only" ]; then
	QUIET=
    fi
    LISPIMPORT=t
    LISPSCRIPTS=nil
    LISPDEPENDENCIES=relative
  fi
}


# $ARG has the general form
# <dir> | <file>[.pvs] | [<dir>@]<thf1>,..,<thfn>, where 
# <thfi> has the form <th>[.<f1>:..:<fm>]

compile_infile_name() {
  # If <dir>, set context to <dir> and pvsfile to top.pvs
  if [ -d $ARG ]; then
    PVSCONTEXT=$ARG
    if [ -z "$OUTFILE" ]; then
	OUTFILE=$ARG$EXT
    fi
    PVSFILE=`basename $TOP .pvs`
    if [ -f $PVSCONTEXT/$PVSFILE.pvs -o "$LISPAUTOTOP" = "t" ]; then
	all_opt
    else
	FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
    fi
    LISPDEPENDENCIES=relative
  # If  <file>, set context to its dirname and pvsfile to its base name
  else
    PVSCONTEXT=$(cd "$(dirname $ARG)"; pwd -P)
    PVSFILE=`basename $ARG .pvs`
    if [ ! -f $PVSCONTEXT/$PVSFILE.pvs ]; then
	case $ARG in
	    *@*) predir=`echo $ARG | sed -e "s/\([^@]*\)@.*/\1/"`
		THFS=`echo $ARG | sed -e "s/[^@]*@//"`
		if [ -z "$predir" ]; then
		    PVSCONTEXT=$(pwd -P)
		else 
		    if [ -d "$predir" ]; then
			PVSCONTEXT=$predir
		    else
			echo "Error: $predir is not a directory"
			exit 1
		    fi
		fi
		if [ "$THFS" ]; then
		    PVSFILE=$THFS
		    THEORIES=`echo $THFS | sed -e "s/\..*,/,/g" -e "s/\..*//"`
		else
		    echo "Error: At least one theory has to be specified in $ARG"
		    exit 1
		fi;;
	    *)  FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
		if [ -z "$NOFILE" -a "$LISPAUTOTOP" != "t" ]; then
		    echo "Error: File $FILENOTFOUND not found"
		    exit 1;
		fi;;
	esac
    fi
  fi
}

strip_ext() {
  echo "$1" | sed -e "s/\(.*\)\..*/\1/g" 
}

# If necessary, set the name of the output file
#
compile_outfile_names() {
    dir=$OUTDIR
    if [ -z "$OUTFILE" ]; then
	if [ -z "$dir" ]; then
	    dir=$PVSCONTEXT
	fi
	OUTFILE=$PVSFILE$EXT
    else 
      if [ -z "$dir" ]; then
        dir=`dirname $OUTFILE`
      fi
    fi
    base=`basename $OUTFILE`
    BASEOUT=`strip_ext $base`
    if [ "$BASEOUT" = $base ]; then
      base=$BASEOUT$EXT
    fi
    if [ "$dir" ]; then
	OUTFILE=$dir/$base
	LOGFILE=$dir/$BASEOUT.log
    fi
    if [ "$LISPTYPECHECK" = "t" ]; then 
	OUTFILE=$OUTFILE-tc
    fi
}

# Translate a list l1,...,ln into (l1 .. ln)
list_to_lisp() {
  if [ -z "$1" ]
  then 
      echo nil
  else
      echo "(\"$1\")" | sed -e "s/,/\" \"/g"
  fi
}

# append e l = e,le. Check for the special case when l is empty
append() {
    if [ -z "$2" ]; then
	echo "$1"
    else
	echo "$2,$1"
    fi
}

# Take care of the optional cleaning
#
cleanup() {
  if [ "$CLEAN" ]
  then
      if [ "$PVSCONTEXT" ]; then
	  if [ "$BINARIESONLY" ]; then
	      PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.bin"
	  else
	      PVSCONTEXT_CTXT="$PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.*"
	  fi
      fi   
      if [ "$LOGFILE" ]; then
	  LOGFILE_RELATIVE_PATH="$LOGFILE"
      fi
      if [ "$OUTFILE" ]; then
	  OUTFILE_RELATIVE_PATH="$OUTFILE"
      fi
      if [ -z "$QUIET" ]
      then
	  echo "Removing $PVSCONTEXT_CTXT $OUTFILE_RELATIVE_PATH $LOGFILE_RELATIVE_PATH"
      fi
      rm -f $PVSCONTEXT_CTXT $OUTFILE_RELATIVE_PATH $LOGFILE_RELATIVE_PATH
  fi
}

# Help print command
#
usage() {
    readVersion
    
    echo "NAME
  proveit $VERSION -- runs PVS in batch mode

SYNOPSIS

  proveit <option> ... <file>[.pvs] | [<ctxt>]@<thf1>,..,<thfn> ... | <dir>
     where <thfi> has the form  <th>[.<f1>:..:<fm>]

DESCRIPTION
  Prove all theories in the input files, e.g.,
 
  \$ proveit <dir>
     Prove all theories imported in <dir>/top.pvs

  \$ proveit <file>.pvs
     Prove all theories in <file>.pvs

  \$ proveit -a <file>.pvs
     Prove all theries in <file>.pvs and their dependencies

ADVANCED USE
  In the more general form, a context, a list of theories, and a list of 
  formulas are specified using the syntax <[ctxt]@thf1,..,thfn>,  where <ctxt> 
  is a directory and each <thfi> has the form <th[.f1:..:fm]> with <th> being a 
  theory and <f1:..:fn> a list of formulas in <th>. Only formulas specified
  this way are proven by PVS. In this case, the proof status is saved
  in <th.f1:..:fm>.summary in <ctxt>. For example, to prove formulas <f1> and 
  <f2> in theory <theory> in the current context, type: 
  \$proveit @<theory>.<f1>:<f2>

  Note that, when the target is a directory (as in the first example in the 
  Description section), all the files in its pvsbin subfolder are overwritten.

OPTIONS
  Options are processed in the order they appear. One letter options can be 
  combined.

   -a|--all            equivalent to -ciq 
   --auto-fix [<num>]  try sibling proofs on unfinished branchs (<num> is the maximum 
                       acceptable distance between the current branch and the sibling 
                       which proof is to be tried; default value is 2)
   -c|--clean          remove .pvscontext and binary files in the pvsbin folder before proving
   -C|--clean-only     just remove .pvscontext and binary files in the pvsbin folder 
                       (do not typecheck nor prove)
   --clean-all         just remove .pvscontext and all files in the pvsbin folder 
                       (do not typecheck nor prove)
   -d|--dir <dir>      use <dir> as default directory of summary files
   --dependencies [relative|fullpath]  compute theory dependencies and save them in 
                       pvsbin/<file>.dep. 
   --default-script <proof script> default prooflite script to be tried on unfinished branches
   --disable <o1,..,on> disable external oracles o1,...,on
   --disable-oracles   disable any external oracle
   --enable <o1,..,on> enable external oracles o1,..,on. Overwrite --disable
   .<ext>              use <ext> as default extension of summary files
   -f|--force          force proof reruns (default)
   ~f|--no-force       don't force proof reruns 
   -h|--help           print this message
   -i|--importchain    prove chain of imported theories (set --no-scripts)
   ~i|--no-importchain don't prove chain of imported theories (default)
   --lisp <lisp>       specify lisp version; <lisp> is one of allegro,cmulisp
   -l|--log            log all information generated by PVS in <outfile>.log
   ~l|--no-log         don't log PVS information (default)
   -o|--out <outfile>  save the proof status summary in <outfile>.
   -p|--prelude-ext <p1,..,pn> load prelude extensions p1,..,pn 
   ~p|--no-prelude-ext don't load any prelude extension
   -q|--quiet          print only untried and unfinished proofs per theory, and grand total  
   -s|--scripts        install ProofLite scripts (default)
   ~s|--no-scripts     don't install ProofLite scripts
   --tex               generate LaTeX proof files in directory pvstex
   --no-tex            don't generate LaTeX proof files (default)
   --txt               generate text proof files in directory pvstxt
   --no-txt            don't generate text proof files (default)
   -t|--top <topfile>  use <topfile>.pvs instead of top.pvs when the input is a directory
   --generate-top      generate top file if it does not exist
   --timeout <secs>    timeout in seconds for each proof
   --traces            include proof traces in log file
   --no-traces         don't include proof traces in log file (default)
   -T|--typecheck-only typecheck but do not prove the theory
   -v|--verbose        print proof status information per theory and grand total (default)
   --version           print version information and exit
   -w|--write-scripts  write proofs as prooflite scripts into separate files (disabled by default,
                       this option is omitted in typecheck-only mode.)

SEE ALSO
  provethem -- for iterating proveit on a list of directories
"
}

# Print error output
error_output() {
    sed -i.bak -n -e '/^<pvserror/,/^<\/pvserror/p' \
	-e '/^Restored .*/d' \
	-e '/^\*\*\* /p' \
	-e '/^Error/p' \
	-e '/^Typechecking/ !{
                 /^Typecheck error/ {
                   p;g;p
                 }
                 /^Typecheck error/! {
                   /^PVS file .* is not/h
                   /^PVS file .* is not/!H
                 }
              }' \
	-e '/^Typechecking/h' \
	-e '/Proof summary/,/Grand Totals/p' $OUTFILE 
    if [ -z "$QUIET" ]; then
	cat $OUTFILE | \
	    sed -e "s+^<pvserror msg=\"\(.*\)\">+Error: \1 ($ARG) +" \
            -e 's/"//g' -e 's/<\/pvserror>//g' \
	    -e 's/^Error/*** Error/gp'\
	    -e 's/^\*\*\* Warning/*** Warning/gp'\
	    -e '/^\*\*\*.*/d' 
    else
	cat $OUTFILE | \
	    sed -n -e "s+^<pvserror msg=\"\(.*\)\">\"\(.*\)\"<\/pvserror>+Error: \1 ($ARG) \2 +p" \
		-e 's/^Error/*** Error/gp'\
		-e 's/^\*\*\* Warning/*** Warning/gp'\
		-e "/^Typecheck error/p" \
		-e '/Proof summary/h'\
               -e '/Proof summary/ !{
                    /unfinished/H
                    /unchecked/H
                    /untried/H
                   }'\
               -e '/Theory totals/ {
                   H;g
                   /\.\.\.\./p
                  }'\
               -e '/^Grand Totals:/p'
    fi
    cat $OUTFILE.bak | sed  -n \
			    -e 's/^Typechecking/*** Error occurred while typechecking/p' \
			    -e 's/^Proving/*** Error occurred while proving/p' \
			    -e 's/^Rerunning proof/*** Error occurred while rerunning proof/p' \
	| tail -1
    if [ "$LOG" ]; then
	mv -f $OUTFILE.bak $LOGFILE
    else
	rm $OUTFILE.bak
    fi
}

# Pretty print PVS output
pvs_output() {
    sed -i.bak -n -e '/File .*\.pvs typechecked/p'\
        -e '/^\*\*\* /p'\
	-e '/^Error/p'\
        -e '/Proof summary/,/Grand Totals/p' $OUTFILE
    cat $OUTFILE | quiet_output
    if [ "$LOG" ]; then
	mv -f $OUTFILE.bak $LOGFILE
    else
	rm $OUTFILE.bak
    fi
}

# quiet output
quiet_output() {
    if [ -z "$QUIET" ] || [ "$LISPTYPECHECK" = "t" ]
    then
	sed -n -e '/File/p'\
	       -e '/Warning/p'\
	       -e '/Error/p'\
               -e '/Proof summary/h'\
               -e '/Proof summary/ !{
                    /unfinished/H
                    /unchecked/H
                    /untried/H
                   }'\
               -e '/Theory totals/ { 
                    i\

                    x;p;g;p
                  }' \
               -e '/^Grand Totals:/ {
                    i\

                    p
                  }'
    else
	sed -n -e '/Proof summary/h'\
	       -e '/Warning/p'\
	       -e '/Error/p'\
               -e '/Proof summary/ !{
                    /unfinished/H
                    /unchecked/H
                    /untried/H
                   }'\
               -e '/Theory totals/ {
                   H;g
                   /\.\.\.\./p
                  }'\
               -e '/^Grand Totals:/p' 
    fi
}

process_opts() {
  while [ $# -gt 0 ]
  do
    case $1 in
	-a|all|--all)  
	    all_opt;;
	-c|-clean|--clean)
	    CLEAN=yes;;
        ~c|-no-clean|--no-clean)
	    CLEAN=;;
	-f|-force|--force)   
	    LISPFORCE=t;;
	~f|-no-force|--no-force)   
	    LISPFORCE=nil;;
	-i|-importchain|--importchain) 
	    LISPSCRIPTS=nil
	    LISPIMPORT=t;;
        ~i|-no-importchain|--no-importchain)
	    LISPIMPORT=nil;;
	-w|-write-scripts|--write-scripts)
	    LISPWRITESCRIPTS=t;;
	-s|-scripts|--scripts)
	    LISPSCRIPTS=t;;
	~s|-no-scripts|--no-scripts)
	    LISPSCRIPTS=nil;;
        -T|-Typecheck|--Typecheck|-typecheck-only|--typecheck-only)
	    LISPTYPECHECK=t;;
	-traces|--traces) 
	    LOG=yes
	    LISPTRACES=t;;
	-no-traces|--no-traces) 
	    LISPTRACES=nil;;
	-txt|--txt)
	    LISPTXTPROOFS=t;;
	-no-txt|--no-txt)
	    LISPTXTPROOFS=nil;;
	-tex|--tex)
	    LISPTEXPROOFS=t;;
	-no-tex|--no-tex)
	    LISPTEXPROOFS=nil;;
	-l|-log|--log)
	    LOG=yes;;
	~l|-no-log|--no-log)
	    LOG=;;
	~p|-no-prelude-ext|--no-prelude-ext)
	    PRELUDEXT=;;
	-q|-quiet|--quiet)
	    QUIET=yes;;
	-v|-verbose|--verbose)
	    QUIET=;;
	--*)           
	    echo "Error: $1 is not a valid option"
	    exit 1;;
	-*)
	    opts=`echo "$1" | sed -e s/-//g -e "s/\(.\)/\1 /g"`
	    for opt in $opts; do
	      case $opt in
		  a)     
		      all_opt;;
		  c)   
		      CLEAN=yes;;
		  C)
		      QUIET=
		      BINARIESONLY=t
		      CLEAN=only;;
		  f)   
		      LISPFORCE=t;;
		  s)
		      LISPSCRIPTS=t;;
		  w)
		      LISPWRITESCRIPTS=t;;
		  v)  
		      QUIET=;;
		  i) 
		      LISPSCRIPTS=nil
		      LISPIMPORT=t;;
		  l)
		      LOG=yes;;
		  q)
		      QUIET=yes;;
		  T)
		      LISPTYPECHECK=t;;
		  *) 
		      usage
		      echo "Error: -$opt is not a valid option"
		      exit 1;;
	      esac
	    done;;
	~*)
	    opts=`echo "$1" | sed -e s/~//g -e "s/\(.\)/\1 /g"`
	    for opt in $opts; do
	      case $opt in
		  c)
		      CLEAN=;;
		  f)   
		      LISPFORCE=nil;;
		  i)
		      LISPIMPORT=nil;;
		  s)
		      LISPSCRIPTS=nil;;
		  w)
		      LISPWRITESCRIPTS=nil;;
		  l) 
		      LOG=;;
		  p)  
		      PRELUDEXT=;;
		  *) 
		      usage
		      echo "Error: ~$opt is not a valid option"
		      exit 1;;
	      esac
	    done
    esac
    shift
  done
}


# Main Function
proveit() {
  compile_infile_name
  if [ "$CLEAN" = "only" ]; then
      cleanup
  else
      process_opts $OPTS
      if [ "$DEBUG" ]; then
	  QUIET=
	  LOG=y
      fi
      compile_outfile_names
      cleanup
      
      if [ "$FILENOTFOUND" -a "$LISPAUTOTOP" != "t" ]; then
	  if [ -z "$CLEAN" ]; then
	      echo "Error: File $FILENOTFOUND not found"
	  fi
	  exit 1
      fi
      
      echo Processing $ARG. Writing output to file $OUTFILE
      if [ "$LOG" ]; then
	  echo "Logging PVS information in $LOGFILE"
      fi
      if [ -z "$QUIET" ]; then
	  if [ "$PRELUDEXT" ]; then
	      echo "Loading prelude extensions: $PRELUDEXT"
	  fi
	  if [ "$DISABLE" ]; then
	      if [ "$DISABLE" = "_" ]; then
                  echo "Disabling any external oracle"
              else
 		  echo "Disabling oracles: $DISABLE"
	      fi
	  fi
	  if [ "$ENABLE" ]; then
 	      echo "Enabling oracles: $ENABLE"
	  fi
	  if [ "$LISPIMPORT" = "t" ]; then
	      echo "Proving chain of imported theories"
	  fi 
	  if [ "$LISPDEPENDENCIES" != "nil" ]; then
	      echo "Saving theory dependencies ($LISPDEPENDENCIES) in directory pvsbin"
	  fi
	  if [ "$LISPSCRIPTS" != "t" ]; then
	      echo "ProofLite scripts won't be installed"
	  fi 
	  if [ "$LISPWRITESCRIPTS" = "t" ]; then
	      echo "Proofs wish/ill be stored as ProofLite scripts in .prl files."
	  fi 
	  if [ "$LISPAUTOTOP" = "t" ]; then
	      echo "Top file will be automatically generated."
	  fi
	  if [ "$LISPFORCE" != "t" ]; then
	      echo "Proofs won't be forced"
	  fi
	  if [ "$LISPTRACES" = "t" ]; then
	      echo "Including proof traces in output file"
	  fi
	  if [ "$LISPTXTPROOFS" = "t" ]; then
	      echo "Generating text proof files in directory pvstxt"
	  fi
	  if [ "$LISPTEXPROOFS" = "t" ]; then
	      echo "Generating LaTeX proof files in directory pvstex"
	  fi
	  if [ "$LISPAUTOFIX" != "nil" ]; then
	      echo "Auto-fix enabled"
	  fi
	  if [ "$LISPRETRYWITHTCCS" != "nil" ]; then
	      echo "Retry-with-tccs enabled"
	  fi
	  if [ "$LISPDEFAULTPROOFSCRIPT" != "nil" ]; then
	      echo "Default proof script $LISPDEFAULTPROOFSCRIPT"
	  fi
	  if [ "$PVSTIMEOUT" ]; then
	      echo "Timeout set at $PVSTIMEOUT secs."
	  fi
      fi

      export PROVEITARG="$ARG"
      export PROVEITPVSCONTEXT="$PVSCONTEXT"
      if [ -f $PVSCONTEXT/$PVSFILE.pvs -o "$LISPAUTOTOP" = "t" ]; then
	  export PROVEITPVSFILE="$PVSFILE"
      else
 	  export PROVEITPVSFILE=""
      fi
      export PROVEITLISPIMPORT="$LISPIMPORT"
      export PROVEITLISPSCRIPTS="$LISPSCRIPTS"
      export PROVEITLISPWRITESCRIPTS="$LISPWRITESCRIPTS"
      export PROVEITLISPTRACES="$LISPTRACES"
      export PROVEITLISPFORCE="$LISPFORCE"
      export PROVEITLISPAUTOTOP="$LISPAUTOTOP"
      export PROVEITLISPTYPECHECK="$LISPTYPECHECK"
      export PROVEITLISPTXTPROOFS="$LISPTXTPROOFS"
      export PROVEITLISPTEXPROOFS="$LISPTEXPROOFS"
      export PROVEITLISPDEPENDENCIES="$LISPDEPENDENCIES"
      export PROVEITLISPPRELUDEXT="`list_to_lisp $PRELUDEXT`"
      export PROVEITLISPDISABLE="`list_to_lisp $DISABLE`"
      export PROVEITLISPENABLE="`list_to_lisp $ENABLE`"
      export PROVEITLISPTHFS="`list_to_lisp $THFS`"
      export PROVEITLISPTHEORIES="`list_to_lisp $THEORIES`"
      export PROVEITLISPAUTOFIX="$LISPAUTOFIX"
      export PROVEITLISPRETRYWITHTCCS="$LISPRETRYWITHTCCS"
      export PROVEITLISPDEFAULTPROOFSCRIPT="$LISPDEFAULTPROOFSCRIPT"
      
      if [ "$DEBUG" ]; then
	  readVersion
	  echo "QUIET: $QUIET"
	  echo "PROVEITVERSION: $VERSION"
	  echo "OUTFILE: $OUTFILE"
	  echo "LOGFILE: $LOGFILE"
	  echo "PROVEITARG: $PROVEITARG"
	  echo "PROVEITPVSCONTEXT: $PROVEITPVSCONTEXT"
	  echo "PROVEITPVSFILE: $PROVEITPVSFILE"
	  echo "PROVEITLISPIMPORT: $PROVEITLISPIMPORT"
	  echo "PROVEITLISPSCRIPTS: $PROVEITLISPSCRIPTS"
	  echo "PROVEITLISPWRITESCRIPTS: $PROVEITLISPWRITESCRIPTS"
	  echo "PROVEITLISPTRACES: $PROVEITLISPTRACES"
	  echo "PROVEITLISPFORCE: $PROVEITLISPFORCE" 
	  echo "PROVEITLISPAUTOTOP: $LISPAUTOTOP"
	  echo "PROVEITLISPTYPECHECK: $PROVEITLISPTYPECHECK"
	  echo "PROVEITLISPTXTPROOFS: $PROVEITLISPTXTPROOFS"
	  echo "PROVEITLISPTEXPROOFS: $PROVEITLISPTEXPROOFS"
	  echo "PROVEITLISPDEPENDENCIES: $PROVEITLISPDEPENDENCIES"
	  echo "PROVEITLISPPRELUDEXT: $PROVEITLISPPRELUDEXT"
	  echo "PROVEITLISPDISABLE: $PROVEITLISPDISABLE"
	  echo "PROVEITLISPENABLE: $PROVEITLISPENABLE"
	  echo "PROVEITLISPTHFS: $PROVEITLISPTHFS"
	  echo "PROVEITLISPTHEORIES: $PROVEITLISPTHEORIES"
	  echo "PROVEITLISPAUTOFIX: $PROVEITLISPAUTOFIX"
	  echo "PROVEITLISPRETRYWITHTCCS: $PROVEITLISPRETRYWITHTCCS"
	  echo "PROVEITLISPDEFAULTPROOFSCRIPT: $PROVEITLISPDEFAULTPROOFSCRIPT"
      fi

      if [ $PVSTIMEOUT ]; then
	  $PVSPATH/pvs -raw $PVSLISP -timeout $PVSTIMEOUT -E "(proveit)" > $OUTFILE 2>&1
	  ret_value=$?
      else
	  $PVSPATH/pvs -raw $PVSLISP -E "(proveit)" > $OUTFILE 2>&1
	  ret_value=$?
      fi

      if [ $ret_value -ne 0 ]; then
	  error_output
	  exit $ret_value 
      fi
      pvs_output
  fi
  reset_vars
  return $ret_value;
}

# ... and go!
#

ret_value=0

reset_vars
while [ $# -gt 0 ]
do
  case $1 in
    --debug)
      DEBUG=yes;;
    -h|-help|--help)    
	  usage
	  exit 0;;
    -version|--version)
	  readVersion
	  echo $VERSION
	  exit 0;;
    .*) 
      EXT=$1;;
    -lisp|--lisp)    
	  case $2 in
	      allegro) 
		  LISP='allegro';;
	      cmulisp) 
		  LISP='cmulisp'
		  PVSBIN='PVSBIN';;
	      sbclisp)
		  LISP='sbclisp'
		  PVSBIN='PVSBIN';;
	      *) 
		  echo "Error: Only allegro, cmulisp, and sbcl are currently available"
		  exit 1;;
	  esac
	  if [ "$LISP" ]; then
	      PVSLISP="-lisp $LISP"
	  fi
	  shift;;
    -d|-dir|--dir)           
      OUTDIR=$2
      if [ ! -e "$OUTDIR" ]; then
        mkdir $OUTDIR
      fi
      if [ ! -d "$OUTDIR" ]; then
        echo "Error: $OUTDIR is not a directory"
        exit 1
      fi
	  shift;;
    -t|-top|--top)           
	  TOP=$2
	  shift;;
    -generate-top|--generate-top)           
	  LISPAUTOTOP=t;;
    -Clean|--Clean)
	echo "The option $1 is not longer supported. Please use --clean-all instead."
	exit 1;;
    -C|-clean-only|--clean-only)
	QUIET=
	BINARIESONLY=t
	CLEAN=only;;
    -clean-all|--clean-all)
	QUIET=
	BINARIESONLY=
	CLEAN=only;;
    -o|-out|--out)           
	  if [ -d "$2" ]; then
	      echo "Error: $2 is a directory"
	      exit 1
          else
 	      OUTFILE=$2
	  fi
	  shift;;
    -p|-prelude-ext|--prelude-ext) 
	  PRELUDEXT=`append $2 $PRELUDEXT`
	  shift;;
    -disable|--disable) 
	  DISABLE=`append $2 $DISABLE`
	  shift;;
    -disable-oracles|--disable-oracles) 
	  DISABLE="_";;
    -enable|--enable) 
	  ENABLE=`append $2 $ENABLE`
	  shift;;
    --retry-with-tccs)
	LISPRETRYWITHTCCS=t
	shift;;
    --auto-fix)
	LISPAUTOFIX=2
	if echo $2 | grep -qE '^[+-]?[0-9]+$'; then
	    LISPAUTOFIX=$2
	    shift
	fi;;
    -dep|--dep|-dependencies|--dependencies)
	if echo $2 | grep -qE '^-.*$'; then
	    # 'relative' by default
	    LISPDEPENDENCIES=relative
	elif echo $2 | grep -qE '^relative$'; then
	    LISPDEPENDENCIES=relative
	    shift
	elif echo $2 | grep -qE '^fullpath$'; then
	    LISPDEPENDENCIES=fullpath
	    shift
	else
	    echo "Error: --dependencies option must be followed by the options 'relative' or 'fullpath'. (See proveit --help for details.)"
	    exit 1
	fi;;
    --timeout)
	if echo $2 | grep -qE '^[0-9]+$'; then
	    PVSTIMEOUT=$2
	    shift
	else
	    echo "Error: --timeout option must be followed by the limit in seconds. (See proveit --help for details.)"
	    exit 1
	fi;;
    --default-script)
	if echo $2 | grep -qE '\(.*\)'; then
	    LISPDEFAULTPROOFSCRIPT=$2
	    shift
	else
	    echo "Error: $2 does not seem to be a proof script."
	    exit 1
	fi;;
    -*|~*) OPTS="$OPTS $1";;
    *)     ARG=$1
 	   NOFILE=
           proveit
	   ret_value=$?
  esac
  shift 
done 
if [ "$NOFILE" ]; then
  ARG=$TOP.pvs
  if [ -f $ARG -o "$CLEAN" = "only" ]; then
      proveit
      ret_value=$?
  else
      echo "[proveit] no file '$NOFILE'"
      usage
  fi
fi

exit $ret_value;