configure.in

####################################################################
#                                                                  #
#  The Why3 Verification Platform   /   The Why3 Development Team  #
#  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  #
#                                                                  #
#  This software is distributed under the terms of the GNU Lesser  #
#  General Public License version 2.1, with the special exception  #
#  on linking described in file LICENSE.                           #
#                                                                  #
####################################################################

#
# 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).

AC_INIT([Why3], m4_esyscmd([. ./Version; printf "$VERSION"]))

# verbosemake

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

# LOCAL_CONF

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

# RELOCATABLE INSTALLATION

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

# NATIVE

AC_ARG_ENABLE(native-code,
    AS_HELP_STRING([--disable-native-code], [use only the byte-code compiler]),,
    enable_native_code=yes)

# Zarith

AC_ARG_ENABLE(zarith,
    AS_HELP_STRING([--disable-zarith], [use Nums instead of Zarith for computations]),,
    enable_zarith=yes)


# camlzip

AC_ARG_ENABLE(zip,
    AS_HELP_STRING([--enable-zip], [use LZ compression to store session files]),,
    enable_zip=yes)

# menhirLib

AC_ARG_ENABLE(menhirLib,
    AS_HELP_STRING([--enable-menhirLib], [use MenhirLib parsing library]),,
    enable_menhirLib=yes)

# IDE

AC_ARG_ENABLE(ide,
    AS_HELP_STRING([--disable-ide], [do not build Why3 IDE]),,
    enable_ide=yes)

# Coq tactic and libraries

AC_ARG_ENABLE(coq-tactic,
    AS_HELP_STRING([--disable-coq-tactic], [do not build Coq "why3" tactic]),,
    enable_coq_tactic=yes)

AC_ARG_ENABLE(coq-libs,
    AS_HELP_STRING([--disable-coq-libs], [do not build Coq realizations]),,
    enable_coq_libs=yes)

# PVS libraries

AC_ARG_ENABLE(pvs-libs,
    AS_HELP_STRING([--disable-pvs-libs], [do not build PVS realizations]),,
    enable_pvs_libs=yes)

# Isabelle libraries

AC_ARG_ENABLE(isabelle-libs,
    AS_HELP_STRING([--disable-isabelle-libs], [do not build Isabelle realizations]),,
    enable_isabelle_libs=yes)

# hypothesis selection

AC_ARG_ENABLE(hypothesis-selection,
    AS_HELP_STRING([--disable-hypothesis-selection], [do not support hypothesis selection]),,
    enable_hypothesis_selection=yes)

# documentation

AC_ARG_ENABLE(doc,
    AS_HELP_STRING([--disable-doc], [do not build documentation]),,
    enable_doc=yes)

AC_ARG_ENABLE(html-doc,
    AS_HELP_STRING([--disable-html-doc], [do not build HTML documentation]),,
    enable_html_doc=yes)

# Experimental Jessie3 Frama-C plugin, disabled by default

AC_ARG_ENABLE(frama-c,
    AS_HELP_STRING([--enable-frama-c], [enable Frama-C plugin]),,
    [enable_frama_c=no
     reason_frama_c=" (disabled by default)"])

# profiling

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

# Emacs compilation

AC_ARG_ENABLE(emacs-compilation,
    AS_HELP_STRING([--disable-emacs-compilation], [do not compile why3.elc]),,
    enable_emacs_compilation=yes)

# 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 "'
  AC_MSG_RESULT(.exe <Cygwin>)
else
if uname -s | grep -q MINGW ; then
  EXE=.exe
  STRIP=strip
  AC_MSG_RESULT(.exe <MinGW>)
else
  EXE=
  STRIP=strip
  AC_MSG_RESULT(<none>)
fi
fi

AC_PROG_CC
# Add compatibility for C99
AC_PROG_CC_STDC
AC_PROG_MKDIR_P
AC_PROG_INSTALL

# Check for Ocaml compilers

# we first look for ocamlc in the path; if not present, we fail
AC_CHECK_PROGS(OCAMLC,ocp-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.*|4.00.*|4.01.*|4.02.[[0-2]])
        AC_MSG_ERROR(You need Objective Caml 4.02.3 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_PROGS(OCAMLOPT,ocp-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_PROGS(OCAMLCDOTOPT,ocp-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_PROGS(OCAMLOPTDOTOPT,ocp-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(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
	AC_MSG_ERROR(Cannot find menhir.)
fi

## 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

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

if test "$enable_local" = yes ; then
   OCAMLINSTALLLIB=$LOCALDIR/lib
else
   #if ocamlfind is used it gives the install path for ocaml library
   if test "$USEOCAMLFIND" = yes; then
      OCAMLINSTALLLIB=$(ocamlfind printconf destdir)
   else
      OCAMLINSTALLLIB=$OCAMLLIB
   fi
fi

# checking for rubber
if test "$enable_doc" = yes ; then
   AC_CHECK_PROG(RUBBER,rubber,rubber,no)
   if test "$RUBBER" = no ; then
      enable_doc=no
      enable_html_doc=no
      reason_doc=" (rubber not found)"
      AC_MSG_WARN([Cannot find rubber, documentation disabled.])
   fi
else
   enable_html_doc=no
fi

# checking for hevea (note that the pdf documentation DOES NOT use hevea.sty)
if test "$enable_html_doc" = yes ; then
   AC_CHECK_PROG(HEVEA,hevea,hevea,no)
   if test "$HEVEA" = no ; then
      enable_html_doc=no
      reason_html_doc=" (hevea not found)"
      AC_MSG_WARN([Cannot find hevea, HTML documentation disabled.])
   fi
fi

# checking for hacha
if test "$enable_html_doc" = yes ; then
   AC_CHECK_PROG(HACHA,hacha,hacha,no)
   if test "$HACHA" = no ; then
      enable_html_doc=no
      reason_html_doc=" (hacha not found)"
      AC_MSG_WARN([Cannot find hacha, HTML documentation disabled.])
   fi
fi

# checking for emacs
if test "$enable_emacs_compilation" = yes ; then
   AC_CHECK_PROG(EMACS,emacs,emacs,no)
   if test "$EMACS" = no ; then
      enable_emacs_compilation=no
      AC_MSG_WARN([Cannot find emacs, compilation of why3.elc disabled.])
   fi
fi

# checking for Num
if test "$USEOCAMLFIND" = yes; then
   NUMINCLUDE=$(ocamlfind query num)
fi
if test -n "$NUMINCLUDE"; then
   echo "ocamlfind found num in $NUMINCLUDE"
else
   AC_CHECK_FILE($OCAMLLIB/nums.cma,,found_num=no)
      if test "$found_num" = no; then
         AC_MSG_ERROR([Library Num not found.])
      fi
fi

# checking for Zarith
if test "$enable_zarith" = yes; then
   if test "$USEOCAMLFIND" = yes; then
      BIGINTINCLUDE=$(ocamlfind query zarith)
   fi
   if test -n "$BIGINTINCLUDE"; then
      echo "ocamlfind found zarith in $BIGINTINCLUDE"
      BIGINTINCLUDE="-I $BIGINTINCLUDE"
   else
      AC_CHECK_FILE($OCAMLLIB/zarith/zarith.cma,,enable_zarith=no)
      if test "$enable_zarith" = no; then
         AC_MSG_WARN([Lib Zarith not found, using Nums instead.])
         reason_zarith=" (zarith not found)"
      else
         BIGINTINCLUDE="-I +zarith"
      fi
   fi
fi

if test "$enable_zarith" = yes; then
   BIGINTLIB=zarith
   BIGINTPKG=zarith
else
   BIGINTLIB=nums
   BIGINTPKG=num
fi

# checking for camlzip
if test "$enable_zip" = yes; then
   if test "$USEOCAMLFIND" = yes; then
      ZIPINCLUDE=$(ocamlfind query zip)
   fi
   if test -n "$ZIPINCLUDE"; then
      echo "ocamlfind found camlzip in $ZIPINCLUDE"
      ZIPINCLUDE="-I $ZIPINCLUDE"
   else
      AC_CHECK_FILE($OCAMLLIB/zip/zip.cma,,enable_zip=no)
      if test "$enable_zip" = no; then
         AC_MSG_WARN([Lib camlzip not found, sessions files will not be compressed.])
         reason_zip=" (camlzip not found)"
      else
         ZIPINCLUDE="-I +zip"
      fi
   fi
fi

if test "$enable_zip" = yes; then
   ZIPLIB=zip
else
   ZIPLIB=
fi

if test "$enable_menhirLib" = yes; then
  if test "$USEOCAMLFIND" = yes; then
     MENHIRINCLUDE=$(ocamlfind query menhirLib)
  fi
  if test -n "$MENHIRINCLUDE"; then
     echo "ocamlfind found menhirLib in $MENHIRINCLUDE"
     MENHIRINCLUDE="-I $MENHIRINCLUDE"
  else
     AC_CHECK_FILE($OCAMLLIB/menhirLib/menhirLib.cmx,,enable_menhirLib=no)
     if test "$enable_menhirLib" = no; then
        AC_MSG_WARN([Lib menhirLib not found, parser source files will be bigger.])
        reason_menhirLib=" (menhirLib not found)"
     else
        MENHIRINCLUDE="-I +menhirLib"
     fi
   fi
fi

if test "$enable_menhirLib" = yes; then
   MENHIRLIB=menhirLib
else
   MENHIRLIB=
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 lablgtk2.sourceview2)
      if test -z "$LABLGTKSV2LIB"; then
         LABLGTKSV2LIB=$(ocamlfind query lablgtksourceview2)
      fi
   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

if test "$enable_ide" = yes ; then
  LABLGTK2PKG="lablgtk2 lablgtk2.init lablgtk2.sourceview2"
else
  LABLGTK2PKG=
fi

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

dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)


# checking for js_of_ocaml
HASJSOFOCAML=no
if test "$USEOCAMLFIND" = yes; then
   JSOFOCAML=$(ocamlfind query js_of_ocaml)
   if test -z "$JSOFOCAML"; then
      reason_jsofocaml=" (js_of_ocaml not found)"
   else
      JSOFOCAMLPPX=$(ocamlfind query js_of_ocaml-ppx)
      if test -z "$JSOFOCAMLPPX"; then
         reason_jsofocaml=" (js_of_ocaml-ppx not found)"
      else
         HASJSOFOCAML=yes
      fi
   fi
else
   reason_jsofocaml=" (ocamlfind not available)"
fi

# Coq

enable_coq_support=yes
enable_coq_fp_libs=yes

coq_compat_version=

if test "$enable_coq_tactic" = no -a "$enable_coq_libs" = no; then
   enable_coq_support=no
   reason_coq_support=" (disabled by user)"
fi

if test "$enable_coq_tactic" = no; then
   reason_coq_tactic=" (disabled by user)"
fi

if test "$enable_coq_support" = yes; then
   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)"
   fi
fi

if test "$enable_coq_support" = yes; then
   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' `

   #Even if the name of the variable is CAMLP4 the value can be camlp5
   CAMLP4BIN=`$COQC -config | sed -n -e 's/CAMLP4BIN=\(.*\)$/\1/p'`
   CAMLP4=`$COQC -config | sed -n -e 's/CAMLP4=\(.*\)$/\1/p'`
   COQCAMLPLIB=`$COQC -config | sed -n -e 's/CAMLP4LIB=\(.*\)$/\1/p'`

   case $COQVERSION in
      8.4*)
         coq_compat_version="COQ84"
         COQPPLIBS="$COQLIB/parsing/grammar.cma"
         AC_MSG_RESULT($COQVERSION)
         if test "$enable_coq_tactic" = yes; then
            enable_coq_tactic=no
            reason_coq_tactic=" (coq >= 8.5 not found)"
         fi
         ;;
      8.5*)
         coq_compat_version="COQ85"
         COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
         AC_MSG_RESULT($COQVERSION)
         ;;
      8.6*)
         coq_compat_version="COQ86"
         COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
         AC_MSG_RESULT($COQVERSION)
         ;;
      8.7*)
         coq_compat_version="COQ87"
         COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
         AC_MSG_RESULT($COQVERSION)
         ;;
      *)
         enable_coq_support=no
         AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
         reason_coq_support=" (version is $COQVERSION but need version 8.4 or later)"
         ;;
   esac
fi

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

if test "$enable_coq_support" = no; then
   enable_coq_tactic=no
   enable_coq_libs=no
   COMPILETIMECOQ=
else
   COMPILETIMECOQ="\\\"Coq\\\", \\\"$COQVERSION\\\"; "
fi

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

if test "$enable_coq_tactic" = yes; then
   AC_PATH_PROG(COQCAMLP,${CAMLP4}o,no,$CAMLP4BIN)
   if test "$COQCAMLP" = no; then
      enable_coq_tactic=no
      AC_MSG_WARN(Cannot find camlpXo.)
      reason_coq_tactic=" (camlpXo not found)"
   fi
fi

if test "$enable_coq_tactic" = yes -a "$OCAMLBEST" = "byte"; then
   AC_CHECK_PROG(COQTOPBYTE,coqtop.byte,coqtop.byte,no)
   if test "$COQTOPBYTE" = no; then
      enable_coq_tactic=no
      AC_MSG_WARN(Cannot find coqtop.byte.)
      reason_coq_tactic=" (byte compilation needed but coqtop.byte not found)"
   fi
fi

if test "$enable_coq_libs" = yes; then
   AC_MSG_CHECKING([for Flocq])
   AS_IF(
     [ echo "Require Import Flocq.Flocq_version BinNat." \
            "Goal (20500 <= 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.5 not found)" ])
   rm -f conftest.v conftest.vo conftest.err
fi

# PVS

if test "$enable_pvs_libs" = no; then
    enable_pvs_support=no
    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.*)
	        enable_pvs_support=yes
                AC_MSG_RESULT($PVSVERSION)
                ;;
          *)
                AC_MSG_RESULT($PVSVERSION)
                enable_pvs_support=no
	        AC_MSG_WARN(You need PVS 6.0 or higher; PVS discarded)
                reason_pvs_support=" (need version 6.0 or higher)"
                ;;
        esac
    fi
fi

if test "$enable_pvs_support" = no; then
   enable_pvs_libs=no
   COMPILETIMEPVS=
else
   COMPILETIMEPVS="\\\"PVS\\\", \\\"$PVSVERSION\\\"; "
fi

# Isabelle

# Default version used for generation of realization in the case Isabelle is not
# detected or Why3 is compiled with disable-isabelle.
ISABELLEVERSION=2017

if test "$enable_isabelle_libs" = no; then
    enable_isabelle_support=no
    reason_isabelle_support=" (disabled by user)"
else
    AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
    if test "$ISABELLE" = no ; then
       enable_isabelle_support=no
       AC_MSG_WARN(Cannot find isabelle.)
       reason_isabelle_support=" (isabelle not found)"
    else
        AC_MSG_CHECKING(Isabelle version)
        ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `

        case $ISABELLEDETECTEDVERSION in
          2016-1*)
	        enable_isabelle_support=yes
                ISABELLEVERSION=2016-1
                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                ;;
          2017*)
	        enable_isabelle_support=yes
                ISABELLEVERSION=2017
                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                ;;
          *)
                AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
                enable_isabelle_support=no
	        AC_MSG_WARN(You need Isabelle 2016-1 or later; Isabelle discarded)
                reason_isabelle_support=" (need version >= 2016-1)"
                ;;
        esac
    fi
fi

if test "$enable_isabelle_support" = no; then
   enable_isabelle_libs=no
fi

if test "$enable_pvs_libs" = yes; then
   AC_MSG_CHECKING([for NASA PVS library])
   enable_pvs_libs=no
   reason_pvs_libs=" (no NASA PVS library in PVS_LIBRARY_PATH)"
   for dir in  `echo $PVS_LIBRARY_PATH | tr ':' ' '`; do
       if test -f $dir/nasalib-version; then
          enable_pvs_libs=yes
          reason_pvs_libs=""
       fi
   done
   AC_MSG_RESULT($enable_pvs_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
       reason_hypothesis_selection=" (ocamlgraph not found)"
       AC_MSG_WARN([Lib ocamlgraph not found, hypothesis selection disabled.])
     fi
   fi
fi

#check frama-c
if test "$enable_frama_c" = yes ; then
   AC_CHECK_PROG(FRAMAC,frama-c,frama-c,no)
   if test "$FRAMAC" = no ; then
        AC_MSG_WARN(Cannot find Frama-C.)
        enable_frama_c="no"
        reason_frama_c=" (frama-c not found)"
   else
      AC_MSG_CHECKING(Frama-C version)
      FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|Version: *\(.*\)$|\1|p'`
      AC_MSG_RESULT($FRAMAC_VERSION)
      case $FRAMAC_VERSION in
         Sodium-*) ;;
         *) AC_MSG_WARN(Version Sodium required.)
            enable_frama_c=no
            reason_frama_c=" (version Sodium required)"
            ;;
      esac
      FRAMAC_SHARE=`$FRAMAC -print-path`
      FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
   fi
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=$PACKAGE_VERSION

# substitutions to perform
AC_SUBST(VERSION)

AC_SUBST(enable_verbose_make)

AC_SUBST(EXE)
AC_SUBST(STRIP)

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)
AC_SUBST(OCAMLINSTALLLIB)
dnl AC_SUBST(OCAMLV)
dnl AC_SUBST(FORPACK)
AC_SUBST(OCAMLGRAPHLIB)
dnl AC_SUBST(OCAMLWEB)
AC_SUBST(MENHIR)

AC_SUBST(enable_profiling)

AC_SUBST(COQCAMLP)
AC_SUBST(COQCAMLPLIB)

AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)

AC_SUBST(HASJSOFOCAML)

AC_SUBST(META_OCAMLGRAPH)

AC_SUBST(enable_zarith)
AC_SUBST(BIGINTINCLUDE)
AC_SUBST(BIGINTLIB)
AC_SUBST(BIGINTPKG)

AC_SUBST(enable_zip)
AC_SUBST(ZIPINCLUDE)
AC_SUBST(ZIPLIB)

AC_SUBST(enable_menhirLib)
AC_SUBST(MENHIRINCLUDE)
AC_SUBST(MENHIRLIB)

AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_support)
AC_SUBST(enable_coq_fp_libs)
AC_SUBST(coq_compat_version)

AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQPPLIBS)
AC_SUBST(COMPILETIMECOQ)

AC_SUBST(enable_pvs_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
AC_SUBST(COMPILETIMEPVS)

AC_SUBST(enable_isabelle_libs)
AC_SUBST(ISABELLE)
AC_SUBST(ISABELLEVERSION)

AC_SUBST(enable_hypothesis_selection)

AC_SUBST(enable_doc)
AC_SUBST(enable_html_doc)

AC_SUBST(RUBBER)
AC_SUBST(HEVEA)
AC_SUBST(HACHA)

AC_SUBST(enable_emacs_compilation)
AC_SUBST(EMACS)

AC_SUBST(enable_frama_c)

AC_SUBST(FRAMAC)
AC_SUBST(FRAMAC_VERSION)
AC_SUBST(FRAMAC_SHARE)
AC_SUBST(FRAMAC_LIBDIR)

AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)

AC_SUBST(enable_relocation)

dnl AC_SUBST(PSVIEWER)
dnl AC_SUBST(PDFVIEWER)

# Finally create the Makefile from Makefile.in
AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
AC_CONFIG_FILES(lib/why3/META)
AC_CONFIG_FILES(.merlin)
AC_CONFIG_FILES(src/jessie/Makefile)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/config.sh doc/version.tex;
chmod a-w lib/why3/META;
chmod a-w .merlin;
chmod a-w src/jessie/Makefile;
chmod u+x src/config.sh)

AC_OUTPUT


# Summary

echo
echo "                 Summary"
echo "-----------------------------------------"
echo "Verbose make                : $enable_verbose_make"
echo "OCaml compiler              : yes"
echo "    Version                 : $OCAMLVERSION"
echo "    Library path            : $OCAMLLIB"
echo "    Native compilation      : $enable_native_code"
echo "    Profiling               : $enable_profiling"
echo "Components"
echo "    GTK IDE                 : $enable_ide$reason_ide"
echo "    Web IDE                 : $HASJSOFOCAML$reason_jsofocaml"
echo "    GMP arithmetic          : $enable_zarith$reason_zarith"
echo "    Compressed sessions     : $enable_zip$reason_zip"
echo "    MenhirLib support       : $enable_menhirLib$reason_menhirLib"
echo "    Hypothesis selection    : $enable_hypothesis_selection$reason_hypothesis_selection"
echo "    Frama-C support         : $enable_frama_c$reason_frama_c"
if test "$enable_frama_c" = yes ; then
   echo "        Version             : $FRAMAC_VERSION"
   echo "        Share path          : $FRAMAC_SHARE"
   echo "        Library path        : $FRAMAC_LIBDIR"
fi
echo "Documentation               : $enable_doc$reason_doc"
if test "$enable_doc" = yes ; then
   echo "    PDF                     : yes"
   echo "    HTML                    : $enable_html_doc$reason_html_doc"
fi
echo "Support for interactive proof assistants"
echo "    Coq                     : $enable_coq_support$reason_coq_support"
if test "$enable_coq_support" = yes ; then
   echo "        Version             : $COQVERSION"
   echo "        Library path        : $COQLIB"
   echo "        \"why3\" tactic       : $enable_coq_tactic$reason_coq_tactic"
   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                     : $enable_pvs_support$reason_pvs_support"
if test "$enable_pvs_support" = yes ; then
   echo "        Version             : $PVSVERSION"
   echo "        Library path        : $PVSLIB"
   echo "        Realization support : $enable_pvs_libs$reason_pvs_libs"
fi
echo "    Isabelle                : $enable_isabelle_support$reason_isabelle_support"
if test "$enable_isabelle_support" = yes ; then
   echo "        Version             : $ISABELLEVERSION ($ISABELLEDETECTEDVERSION)"
   echo "        Realization support : $enable_isabelle_libs$reason_isabelle_libs"
fi
if test "$enable_local" = yes ; then
   echo "Installable                 : no"
else
   echo "Installable                 : yes"
   echo "    Binary path             : $bindir"
   echo "    Lib path                : $libdir/why3"
   echo "    Data path               : $datarootdir/why3"
   echo "    Ocaml Library           : $OCAMLINSTALLLIB/why3"
   echo "    Relocatable             : $enable_relocation"
fi