pvs.in

#!/bin/sh
# Script for starting PVS
# This script starts up Emacs, which in turn invokes the PVS lisp image.
# The image is in the main PVS directory, and is named
#   pvs-PVSLISP-PVSARCH
# where PVSLISP reflects the lisp name and version, and PVSARCH is determined
# from the system on which PVS is invoked.

# command line arguments:
#   -h | -help | --help  prints a help line and exits
#   -version | --version prints the PVS version
#   -emacs emacsref        emacs, xemacs, alias, or pathname
#   -lisp name             lisp image name - allegro, cmulisp, or sbclisp
#   -runtime               use the runtime image (devel is default, if there)
#   -decision-procedures   set the default decision procedures (ics or shostak)
#   -force-decision-procedures  forces the decision procedures to be used
#   -patchlevel    indicates the patch level: 0 for no patches
#   -batch         run in batch mode
#   -timeout       seconds to timeout commands or proofs - only allowed in batch
#   -nobg          don't run PVS in the background
#   -port number   start XML-RPC server on port number num
#   -raw           run PVS without Emacs
#   -v             the (verbose) level number - 0-3 (mostly for batch mode)
#   -q             do not load ~/.emacs, ~/.pvsemacs, or ~/.pvs.lisp files
#   -e expr        evaluate the given Emacs expression
#   -l efile       load the given Emacs file before PVS emacs files
#   -load-after efile      loads Emacs file after PVS emacs files
#   -E expr
#   -L lfile     load the given Lisp file (after PVS initializes)
#   any other emacs parameters (e.g. -u or -nw)
#   any X window parameters (e.g. -geometry 80x60+0-0)
# Other arguments will simply pass through, but they are likely not to work
# with different Emacs/Lisp combinations
#
# If the corresponding command line argument is not given, the following
# environment variables are used if set:
#   PVSLISP       - corresponds to the -lisp argument
#   PVSEMACS      - corresponds to the -emacs argument
#   PVSPATCHLEVEL - corresponds to the -patchlevel argument
#   PVSXINIT      - X window parameters; e.g., "-g '-0-0'"
#   PVSVERBOSE    - corresponds to the -v argument
#
# The following environment variables are used by PVS, and are set below:
#   PVSPATH     pvs system path - this should not normally be set by the user
#   PVSARCH	ix86 or ix86_64
#
# The PVS binary paths are appended to the front of the PATH variable
# --------------------------------------------------------------------
# PVS
# Copyright (C) 2006, SRI International.  All Rights Reserved.

# This program is free software; you can redistribute it and/or
# modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; either version 2
# of the License, or (at your option) any later version.

# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.

# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
# --------------------------------------------------------------------

# PVSPATH should be set after installation by <PVS>/bin/relocate or by hand
# to the location of the PVS installation
PVSPATH=@PVSPATH@

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


# get the command-line options
opsys=`uname -s`
flags=
batch=
rawmode=
PVSINEMACS=t
getversion=
nobg=
if [ -f $HOME/.emacs ]
  then dotemacs="-l $HOME/.emacs"
  else dotemacs=
fi
PVSXINIT=${PVSXINIT:-""}
PVSFORCEDP=nil
pvsruntime=
while [ $# -gt 0 ]
do
   case $1 in
     -emacs) PVSEMACS="$2"
             shift;;
     -lisp)
       case $2 in
	 allegro) PVSLISP=allegro;;
	 cmulisp) PVSLISP=cmulisp;;
	 sbclisp) PVSLISP=sbclisp;;
	 *) echo "Only allegro, cmulisp, and sbclisp are currently available"
	    exit 1;;
       esac
       shift;;
     -image) PVSIMAGE="$2"
	     shift;;
     -load-after) loadafter=$loadafter" -load $2"
                  shift;;
     -runtime) pvsruntime=1;;
     -port) PVSPORT=$2
        if expr $PVSPORT : '\([0-9]*\)' != $PVSPORT > /dev/null; then
	  echo "The -port must be an integer"
	  exit 1
	fi
	shift;;
     -decision-procedures)
        case $2 in
	  ics)     PVSDEFAULTDP=ics;;
	  shostak) PVSDEFAULTDP=shostak;;
	  *) echo "The decision-procedures argument must be ics or shostak"
	     exit 1;;
	esac
	shift;;
     -force-decision-procedures)
        case $2 in
	  ics) PVSFORCEDP=:ics;;
	  shostak) PVSFORCEDP=:shostak;;
	  *) echo "The force-decision-procedures argument must be ics or shostak"
	     exit 1;;
	esac
	shift;;
     -nw)    nowin=1
             flags="$flags $1";;
     -nobg)  nobg=1;;
     -patchlevel)
        case $2 in
	  none) PVSPATCHLEVEL=0;;
	  rel)  PVSPATCHLEVEL=1;;
	  test) PVSPATCHLEVEL=2;;
	  exp)  PVSPATCHLEVEL=3;;
	  0|1|2|3) PVSPATCHLEVEL=$2;;
	  *) echo "The patchlevel must be none, rel, test, exp, or 0-3"
             exit 1;;
	esac
        shift;;
     -batch) PVSNONINTERACTIVE=t
             batch="$1";;
     -timeout) PVSTIMEOUT=$2
         if expr $PVSTIMEOUT : '\([0-9]*\)' != $PVSTIMEOUT > /dev/null; then
	   echo "The -timeout must be an integer"
	   exit 1
	 fi
	 shift;;
     -raw) unset PVSINEMACS
           rawmode="yes";;
     -v) case $2 in
           0|1|2|3) PVSVERBOSE=$2
                    shift;;
	   *) echo "The -v argument must be in the range 0-3"
              exit 1;;
	 esac;;
     -name|-title|-xrm) PVSXINIT="$PVSXINIT $1 $2"
                        shift;;
     -q|-no-init-file) flags="$flags $1"
                       PVSMINUSQ="-q"
		       dotemacs= ;;
     -E) PVSEVALLOAD="$PVSEVALLOAD $2"
                     shift;;
     -L) PVSEVALLOAD="$PVSEVALLOAD (load \"$2\")"
                     shift;;
     -e) emacsargs="$emacsargs --eval $2"
         shift;;
     -l) emacsargs="$emacsargs --load $2"
         shift;;
     -ee|-eval)
        echo "Use -E, not $1, for lisp evaluation argument to PVS"
        exit 1;;
    --eval)
      echo "Use -E/-e, not $1, for lisp/emacs evaluation argument to PVS"
      exit 1;;
     -load)
        echo "Use -L, not $1, for loading lisp files in PVS"
        exit 1;;
     -where|--where) echo $PVSPATH
                     exit 0;;
     -version|--version) unset PVSINEMACS
                         getversion="yes";;
     -h|-help|--help)  echo "usage:
       pvs [-options ...] [file]
where options include:
  -h | -help | --help  print out this message
  -version | --version show the PVS version number
  -emacs emacsref    emacs, xemacs, alias, or pathname
  -load-after efile  loads emacs file after PVS emacs files
  -lisp name         lisp image name (allegro, cmulisp, or sbclisp)
  -runtime           use the runtime image
  -decision-procedures  set default decision procedures (ics or shostak)
  -force-decision-procedures  forces the decision procedures (ics or shostak)
  -patchlevel level  patchlevel (none, rel, test, exp or 0-3, resp.)
  -batch             run in batch mode
  -timeout number    use a timeout for commands or proofs in batch mode
  -nobg              don't put PVS in the background
  -port number       run PVS as XML-RPC server on port number
  -raw               run PVS without Emacs
  -v number          verbosity level for batch mode (0-3)
  -q           do not load ~/.emacs, ~/.pvsemacs, or ~/.pvs.lisp files
  -e expr      evaluate the Emacs expression
  -l efile     load the given Emacs file (before PVS emacs files)
  -E expr      evaluate the Lisp expression
  -L lfile     load the given Lisp file (after PVS initializes)
  and any Emacs or X window options
To change the title and icon names, use -title and -xrm, for example,
  pvs -title foo -xrm \"pvs*iconName:bar\""
	            exit 0;;
     *)      flags="$flags $1";;
   esac
   shift
done

if [ -n "$PVSEVALLOAD" ]
    then PVSEVALLOAD="(progn $PVSEVALLOAD)"
fi

PVSEMACS=${PVSEMACS:-"emacs"}

# Determine the system type and set PVSARCH accordingly
case $opsys in
  SunOS) majvers=`uname -r | cut -d"." -f1`
	 if [ $majvers = 4 ]
	    then echo "PVS only runs under Mac OS X, Linux, or FreeBSD"; exit 1
	 fi
	 PVSARCH=sun4;;
  Linux) # If Linux, we need to determine the Redhat version to use.
	 opsys=Linux
	 majvers=
	 case `uname -m` in
	   x86_64) PVSARCH=ix86_64 ;;
	   *86*)   PVSARCH=ix86 ;;
	   *) echo "PVS only runs on Intel under Linux"; exit 1
	 esac
	 # Allegro does not work with Linux's New Posix Thread Library (NPTL)
	 # used in newer Red Hat kernels and 2.6 kernels.  This will force
	 # the old thread-implementation.
	 export LD_ASSUME_KERNEL=2.4.19;
	 # See if setting this leads to problems - if it does, then
	 # uname exits with an error and we unset it.
	 uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL
	 ;;
  FreeBSD) opsys=Linux
	   majvers=
	   case `uname -m` in
	     x86_64) PVSARCH=ix86_64 ;;
	     *86*)   PVSARCH=ix86 ;;
	     *) echo "PVS only runs on Intel under Linux"; exit 1
	   esac
	   # Allegro does not work with Linux's New Posix Thread Library (NPTL)
	   # used in newer Red Hat kernels and 2.6 kernels.  This will force
	   # the old thread-implementation.
	   export LD_ASSUME_KERNEL=2.4.19;
	   # See if setting this leads to problems - if it does, then
	   # uname exits with an error and we unset it.
	   uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL
           ;;
  Darwin) case `uname -p` in
            powerpc) PVSARCH=powerpc;;
	    i*86) PVSARCH=ix86;;
	    *) PVSARCH=`uname -p`;;
	  esac
          opsys=MacOSX
	  export LC_ALL="en_US.UTF-8"
	  # Hack for emacs on Mac - /usr/bin/emacs doesn't support X
	  # but if X is enabled, then DISPLAY env var is set
	  if [ ! `(export EMACS=$PVSEMACS; $PVSPATH/emacs/configured-for-x)` ]
	  then nowin=1
	    echo "$PVSEMACS does not support X; running in terminal mode"
	  fi
          #majvers=`uname -r | cut -d"." -f1`
	  majvers=
	  ;;
  *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1
esac

PVSBINPATH=$PVSPATH/bin/$PVSARCH-$opsys${majvers}
# Check if this is a 64-bit platform, but only 32-bit available
if [ "$PVSARCH" = "ix86_64" -a ! -x "$PVSBINPATH" ]
    then PVSBINPATH=$PVSPATH/bin/ix86-$opsys${majvers}
fi

if [ -n "$PVSLISP" -a "$PVSLISP" != "allegro" -a "$PVSLISP" != "cmulisp" -a "$PVSLISP" != "sbclisp" ]
  then echo "ERROR: PVSLISP must be unset, or set to 'allegro', 'cmulisp', or 'sbclisp'"
       exit 1
fi

if [ -z "$PVSLISP" ]
   then if   [ -x $PVSBINPATH/devel/pvs-allegro ]
        then PVSLISP=allegro
        elif [ -x $PVSBINPATH/runtime/pvs-allegro ]
        then PVSLISP=allegro
        elif [ -x $PVSBINPATH/devel/pvs-cmulisp ]
        then PVSLISP=cmulisp
        elif [ -x $PVSBINPATH/runtime/pvs-cmulisp ]
        then PVSLISP=cmulisp
	elif [ -e $PVSBINPATH/devel/pvs-sbclisp ]
	then PVSLISP=sbclisp
	elif [ -e $PVSBINPATH/runtime/pvs-sbclisp ]
	then PVSLISP=sbclisp
        else echo "No executable available in $PVSBINPATH"
             exit 1
        fi
fi

# If PVSIMAGE is set, PVSLISP must be sbclisp
if [ "$PVSIMAGE" ]; then PVSLISP=sbclisp; fi
# Set PVSIMAGE if not already given
PVSIMAGE=${PVSIMAGE:=pvs-$PVSLISP}

if [ -d $PVSBINPATH/devel -a -e $PVSBINPATH/devel/$PVSIMAGE -a ! "$pvsruntime" ]
then
  PATH=$PVSBINPATH/devel:$PVSBINPATH:$PVSPATH/bin:$PATH
  LD_LIBRARY_PATH=$PVSBINPATH/devel:$LD_LIBRARY_PATH
  DYLD_LIBRARY_PATH=$PVSBINPATH/devel:$DYLD_LIBRARY_PATH
  pvsimagepath=$PVSBINPATH/devel/$PVSIMAGE
elif [ -d $PVSBINPATH/runtime -a -e $PVSBINPATH/runtime/$PVSIMAGE ]
then
  PATH=$PVSBINPATH/runtime:$PVSBINPATH:$PVSPATH/bin:$PATH
  LD_LIBRARY_PATH=$PVSBINPATH/runtime:$LD_LIBRARY_PATH
  DYLD_LIBRARY_PATH=$PVSBINPATH/runtime:$DYLD_LIBRARY_PATH
  pvsimagepath=$PVSBINPATH/runtime/$PVSIMAGE
else
  echo "Cannot find $PVSBINPATH/runtime/$PVSIMAGE"
  echo "Check the values of PVSPATH and PVSLISP"
  exit 1
fi

# Here is where we handle the different flags for the different lisps
case $PVSLISP in
    allegro) 
	ALLEGRO_CL_HOME=$PVSPATH/bin/$PVSARCH-$opsys${majvers}/home
	noinit="-qq"
	evalflag="-e"
	;;
    cmulisp)
	noinit="-quiet -noinit"
	evalflag="-eval"
	;;
    sbclisp)
	noinit="--no-userinit"
	evalflag="--eval"
	;;
esac

PVSPATCHLEVEL=${PVSPATCHLEVEL:-2}

case $PVSPATCHLEVEL in
    none) PVSPATCHLEVEL=0;;
    rel)  PVSPATCHLEVEL=1;;
    test) PVSPATCHLEVEL=2;;
    exp)  PVSPATCHLEVEL=3;;
esac

if [ "$PVSVERBOSE" -a ! "$batch" ]
 then echo "The -verbose flag is used only with -batch; it will be ignored"
fi

if [ "$PVSTIMEOUT" -a ! "$batch" ]
 then echo "The -timeout flag is used only with -batch; it will be ignored"
fi

PVSVERBOSE=${PVSVERBOSE:-0}

export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
export PVSARCH PVSIMAGE PVSPATH PVSBINPATH PATH PVSLISP PVSVERBOSE PVSTIMEOUT
export PVSPORT PVSPATCHLEVEL PVSMINUSQ PVSFORCEDP PVSDEFAULTDP
export PVSNONINTERACTIVE PVSINEMACS PVSEVALLOAD

# Warn about for PVS_LIBRARY_PATH conflicts
if [ "$PVS_LIBRARY_PATH" -a ! "$getversion" -a ! "$rawmode" ]
 then
  plibs=`for plib in ${PVSPATH}/lib/*; do if [ -d $plib -a -f $plib/.pvscontext ]; then basename $plib; fi; done`
  for path in `echo $PVS_LIBRARY_PATH | tr ':' ' '`
   do for plib in $plibs
       do if [ -d $path/$plib ]
           then echo "Warning: PVS_LIBRARY_PATH $path/$plib"
	        echo "         conflicts with $PVSPATH/lib/$plib"
		echo "    $plib will default to $path/$plib"
	  fi
       done
   done
fi

pvsemacsinit="-load $PVSPATH/emacs/go-pvs.el $emacsargs $loadafter"

if [ ! "$getversion" -a ! "$rawmode" -a ! "$batch" -a "$DISPLAY" != "" -a "$nowin" != 1 ]
 then
  HOST=${HOST:-`uname -n`}

  # Now try to determine which version of Emacs we're running, and set
  # PVSXINIT accordingly.

  case $PVSEMACS in
    *[xl]emacs*) \
      if [ $nobg ] ; then
        ("$PVSEMACS" $flags -name pvs -in PVS@$HOST -wn PVS@$HOST \
                   $PVSXINIT $pvsemacsinit )
      else
        ("$PVSEMACS" $flags -name pvs -in PVS@$HOST -wn PVS@$HOST \
                   $PVSXINIT $pvsemacsinit &)
      fi;;
    *) \
      if [ $nobg ] ; then
        ("$PVSEMACS" $flags -name pvs $PVSXINIT $pvsemacsinit)
      else
        ("$PVSEMACS" $flags -name pvs $PVSXINIT $pvsemacsinit &)
      fi;;
  esac
elif [ $getversion ]
  then
    # Make sure there are no spaces in the eval form - otherwise it goes
    # through the pvs-cmulisp script and gets mangled.
    echo `$pvsimagepath $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"`
elif [ $rawmode ]
  then
    if [ -n "$emacsargs" ]
      then echo "Emacs flags '$emacsargs' will be ignored in raw mode"
    fi
    $pvsimagepath $noinit $flags
elif [ $batch ]
  then
    "$PVSEMACS" $batch $dotemacs $pvsemacsinit $flags 2>&1
else
  "$PVSEMACS" $pvsemacsinit $flags
fi