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],[8.0],[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 sets build, build_cpu, build_vendor, and build_os
AC_CANONICAL_BUILD
	
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	

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

dnl AC_CHECK_PROGS(ETAGS,etags etags-emacs etags.emacs,no)
dnl if test "$ETAGS" = no ; then
dnl 	AC_MSG_WARN(Cannot find etags)
dnl 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_WARN(Cannot find tar)
fi

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

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

AC_CHECK_PROG(GIT,git,git,no)
if test "$GIT" = no ; then
	AC_MSG_WARN(Cannot find git; probably not needed)
fi

AC_CHECK_PROG(SBCL,sbcl,sbcl,no)
if test "$SBCL" = no ; then
	AC_MSG_WARN(Cannot find sbcl; install it or set SBCL_HOME or ALLEGRO_HOME to build pvs)
fi

dnl ~/.config/common-lisp/source-registry.conf.d/20-pvs.conf

# 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 lib/registry.conf])
AC_OUTPUT

chmod a+x pvs pvsio proveit provethem