proveit.in

#!/bin/sh
#
# proveit.in
# Release: ProofLite-8.0 (10/13/2023)
#
# 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 (10/13/2023)
#
# 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
}

type "$PVSPATH/pvs"  > /dev/null 2>&1
if [ $? -eq 0 ]; then
    PVSPATH=$PVSPATH/
else
    type pvs  > /dev/null 2>&1
    if [ $? -eq 0 ]; then
	PVSPATH="" # pvs is in the system path, then no path information is needed
    else
	PVSPATH=`dirname $0`
	type "$PVSPATH/pvs"  > /dev/null 2>&1
	if [ $? -eq 0 ]; then
	    PVSPATH=$PVSPATH/
	else
	    printf "Error: PVS could not be located. Add it to the system path or run install-scripts in the PVS folder.\n"
	    exit 1;
	fi
    fi
fi

PVS_RETURN_VALUE_MISSED_FORMS=142 # PVS' return value indicating missed (ie, not proved) formulas

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
LISPALTSUMMARIESMODE=nil

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
	  # if ARG contains a slash, it is replaced by '-' since PVS does not
	  # accept library names containing that symbol ('-').
	  OUTFILE=`echo $ARG | sed "s#/#-#g" `
	  OUTFILE=$OUTFILE$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
      case $ARG in
	  *@*@*)
	      echo "Error: at most one @-sign can be provided in $ARG"
	      exit 1;;
	  *@*)
	      predir=`echo $ARG | sed -e "s/\([^@]*\)@.*/\1/"`
	      THFS=`echo $ARG | sed  -e 's/,$//' -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;;
	  *)
	      PVSCONTEXT=$(cd "$(dirname $ARG)" && pwd -P)
	      PVSFILE=`basename $ARG .pvs`
	      if [ ! -f $PVSCONTEXT/$PVSFILE.pvs ]; then
		  FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
		  if [ -z "$NOFILE" ]; then
		      echo "Error: File $FILENOTFOUND not found"
		      exit 1;
		  fi
	      fi;;
      esac
  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)
   --backup-summaries  backup summary files instead of replacing them (disable by default)
   -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.)
   --summary-mode [md] alternative summary 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

      if [ $BACKUP_SUMMARIES ]; then
	  # if $OUTFILE already exists, save it as old version
	  if [ -f "$OUTFILE" ]; then
	      OUTFILEBAK=`dirname $OUTFILE`"/"`basename $OUTFILE $EXT`"."`ls -lUD "%y%m%d%H%M%S" $OUTFILE | awk '{print $6}'`$EXT
	      if [ -z "$QUIET" ]; then echo "Warning: Backing up $OUTFILE as $OUTFILEBAK"; fi
	      mv $OUTFILE $OUTFILEBAK
	  fi
	  if [ "$LOG" ] && [ -f "$LOGFILE" ]; then
	      LOGEXT=".log"
	      LOGFILEBAK=`dirname $LOGFILE`"/"`basename $LOGFILE $LOGEXT`"."`ls -lUD "%y%m%d%H%M%S" $LOGFILE | awk '{print $6}'`$LOGEXT
	      if [ -z "$QUIET" ]; then echo "Warning: Backing up $LOGFILE as $LOGFILEBAK"; fi
	      mv $LOGFILE $LOGFILEBAK
	  fi
      fi

      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 [ "$LISPALTSUMMARIESMODE" != "nil" ]; then
	      echo "Summaries will be reported in alternative format ($LISPALTSUMMARIESMODE)."
	  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 PROVEITLISPALTSUMMARIESMODE="$LISPALTSUMMARIESMODE"
      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"

      export PROVEITLISPOUTDIR=$dir
      export PROVEITLISPOUTBASENAME=$BASEOUT
      
      if [ "$DEBUG" ]; then
	  readVersion
	  export DEBUG
	  echo "QUIET=$QUIET"
	  echo "PROVEITVERSION=$VERSION"
	  echo "OUTFILE=$OUTFILE"
	  echo "LOGFILE=$LOGFILE"
	  echo "export PROVEITARG=$PROVEITARG"
	  echo "export PROVEITPVSCONTEXT=$PROVEITPVSCONTEXT"
	  echo "export PROVEITPVSFILE=$PROVEITPVSFILE"
	  echo "export PROVEITLISPIMPORT=$PROVEITLISPIMPORT"
	  echo "export PROVEITLISPSCRIPTS=$PROVEITLISPSCRIPTS"
	  echo "export PROVEITLISPWRITESCRIPTS=$PROVEITLISPWRITESCRIPTS"
	  echo "export PROVEITLISPTRACES=$PROVEITLISPTRACES"
	  echo "export PROVEITLISPFORCE=$PROVEITLISPFORCE" 
	  echo "export PROVEITLISPAUTOTOP=$LISPAUTOTOP"
	  echo "export PROVEITLISPTYPECHECK=$PROVEITLISPTYPECHECK"
	  echo "export PROVEITLISPTXTPROOFS=$PROVEITLISPTXTPROOFS"
	  echo "export PROVEITLISPTEXPROOFS=$PROVEITLISPTEXPROOFS"
	  echo "export PROVEITLISPDEPENDENCIES=$PROVEITLISPDEPENDENCIES"
	  echo "export PROVEITLISPALTSUMMARIESMODE=$PROVEITLISPALTSUMMARIESMODE"
	  echo "export PROVEITLISPPRELUDEXT=$PROVEITLISPPRELUDEXT"
	  echo "export PROVEITLISPDISABLE=$PROVEITLISPDISABLE"
	  echo "export PROVEITLISPENABLE=$PROVEITLISPENABLE"
	  echo "export PROVEITLISPTHFS=$PROVEITLISPTHFS"
	  echo "export PROVEITLISPTHEORIES=$PROVEITLISPTHEORIES"
	  echo "export PROVEITLISPAUTOFIX=$PROVEITLISPAUTOFIX"
	  echo "export PROVEITLISPRETRYWITHTCCS=$PROVEITLISPRETRYWITHTCCS"
	  echo "export PROVEITLISPDEFAULTPROOFSCRIPT=$PROVEITLISPDEFAULTPROOFSCRIPT"
      fi
      
      if [ $PVSTIMEOUT ]; then
	  TIMEOUTARG="-timeout $PVSTIMEOUT"
      else
	  TIMEOUTARG=
      fi

      if [ "$DEBUG" ]; then
	  echo "About to run: ""$PVSPATH""pvs -raw $PVSLISP $TIMEOUTARG -E \"(proveit)\" > $OUTFILE 2>&1"
      fi
      
      "$PVSPATH"pvs -raw $PVSLISP $TIMEOUTARG -E "(proveit)" > $OUTFILE 2>&1
      ret_value=$?
      
      if [ "$DEBUG" ]; then
	  echo "PVS return value: $ret_value"
      fi

      if [ $ret_value -ne 0 ] && [ $ret_value -ne $PVS_RETURN_VALUE_MISSED_FORMS ]; 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;;
    --backup-summaries)
	BACKUP_SUMMARIES=t;;
    -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;;
    --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;;
    -summary-mode|--summary-mode)
	if echo $2 | grep -qE '^md$'; then
	    LISPALTSUMMARIESMODE=md
	    shift
	else
	    echo "Error: --summary-mode option must be followed by the option 'md'. (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;