configure.in

##########################################################################
#                                                                        #
#  Copyright (C) 2010-                                                   #
#    François Bobot                                                     #
#    Jean-Christophe Filliâtre                                          #
#    Claude Marché                                                      #
#    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)

# LOCAL_CONF

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

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

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

# TPTP parser

AC_ARG_ENABLE(whytptp,
    [  --enable-whytptp        enable TPTP parser (requires Menhir)],,
    enable_whytptp=yes)

# Menhir library

AC_ARG_ENABLE(menhirlib,
    [  --enable-menhirlib      enable Menhir library],,
    enable_menhirlib=no)

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

# profiling

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 higher);;
  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)

AC_CHECK_PROG(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
    enable_whytptp=no
    enable_menhirlib=no
    AC_MSG_WARN(cannot find menhir.)
fi

# checking for libmenhir
if test "$enable_menhirlib" = yes ; then
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
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
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)"
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

# checking for sqlite3
if test "$enable_ide" = yes ; then
   AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
   if test "$enable_ide" = no; then
     AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
   reason_ide=" (sqlite3 not found)"
   fi
fi

# checking for sqlite3
if test "$enable_bench" = yes ; then
   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

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)
    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.*|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)
                reason_coq_support=" (need version 8.x or later)"
                ;;
        esac
    fi
fi
if test "$enable_coq_support" = yes; then
   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
   if test "$enable_coq_support" = no; then
      reason_coq_support=" ($COQLIB/kernel/term.cmi not found)"
   fi
fi

if test "$CAMLP5O" = no; then
   enable_coq_support=no
   reason_coq_support=" (camlp5o not found)"
fi

# coq-plugin currently disabled
enable_coq_support=no
reason_coq_support=" (not yet implemented)"

# hypothesis_selection

if test "$enable_hypothesis_selection" = yes; then
  AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,,enable_hypothesis_selection=no)
fi

if test "$enable_local" = no; then
   LOCALDIR='None'
else
   LOCALDIR='Some \"$PWD\"'
fi

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

if test "$enable_plugins" = yes; then
  META_DYNLINK="dynlink"
else
  META_DYNLINK=""
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(MENHIR)
AC_SUBST(OCAMLDOC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
dnl AC_SUBST(OCAMLV)
dnl AC_SUBST(FORPACK)
dnl AC_SUBST(OCAMLGRAPHLIB)
dnl AC_SUBST(OCAMLWEB)

AC_SUBST(enable_profiling)

AC_SUBST(CAMLP5O)

AC_SUBST(enable_ide)
AC_SUBST(enable_bench)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)
AC_SUBST(META_DYNLINK)
AC_SUBST(META_OCAMLGRAPH)

AC_SUBST(enable_coq_support)

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

AC_SUBST(enable_whytptp)
AC_SUBST(enable_menhirlib)

AC_SUBST(enable_hypothesis_selection)

AC_SUBST(enable_doc)
AC_SUBST(RUBBER)

AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)

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 META)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/config.sh doc/version.tex;
chmod u+x src/config.sh)

AC_OUTPUT


# 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 $reason_ide"
echo "Why bench tool          : $enable_bench"
echo "Why documentation       : $enable_doc"
echo "Why plugins             : $enable_plugins"
echo "Coq plugin support      : $enable_coq_support $reason_coq_support"
if test "$enable_coq_support" = "yes" ; then
   echo "    Version             : $COQVERSION"
   echo "    Lib                 : $COQLIB"
fi
echo "TPTP parser             : $enable_whytptp"
echo "Menhir library          : $enable_menhirlib"
echo "hypothesis selection    : $enable_hypothesis_selection"
echo "profiling               : $enable_profiling"
echo "localdir                : $enable_local"