configure.in

##########################################################################
#                                                                        #
#  Copyright (C) 2010-                                                   #
#    Francois Bobot                                                      #
#    Jean-Christophe Filliatre                                           #
#    Johannes Kanig                                                      #
#    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 Fillitre
#   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)

# rust prover

AC_ARG_ENABLE(rust-prover,
    [  --enable-rust-prover    enable Why3 rust prover],,
    enable_rust_prover=yes)

# IDE

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

# dynlink

AC_ARG_ENABLE(plugins,
    [  --enable-plugins        enable Why3 plugins],,
    enable_plugins=yes)

# Coq plugin

AC_ARG_ENABLE(coq-support,
    [  --enable-coq-support    enable Coq support],,
    enable_coq_support=yes)

# hypothesis selection

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

# profiling
ENABLE_PROFILING=yes
AC_ARG_ENABLE(profiling,
    [  --enable-profiling      enable profiling],,
    ENABLE_PROFILING=no)

# 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)
else
  EXE=
  STRIP=strip
  CPULIMIT=cpulimit
  AC_MSG_RESULT(<none>)
fi

# 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*)
        AC_MSG_ERROR(You need Objective Caml 3.10 or later);;
  3.10*)
        enable_plugins=no;;
esac

if test "$enable_plugins" = "yes" ; then
    DYNLINK="Dynlink"
else
    DYNLINK="Dynlink_"
fi

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

# checking for sqlite3
if test "$enable_rust_prover" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_rust_prover=no)
fi

# checking for lablgtk2
if test "$enable_ide" = yes ; then
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
fi
dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)

dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)

# Coq

if test "$enable_coq_support" = no; then
    enable_coq_support=no
    AC_MSG_WARN(coq support disabled)
else
    AC_CHECK_PROG(COQC,coqc,coqc,no)
    if test "$COQC" = no ; then
        enable_coq_support=no
        AC_MSG_WARN(Cannot find coqc.)
    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.*|trunk)
	        enable_coq_support=yes
                AC_MSG_RESULT($COQVERSION);;
          *)
                enable_coq_support=no
	        AC_MSG_WARN(You need Coq 8.x or later; Coq discarded);;
        esac
    fi
fi
if test "$enable_coq_support" = yes; then
   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
fi
if test "$CAMLP5O" = no; then
   enable_coq_support=no
fi

# tptp2why

AC_CHECK_PROG(MENHIR,menhir,menhir,no)

if test "$MENHIR" = no; then
  enable_tptp2why_support=no
else
  enable_tptp2why_support=yes
fi

# hypothesis_selection

if test "$enable_hypothesis_selection" = yes; then
  AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,enable_hypothesis_selection=yes,enable_hypothesis_selection=no)
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)
AC_SUBST(ENABLE_PROFILING)
dnl AC_SUBST(OCAMLV)
dnl AC_SUBST(FORPACK)
dnl AC_SUBST(OCAMLGRAPHLIB)
dnl AC_SUBST(OCAMLWEB)

AC_SUBST(CAMLP5O)

AC_SUBST(enable_ide)
AC_SUBST(enable_rust_prover)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)

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

AC_SUBST(MENHIR)
AC_SUBST(enable_tptp2why_support)

AC_SUBST(enable_hypothesis_selection)

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_OUTPUT
chmod a-w Makefile src/config.sh doc/version.tex
chmod a+x src/config.sh

# Summary

echo
echo "                 Summary"
echo "-----------------------------------------"
echo "OCaml version           : $OCAMLVERSION"
echo "OCaml library path      : $OCAMLLIB"
echo "Verbose make            : $enable_verbose_make"
echo "Why IDE                 : $enable_ide"
echo "Why plugins             : $enable_plugins"
echo "Why rust prover         : $enable_rust_prover"
echo "Coq support             : $enable_coq_support"
if test "$enable_coq_support" = "yes" ; then
   echo "    Version             : $COQVERSION"
   echo "    Lib                 : $COQLIB"
fi
echo "tptp2why support        : $enable_tptp2why_support"
echo "hypothesis selection    : $enable_hypothesis_selection"
echo "profiling               : $ENABLE_PROFILING"