configure.in

dnl PVS autoconf input
dnl davesc Feb 2001
dnl --------------------------------------------------------------------
dnl PVS
dnl Copyright (C) 2006, SRI International.  All Rights Reserved.

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

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

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


dnl make sure we are using a recent autoconf version
AC_PREREQ(2.59)
AC_INIT([pvs],[7.1],[pvs-bugs@csl.sri.com])

dnl If it doesn't look like GNU Make is being used, give a friendly warning
tem=`make --version -f /dev/null 2>&1 | grep GNU`
if test "x$tem" = "x"; then
  AC_MSG_WARN([You need to use GNU Make when compiling])
fi

dnl This file must exist for configure to run
AC_CONFIG_SRCDIR([src/pvs.lisp])
	
dnl This sets build, build_cpu, build_vendor, and build_os
AC_CANONICAL_BUILD

dnl No longer look for lisp within configure, as it is possible to
dnl build with several lisps.  Checks have been moved into the Makefile
	
dnl Giving pvspath is optional
AC_MSG_CHECKING(pvspath)
AC_ARG_WITH(pvspath, AS_HELP_STRING([--with-pvspath=path],
				    [path=current directory if automounted]))
if test "x$with_pvspath" = "x"; then
  PVSPATH="$(pwd)"
else
  PVSPATH="$with_pvspath"
fi
if test -d "$PVSPATH"; then
   if test -f "$PVSPATH/pvs.in"; then
     AC_MSG_RESULT(found "$PVSPATH/pvs.in")
   else
     AC_MSG_ERROR(Invalid pvspath: couldn't find "$PVSPATH/pvs.in")
   fi
else
  AC_MSG_ERROR(Invalid pvspath directory: "$PVSPATH")
fi
AC_SUBST(PVSPATH)

dnl Check for programs required to build PVS
AC_PROG_CC    

AC_CHECK_PROG(LD,ld,ld,no)
if test "$LD" = no ; then
	AC_MSG_ERROR(Cannot find ld)
fi

AC_CHECK_PROG(AR,ar,ar,no)
if test "$AR" = no ; then
	AC_MSG_ERROR(Cannot find ar)
fi

AC_PROG_RANLIB	

AC_CHECK_PROG(EMACS,emacs,emacs,no)
AC_CHECK_PROG(XEMACS,xemacs,xemacs,no)
if test \( "$EMACS" = no \) -a \( "$XEMACS" = no \); then
	AC_MSG_ERROR(Cannot find emacs or xemacs)
fi
if test "$EMACS" != no; then
   AC_MSG_CHECKING(for $EMACS version >= 19)
   emacs_version=`$EMACS --version | head -n 1 | sed -e 's,[[^0-9.]],,g'`
   maj_emacs_version=`echo $emacs_version | cut -d. -f 1`
   min_emacs_version=`echo $emacs_version | cut -d. -f 2`
   if test $maj_emacs_version -lt 19; then
      AC_MSG_ERROR(found $emacs_version)
   else
      AC_MSG_RESULT(found $emacs_version)
   fi
fi
dnl Don't need to check the xemacs version

AC_CHECK_PROG(GREP,grep,grep,no)
if test "$GREP" = no ; then
	AC_MSG_ERROR(Cannot find grep)
fi

AC_CHECK_PROG(GIT,git,git,no)
if test "$GIT" = no ; then
	AC_MSG_ERROR(Cannot find git)
fi

AC_CHECK_PROG(ETAGS,etags,etags,no)
if test "$ETAGS" = no ; then
	AC_MSG_ERROR(Cannot find etags)
fi

AC_CHECK_PROG(MKDIR,mkdir,mkdir,no)
if test "$MKDIR" = no ; then
	AC_MSG_ERROR(Cannot find mkdir)
fi

AC_PROG_MKDIR_P

AC_CHECK_PROG(TAR,tar,tar,no)
if test "$TAR" = no ; then
	AC_MSG_ERROR(Cannot find tar)
fi

AC_CHECK_PROG(RM,rm,rm,no)
if test "$RM" = no ; then
	AC_MSG_ERROR(Cannot find rm)
fi

dnl Get the platform to determine relevant Makefiles to update

PLATFORM=$(./bin/pvs-platform)
export PLATFORM

# Finally create all the generated files
AC_CONFIG_FILES([Makefile pvs pvsio proveit provethem pvs-get-patches doc/api/Makefile doc/user-guide/Makefile doc/language/Makefile doc/language/pvs-doc.el doc/prover/Makefile])
AC_OUTPUT

chmod a+x pvs pvsio proveit provethem