configure.in

##########################################################################
#                                                                        #
#  Copyright (C) 2010-2012                                               #
#    François Bobot                                                      #
#    Jean-Christophe Filliâtre                                           #
#    Claude Marché                                                       #
#    Guillaume Melquiond                                                 #
#    Andrei Paskevich                                                    #
#                                                                        #
#  This software is free software; you can redistribute it and/or        #
#  modify it under the terms of the GNU Library General Public           #
#  License version 2.1, with the special exception on linking            #
#  described in file LICENSE.                                            #
#                                                                        #
#  This software 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.                  #
#                                                                        #
##########################################################################

#
# autoconf input for Objective Caml programs
# Copyright (C) 2001 Jean-Christophe Filliâtre
#   from a first script by Georges Mariano
#
# This library is free software; you can redistribute it and/or
# modify it under the terms of the GNU Library General Public
# License version 2, as published by the Free Software Foundation.
#
# This library 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 Library General Public License version 2 for more details
# (enclosed in the file LGPL).

# the script generated by autoconf from this input will set the following
# variables:
#   OCAMLC        "ocamlc" if present in the path, or a failure, or
#                 "ocamlc.opt" if present with same version number as ocamlc
#   OCAMLOPT      "ocamlopt" (or "ocamlopt.opt" if present), or "no"
#   OCAMLBEST     "opt" if a native compiler was found; "byte" otherwise
#   OCAMLDEP      "ocamldep" or "ocamldep.opt"
#   OCAMLLEX      "ocamllex" or "ocamllex.opt"
#   OCAMLYACC     "ocamlyacc"
#   OCAMLDOC      "ocamldoc" or "ocamldoc.opt"
#   OCAMLLIB      the path to the ocaml standard library
#   OCAMLVERSION  the ocaml version number
#   OCAMLWEB      "ocamlweb" (not mandatory)


# check for one particular file of the sources
# ADAPT THE FOLLOWING LINE TO YOUR SOURCES!

AC_INIT(src/)

# verbosemake

AC_ARG_ENABLE(verbose-make,
    [  --enable-verbose-make   verbose makefile commands],,
    enable_verbose_make=no)

# LOCAL_CONF

AC_ARG_ENABLE(local,
    [  --enable-local          use Why3 in the build directory (no installation)],,
    enable_local=no)

# RELOCATABLE INSTALLATION

AC_ARG_ENABLE(relocation,
    [  --enable-relocation     allow for later relocation of Why3 installation],,
    enable_relocation=no)

# NATIVE

AC_ARG_ENABLE(native-code,
    [  --enable-native-code    use the native-code compiler if available],,
    enable_native_code=yes)

# IDE

AC_ARG_ENABLE(ide,
    [  --enable-ide            enable Why3 IDE],,
    enable_ide=yes)

# Bench

AC_ARG_ENABLE(bench,
    [  --enable-bench          enable Why3 benchmarking tool],,
    enable_bench=yes)

# Coq plugin and libraries

AC_ARG_ENABLE(coq-plugin,
    [  --enable-coq-plugin     enable Coq plugin],,
    enable_coq_plugin=yes)

AC_ARG_ENABLE(coq-libs,
    [  --enable-coq-libs       enable Coq realizations],,
    enable_coq_libs=yes)

# PVS libraries

AC_ARG_ENABLE(pvs-libs,
    [  --enable-pvs-libs       enable PVS realizations],,
    enable_pvs_libs=yes)

# hypothesis selection

AC_ARG_ENABLE(hypothesis-selection,
    [  --enable-hypothesis-selection    enable hypothesis selection support],,
    enable_hypothesis_selection=yes)

# documentation

AC_ARG_ENABLE(doc,
    [  --enable-doc            build documentation],,
    enable_doc=yes)

# debug symbols

AC_ARG_ENABLE(debug,
    [  --enable-debug          enable debugging symbols],,
    enable_debug=no)

# profiling

AC_ARG_ENABLE(profiling,
    [  --enable-profiling      enable profiling],,
    enable_profiling=no)

# either relocation or local, not both
if test "$enable_relocation" = yes ; then
if test "$enable_local" = yes ; then
    AC_MSG_ERROR(cannot use --enable-relocation and --enable-local at the same time.)
fi
fi

# Check for arch/OS

AC_MSG_CHECKING(executable suffix)
if uname -s | grep -q CYGWIN ; then
  EXE=.exe
  STRIP='echo "no strip "'
  CPULIMIT=cpulimit-win
  AC_MSG_RESULT(.exe <Cygwin>)
else
if uname -s | grep -q MINGW ; then
  EXE=.exe
  STRIP=strip
  CPULIMIT=cpulimit-win
  AC_MSG_RESULT(.exe <MinGW>)
else
  EXE=
  STRIP=strip
  CPULIMIT=cpulimit
  AC_MSG_RESULT(<none>)
fi
fi

AC_PROG_CC()

# Check for Ocaml compilers

# we first look for ocamlc in the path; if not present, we fail
AC_CHECK_PROG(OCAMLC,ocamlc,ocamlc,no)
if test "$OCAMLC" = no ; then
	AC_MSG_ERROR(Cannot find ocamlc.)
fi

# we extract Ocaml version number
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION"

case "$OCAMLVERSION" in
  0.*|1.*|2.*|3.0*|3.10*|3.11|3.11.0*|3.11.1*)
        AC_MSG_ERROR(You need Objective Caml 3.11.2 or higher);;
esac

# Ocaml library path
# old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
echo "ocaml library path is $OCAMLLIB"

# then we look for ocamlopt; if not present, we issue a warning
# if the version is not the same, we also discard it
# we set OCAMLBEST to "opt" or "byte", whether ocamlopt is available or not
AC_CHECK_PROG(OCAMLOPT,ocamlopt,ocamlopt,no)
OCAMLBEST=byte
if test "$OCAMLOPT" = no ; then
	AC_MSG_WARN(Cannot find ocamlopt; bytecode compilation only.)
else
	AC_MSG_CHECKING(ocamlopt version)
	TMPVERSION=`$OCAMLOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
	if test "$TMPVERSION" != "$OCAMLVERSION" ; then
	    AC_MSG_RESULT(differs from ocamlc; ocamlopt discarded.)
	    OCAMLOPT=no
	else
	    AC_MSG_RESULT(ok)
	    OCAMLBEST=opt
	fi
fi

# checking for native-code
if test "$enable_native_code" != yes || test "$OCAMLBEST" = byte ; then
    enable_native_code=no
    OCAMLBEST=byte
    OCAMLOPT=no
fi

# checking for ocamlc.opt
AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
if test "$OCAMLCDOTOPT" != no ; then
	AC_MSG_CHECKING(ocamlc.opt version)
	TMPVERSION=`$OCAMLCDOTOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
	if test "$TMPVERSION" != "$OCAMLVERSION" ; then
	    AC_MSG_RESULT(differs from ocamlc; ocamlc.opt discarded.)
	else
	    AC_MSG_RESULT(ok)
	    OCAMLC=$OCAMLCDOTOPT
	fi
fi

# checking for ocamlopt.opt
if test "$OCAMLOPT" != no ; then
    AC_CHECK_PROG(OCAMLOPTDOTOPT,ocamlopt.opt,ocamlopt.opt,no)
    if test "$OCAMLOPTDOTOPT" != no ; then
	AC_MSG_CHECKING(ocamlc.opt version)
	TMPVER=`$OCAMLOPTDOTOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
	if test "$TMPVER" != "$OCAMLVERSION" ; then
	    AC_MSG_RESULT(differs from ocamlc; ocamlopt.opt discarded.)
	else
	    AC_MSG_RESULT(ok)
	    OCAMLOPT=$OCAMLOPTDOTOPT
	fi
    fi
fi

# ocamldep, ocamllex and ocamlyacc should also be present in the path
AC_CHECK_PROG(OCAMLDEP,ocamldep,ocamldep,no)
if test "$OCAMLDEP" = no ; then
   AC_MSG_ERROR(Cannot find ocamldep.)
else
   AC_CHECK_PROG(OCAMLDEPDOTOPT,ocamldep.opt,ocamldep.opt,no)
   if test "$OCAMLDEPDOTOPT" != no ; then
      OCAMLDEP=$OCAMLDEPDOTOPT
   fi
fi

AC_CHECK_PROG(OCAMLLEX,ocamllex,ocamllex,no)
if test "$OCAMLLEX" = no ; then
	AC_MSG_ERROR(Cannot find ocamllex.)
else
    AC_CHECK_PROG(OCAMLLEXDOTOPT,ocamllex.opt,ocamllex.opt,no)
    if test "$OCAMLLEXDOTOPT" != no ; then
	OCAMLLEX=$OCAMLLEXDOTOPT
    fi
fi

AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
if test "$OCAMLYACC" = no ; then
	AC_MSG_ERROR(Cannot find ocamlyacc.)
fi

AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,true)
if test "$OCAMLDOC" = true ; then
    AC_MSG_WARN(Cannot find ocamldoc)
else
    AC_CHECK_PROG(OCAMLDOCOPT,ocamldoc.opt,ocamldoc.opt,no)
    if test "$OCAMLDOCOPT" != no ; then
	OCAMLDOC=$OCAMLDOCOPT
    fi
fi

AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)

## Where are the library we need
# we look for ocamlfind; if not present, we just don't use it to find
# libraries
AC_CHECK_PROG(USEOCAMLFIND,ocamlfind,yes,no)

if test "$USEOCAMLFIND" = yes; then
   OCAMLFINDLIB=$(ocamlfind printconf stdlib)
   OCAMLFIND=$(which ocamlfind)
   if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then
   USEOCAMLFIND=no;
   echo "but your ocamlfind is not compatible with your ocamlc:"
   echo "ocamlfind : $OCAMLFINDLIB, ocamlc : $OCAMLLIB"
   fi
fi

# checking for rubber
AC_CHECK_PROG(RUBBER,rubber,rubber,no)
if test "$enable_doc" = yes ; then
if test "$RUBBER" = no ; then
    enable_doc=no
    AC_MSG_WARN(cannot find rubber, documentation building disabled.)
fi
fi

# checking for lablgtk2
if test "$enable_ide" = yes ; then
   if test "$USEOCAMLFIND" = yes; then
      LABLGTK2LIB=$(ocamlfind query lablgtk2)
   fi
   if test -n "$LABLGTK2LIB";then
      echo "ocamlfind found lablgtk2 in $LABLGTK2LIB"
   else
      LABLGTK2LIB="+lablgtk2"
      AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
      if test "$enable_ide" = no; then
         AC_MSG_WARN(Lib lablgtk2 not found, IDE disabled.)
         reason_ide=" (lablgtk2 not found)"
      fi
   fi
fi

# checking for lablgtksourceview2
if test "$enable_ide" = yes ; then
   if test "$USEOCAMLFIND" = yes; then
      LABLGTKSV2LIB=$(ocamlfind query lablgtksourceview2)
   fi
   if test -n "$LABLGTKSV2LIB";then
      echo "ocamlfind found lablgtksourceview2 in $LABLGTKSV2LIB"
   else
      AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
      if test "$enable_ide" = no; then
         AC_MSG_WARN(Lib lablgtksourceview2 not found, IDE disabled.)
         reason_ide=" (lablgtksourceview2 not found)"
      fi
   fi
fi

dnl # checking for sqlite3
dnl if test "$enable_ide" = yes ; then
dnl    if test "$USEOCAMLFIND" = yes; then
dnl       SQLITE3LIB=$(ocamlfind query sqlite3)
dnl    fi
dnl    if test -n "$SQLITE3LIB";then
dnl       echo "ocamlfind found sqlite3 in $SQLITE3LIB"
dnl    else
dnl       SQLITE3LIB="+sqlite3"
dnl       AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
dnl       if test "$enable_ide" = no; then
dnl         AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
dnl    	reason_ide=" (sqlite3 not found)"
dnl       fi
dnl    fi
dnl fi

# checking for sqlite3
if test "$enable_bench" = yes ; then
   if test "$USEOCAMLFIND" = yes; then
      SQLITE3LIB=$(ocamlfind query sqlite3)
   fi
   if test -n "$SQLITE3LIB"; then
      echo "ocamlfind found sqlite3 in $SQLITE3LIB"
   else
      SQLITE3LIB="+sqlite3"
      AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_bench=no)
      if test "$enable_bench" = no; then
        AC_MSG_WARN(Lib sqlite3 not found, why3bench disabled.)
      fi
   fi
fi

dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)

dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)

# Coq

enable_coq_fp_libs=yes

if test "$enable_coq_plugins" = no -a "$enable_coq_libs" = no; then
    enable_coq_support=no
    AC_MSG_WARN(coq support disabled)
    reason_coq_support=" (disabled by user)"
else
    AC_CHECK_PROG(COQC,coqc,coqc,no)
    if test "$COQC" = no ; then
        enable_coq_support=no
        AC_MSG_WARN(Cannot find coqc.)
        reason_coq_support=" (coqc not found)"
    else
        COQLIB=`$COQC -where | sed -e 's|\\\|/|g' -e 's| |\\ |g'`
        AC_MSG_CHECKING(Coq version)
        COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `

        case $COQVERSION in
          8.0*|8.1*|8.2*)
                enable_coq_support=no
                AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
                reason_coq_support=" (need version 8.3 or later)"
                ;;
          8.*|trunk)
	        enable_coq_support=yes
                AC_MSG_RESULT($COQVERSION)
                ;;
          *)
                enable_coq_support=no
	        AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
                reason_coq_support=" (need version 8.3 or later)"
                ;;
        esac
    fi
fi

if test "$enable_coq_support" = no; then
   enable_coq_plugin=no
   enable_coq_libs=no
fi

if test "$enable_coq_plugin" = yes; then
   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_plugin=no)
   if test "$enable_coq_plugin" = no; then
      reason_coq_plugin=" ($COQLIB/kernel/term.cmi not found)"
   fi
fi

if test "$enable_coq_plugin" = yes -a "$CAMLP5O" = no; then
   enable_coq_plugin=no
   reason_coq_plugin=" (camlp5o not found)"
fi

# coq-plugin currently disabled
dnl enable_coq_plugin=no
dnl reason_coq_plugin=" (not yet implemented)"

if test "$enable_coq_libs" = yes; then
   AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
   if test "$COQDEP" = no ; then
      enable_coq_libs=no
      AC_MSG_WARN(Cannot find coqc.)
      reason_coq_libs=" (coqdep not found)"
   fi
fi

if test "$enable_coq_libs" = yes; then
   AC_MSG_CHECKING([for Flocq])
   AS_IF(
     [ echo "Require Import Flocq_version BinNat." \
            "Goal (20000 <= Flocq_version)%N. easy. Qed." > conftest.v
       "$COQC" conftest.v > conftest.err ],
     [ AC_MSG_RESULT(yes) ],
     [ AC_MSG_RESULT(no)
       enable_coq_fp_libs=no
       AC_MSG_WARN(Cannot find Flocq.)
       reason_coq_fp_libs=" (Flocq >= 2.0 not found)" ])
   rm -f conftest.v conftest.vo conftest.err
fi

# PVS

if test "$enable_pvs_libs" = no; then
    enable_pvs_support=no
    AC_MSG_WARN(PVS support disabled)
    reason_pvs_support=" (disabled by user)"
else
    AC_CHECK_PROG(PVS,pvs,pvs,no)
    if test "$PVS" = no ; then
        enable_pvs_support=no
        AC_MSG_WARN(Cannot find pvs.)
        reason_pvs_support=" (pvs not found)"
    else
        PVSLIB=`$PVS -where`
        AC_MSG_CHECKING(PVS version)
        PVSVERSION=`$PVS -version | sed -n -e 's|.*Version* *\([[^ ]]*\)$|\1|p' `

        case $PVSVERSION in
          6.0)
	        enable_pvs_support=yes
                AC_MSG_RESULT($PVSVERSION)
                ;;
          5.0)
	        enable_pvs_support=yes
                AC_MSG_RESULT($PVSVERSION)
                enable_pvs_libs=no
                AC_MSG_WARN(No PVS realizations)
                reason_pvs_libs="(requires version 6.0 or higher)"
                ;;
          *)
                enable_pvs_support=no
	        AC_MSG_WARN(You need PVS 5.0 or higher; PVS discarded)
                reason_pvs_support=" (need version 5.0 or higher)"
                ;;
        esac
    fi
fi

if test "$enable_pvs_support" = no; then
   enable_pvs_libs=no
fi

if test "$enable_pvs_libs" = yes; then
   AC_MSG_CHECKING([for NASA libraries])
   enable_pvs_nasa_libs=no
   reason_pvs_nasa_libs="(not in PVS_LIBRARY_PATH)"
   for dir in ${PVS_LIBRARY_PATH//:/ }; do
       if test -f $dir/nasalib-version; then
          enable_pvs_nasa_libs=yes
          reason_pvs_nasa_libs=""
       fi
   done
   AC_MSG_RESULT($enable_pvs_nasa_libs)
fi

# hypothesis_selection

if test "$enable_hypothesis_selection" = yes; then
   if test "$USEOCAMLFIND" = yes; then
     OCAMLGRAPHLIB=$(ocamlfind query ocamlgraph)
   fi
   if test -n "$OCAMLGRAPHLIB"; then
     echo "ocamlfind found ocamlgraph in $OCAMLGRAPHLIB"
   else
     OCAMLGRAPHLIB="+ocamlgraph"
     AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,,enable_hypothesis_selection=no)
     if test "$enable_hypothesis_selection" = no; then
       AC_MSG_WARN(Lib ocamlgraph not found, hypothesis selection disabled.)
     fi
   fi
fi

if test "$enable_local" = no; then
   LOCALDIR=''
   LOCALBIN=''
else
   LOCALDIR="${PWD}"
   LOCALBIN="${PWD}/bin/"
fi

#For the META
if test "$enable_hypothesis_selection" = yes; then
   META_OCAMLGRAPH="ocamlgraph"
else
   META_OCAMLGRAPH=""
fi

#Viewer for ps and pdf
dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)

. ./Version

BUILDDATE="$(date)"

# substitutions to perform
AC_SUBST(VERSION)
AC_SUBST(BUILDDATE)

AC_SUBST(enable_verbose_make)

AC_SUBST(EXE)
AC_SUBST(STRIP)
AC_SUBST(CPULIMIT)

AC_SUBST(OCAMLC)
AC_SUBST(OCAMLOPT)
AC_SUBST(OCAMLDEP)
AC_SUBST(OCAMLLEX)
AC_SUBST(OCAMLYACC)
AC_SUBST(OCAMLDOC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
dnl AC_SUBST(OCAMLV)
dnl AC_SUBST(FORPACK)
AC_SUBST(OCAMLGRAPHLIB)
dnl AC_SUBST(OCAMLWEB)

AC_SUBST(enable_debug)
AC_SUBST(enable_profiling)

AC_SUBST(CAMLP5O)

AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
AC_SUBST(META_OCAMLGRAPH)

AC_SUBST(enable_coq_plugin)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_fp_libs)

AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)

AC_SUBST(enable_pvs_libs)
AC_SUBST(enable_pvs_nasa_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)

AC_SUBST(enable_hypothesis_selection)

AC_SUBST(enable_doc)
AC_SUBST(RUBBER)

AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)
AC_SUBST(LOCALBIN)

AC_SUBST(enable_relocation)

dnl AC_SUBST(PSVIEWER)
dnl AC_SUBST(PDFVIEWER)

# Finally create the Makefile from Makefile.in
dnl AC_OUTPUT(Makefile)
AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
AC_CONFIG_FILES(share/provers-detection-data.conf META)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/config.sh doc/version.tex;
chmod a-w share/provers-detection-data.conf META;
chmod u+x src/config.sh)

AC_OUTPUT


# Summary

echo
echo "                 Summary"
echo "-----------------------------------------"
echo "OCaml version           : $OCAMLVERSION"
echo "OCaml library path      : $OCAMLLIB"
echo "Compile in native code  : $enable_native_code"
echo "Verbose make            : $enable_verbose_make"
echo "Why IDE                 : $enable_ide $reason_ide"
echo "Why bench tool          : $enable_bench"
echo "Why documentation       : $enable_doc"
echo "Coq support             : $enable_coq_support $reason_coq_support"
if test "$enable_coq_support" = "yes" ; then
   echo "    Version             : $COQVERSION"
   echo "    Lib                 : $COQLIB"
   echo "    Plugin support      : $enable_coq_plugin $reason_coq_plugin"
   echo "    Realization support : $enable_coq_libs $reason_coq_libs"
   if test "$enable_coq_libs" = "yes" ; then
      echo "        FP arithmetic   : $enable_coq_fp_libs $reason_coq_fp_libs"
   fi
fi
echo "PVS support             : $enable_pvs_support $reason_pvs_support"
if test "$enable_pvs_support" = "yes" ; then
   echo "    Version             : $PVSVERSION"
   echo "    Lib                 : $PVSLIB"
   echo "    Realization support : $enable_pvs_libs $reason_pvs_libs"
   if test "$enable_pvs_libs" = "yes" ; then
      echo "        NASA libraries  : $enable_pvs_nasa_libs $reason_pvs_nasa_libs"
   fi
fi
echo "hypothesis selection    : $enable_hypothesis_selection"
echo "debugging symbols       : $enable_debug"
echo "profiling               : $enable_profiling"
echo "relocatable install     : $enable_relocation"
echo "localdir                : $enable_local"