Select Git revision
configure.in 27.98 KiB
####################################################################
# #
# 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)
# WHY3LIB
AC_ARG_ENABLE(why3-lib,
AS_HELP_STRING([--disable-why3-lib], [use an already installed Why3]),,
enable_why3_lib=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([--disable-zip], [do not use LZ compression to store session files]),, enable_zip=yes)
# js_of_ocaml
AC_ARG_ENABLE(js_of_ocaml,
AS_HELP_STRING([--disable-js-of-ocaml], [do not use js-of-ocaml]),,
enable_js_of_ocaml=yes)
# IDE
AC_ARG_ENABLE(ide,
AS_HELP_STRING([--disable-ide], [do not build Why3 IDE]),,
enable_ide=yes)
AC_ARG_ENABLE(web_ide,
AS_HELP_STRING([--disable-web-ide], [do not build Why3 Web IDE]),,
enable_web_ide=yes)
# Coq libraries
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
AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
# 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"
AX_VERSION_GE([$OCAMLVERSION], 4.02.3, [],
[AC_MSG_ERROR(You need Objective Caml 4.02.3 or higher.)])
# 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(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
AC_MSG_ERROR(Cannot find menhir.)
fi
MENHIRVERSION=`$MENHIR --version | sed -n -e 's,.*version *\(.*\)$,\1,p'`
AX_VERSION_GE([$MENHIRVERSION], 20151112, [],
[AC_MSG_ERROR(You need Menhir 20151112 or higher.)])
## 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_why3_lib" = yes ; then
WHY3LIB=
WHY3INCLUDE="-I lib/why3"
else
AC_MSG_CHECKING([For Why3])
if test "$USEOCAMLFIND" = no; then
AC_MSG_RESULT([no])
AC_MSG_ERROR([Cannot use --disable-why3-lib without ocamlfind.])
fi
WHY3LIB=why3
WHY3INCLUDE=$(ocamlfind query why3)
if test -n "$WHY3INCLUDE"; then
AC_MSG_RESULT([$WHY3INCLUDE])
WHY3INCLUDE="-I $WHY3INCLUDE"
else
AC_MSG_RESULT([no])
AC_MSG_ERROR([Cannot use --disable-why3-lib without an installed Why3.])
fi
fi
if test "$enable_local" = no; then
LOCALDIR=''
else
LOCALDIR="${PWD}"
fi
#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
# compiler plugins
AX_VERSION_GE([$OCAMLVERSION], 4.05.0,
[if test "$USEOCAMLFIND" = yes; then
COMPILERLIBS=$(ocamlfind query compiler-libs)
fi
if test -n "$COMPILERLIBS"; then
echo "ocamlfind found compiler-libs in $COMPILERLIBS" enable_compiler_plugins="yes"
else
COMPILERLIBS="+compiler-libs"
AC_CHECK_FILE($OCAMLLIB/compiler-libs/,
enable_compiler_plugins=yes,
enable_compiler_plugins=no)
if test "$enable_compiler_plugins" = no; then
reason_compiler_plugins=" (compiler-libs not found)"
fi
fi],
[enable_compiler_plugins="no"
reason_compiler_plugins=" (Ocaml version 4.05.0 required)"])
if test "$enable_compiler_plugins" = yes; then
COMPILERLIBSPKG="compiler-libs"
else
COMPILERLIBSPKG=
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
# (ocamlfind cannot be trusted here, since the default installation path is $OCAMLLIB)
found_num=no
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query num)
if test -n "$DIR"; then
echo "ocamlfind found num in $DIR"
NUMINCLUDE="-I $DIR"
found_num=yes AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
fi
fi
if test "$found_num" = no; then
DIR="$OCAMLLIB"
NUMINCLUDE=
found_num=yes
AC_CHECK_FILE($DIR/nums.cma,,found_num=no)
AC_CHECK_FILE($DIR/num.cmi,,found_num=no)
fi
if test "$found_num" = no; then
AC_MSG_ERROR([Library Num not found.])
fi
# checking for Zarith
if test "$enable_zarith" = yes; then
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query zarith)
if test -n "$DIR"; then
echo "ocamlfind found zarith in $DIR"
BIGINTINCLUDE="-I $DIR"
fi
fi
if test -z "$DIR"; then
BIGINTINCLUDE="-I +zarith"
DIR="$OCAMLLIB/zarith"
AC_CHECK_FILE($DIR/zarith.cma,,enable_zarith=no)
fi
AC_CHECK_FILE($DIR/z.cmi,,enable_zarith=no)
if test "$enable_zarith" = no; then
AC_MSG_WARN([Lib Zarith not found, using Nums instead.])
reason_zarith=" (zarith not found)"
fi
fi
if test "$enable_zarith" = yes; then
BIGINTLIB=zarith
BIGINTPKG=zarith
else
BIGINTLIB=nums
BIGINTPKG=num
BIGINTINCLUDE="$NUMINCLUDE"
fi
# checking for camlzip
if test "$enable_zip" = yes; then
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query zip)
if test -n "DIR"; then
echo "ocamlfind found camlzip in $DIR"
ZIPINCLUDE="-I $DIR"
fi
fi
if test -z "$DIR"; then
ZIPINCLUDE="-I +zip"
DIR="$OCAMLLIB/zip"
AC_CHECK_FILE($DIR/zip.cma,,enable_zip=no)
fi
AC_CHECK_FILE($DIR/zip.cmi,,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)"
fi
fi
if test "$enable_zip" = yes; then
ZIPLIB=zipelse
ZIPLIB=
ZIPINCLUDE=
fi
# checking for menhirlib
found_menhirlib=yes
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query menhirLib)
if test -n "$DIR"; then
echo "ocamlfind found menhirLib in $DIR"
MENHIRINCLUDE="-I $DIR"
fi
fi
if test -z "$DIR"; then
MENHIRINCLUDE="-I +menhirLib"
DIR="$OCAMLLIB/menhirLib"
AC_CHECK_FILE($DIR/menhirLib.cmx,,found_menhirlib=no)
fi
AC_CHECK_FILE($DIR/menhirLib.cmi,,found_menhirlib=no)
if test "$found_menhirlib" = no; then
AC_MSG_ERROR([Library menhirLib not found.])
fi
# checking for lablgtk2
if test "$enable_ide" != yes ; then
reason_ide=" (disabled by user)"
else
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query lablgtk2)
if test -n "$DIR"; then
echo "ocamlfind found lablgtk2 in $DIR"
LABLGTK2LIB="$DIR"
fi
fi
if test -z "$DIR"; then
LABLGTK2LIB="+lablgtk2"
DIR="$OCAMLLIB/lablgtk2"
AC_CHECK_FILE($DIR/lablgtk.cma,,enable_ide=no)
fi
AC_CHECK_FILE($DIR/gtkButton.cmi,,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
# checking for lablgtksourceview2
if test "$enable_ide" = yes ; then
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query lablgtk2.sourceview2)
if test -z "$DIR"; then
DIR=$(ocamlfind query lablgtksourceview2)
fi
if test -n "$DIR";then
echo "ocamlfind found lablgtksourceview2 in $DIR"
LABLGTKSV2LIB="$DIR"
fi
fi
if test -z "$DIR"; then
DIR="$OCAMLLIB/lablgtk2"
AC_CHECK_FILE($DIR/lablgtksourceview2.cma,,enable_ide=no)
fi
AC_CHECK_FILE($DIR/gSourceView2.cmi,,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
if test "$enable_ide" = yes ; then
LABLGTK2PKG="lablgtk2 lablgtk2.init lablgtk2.sourceview2"
else
LABLGTK2PKG=
LABLGTK2LIB=
fi
dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# checking for ocamlgraph
if test "$enable_hypothesis_selection" = yes; then
DIR=
if test "$USEOCAMLFIND" = yes; then
DIR=$(ocamlfind query ocamlgraph)
if test -n "$DIR"; then
echo "ocamlfind found ocamlgraph in $DIR"
OCAMLGRAPHLIB="$DIR"
fi
fi
if test -z "$DIR"; then
OCAMLGRAPHLIB="+ocamlgraph"
DIR="$OCAMLLIB/ocamlgraph"
AC_CHECK_FILE($DIR/graph.cma,,enable_hypothesis_selection=no)
fi
AC_CHECK_FILE($DIR/graph.cmi,,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
if test "$enable_hypothesis_selection" = yes; then
META_OCAMLGRAPH="ocamlgraph"
else
META_OCAMLGRAPH=
OCAMLGRAPHLIB=
fi
# checking for js_of_ocaml
if test "$enable_js_of_ocaml" != yes; then
reason_js_of_ocaml=" (disabled by user)"
elif test "$USEOCAMLFIND" != yes; then
enable_js_of_ocaml=no
reason_js_of_ocaml=" (ocamlfind not available)"
else
JSOFOCAML=$(ocamlfind query js_of_ocaml)
if test -z "$JSOFOCAML"; then
enable_js_of_ocaml=no
reason_js_of_ocaml=" (js_of_ocaml not found)"
else
JSOFOCAMLPPX=$(ocamlfind query js_of_ocaml-ppx)
if test -z "$JSOFOCAMLPPX"; then
enable_js_of_ocaml=no
reason_js_of_ocaml=" (js_of_ocaml-ppx not found)"
fi
fi
fi
if test "$enable_web_ide" != yes; then
reason_web_ide=" (disabled by user)"
elif test "$enable_js_of_ocaml" != yes; then
enable_web_ide=no
reason_web_ide=" (js_of_ocaml not available)"
fi
# Coq
enable_coq_support=yes
enable_coq_fp_libs=yes
coq_compat_version=
if test "$enable_coq_libs" = no; then
enable_coq_support=no
reason_coq_support=" (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'`]
AC_MSG_RESULT($COQVERSION)
case $COQVERSION in
8.5*)
coq_compat_version="COQ85"
;;
8.6*)
coq_compat_version="COQ86"
;;
8.7*)
coq_compat_version="COQ87"
;;
8.8*)
coq_compat_version="COQ88"
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.5 or later; Coq discarded)
reason_coq_support=" (version is $COQVERSION but need version 8.5 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_libs=no
COQVERSION=
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
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
#check frama-c
FRAMAC_SUPPORTED=Sulfur
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: \)\?\(.*\)$|\2|p'`
AC_MSG_RESULT($FRAMAC_VERSION)
case $FRAMAC_VERSION in
$FRAMAC_SUPPORTED-*) ;;
*) AC_MSG_WARN(Version $FRAMAC_SUPPORTED required.)
enable_frama_c=no
reason_frama_c=" (version $FRAMAC_SUPPORTED required)"
;;
esac
fi
fi
if test "$enable_frama_c" = yes; then
FRAMAC_SHARE=`$FRAMAC -print-path`
FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
FRAMAC_INCLUDE="-I $FRAMAC_LIBDIR"
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(enable_ide)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(LABLGTK2PKG)
AC_SUBST(enable_web_ide)
AC_SUBST(enable_js_of_ocaml)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(enable_compiler_plugins)
AC_SUBST(COMPILERLIBS)
AC_SUBST(COMPILERLIBSPKG)
AC_SUBST(NUMINCLUDE)
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(MENHIRINCLUDE)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_fp_libs)
AC_SUBST(coq_compat_version)
AC_SUBST(COQC)
AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(enable_pvs_libs)
AC_SUBST(PVS)
AC_SUBST(PVSVERSION)
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(FRAMAC_INCLUDE)
AC_SUBST(enable_local)
AC_SUBST(LOCALDIR)
AC_SUBST(enable_why3_lib)
AC_SUBST(WHY3LIB)
AC_SUBST(WHY3INCLUDE)
AC_SUBST(enable_relocation)
dnl AC_SUBST(PSVIEWER)
dnl AC_SUBST(PDFVIEWER)
# Finally create the Makefile from Makefile.in
AC_CONFIG_FILES(Makefile)
AC_CONFIG_FILES(src/config.sh doc/version.tex)
AC_CONFIG_FILES(lib/why3/META)
AC_CONFIG_FILES(.merlin)
AC_CONFIG_FILES(src/jessie/Makefile)
AC_CONFIG_FILES(src/jessie/.merlin)
AC_CONFIG_FILES(lib/coq/version lib/pvs/version)
AC_CONFIG_COMMANDS([chmod],
chmod a-w Makefile src/jessie/Makefile;
chmod a-w src/config.sh doc/version.tex;
chmod a-w lib/why3/META;
chmod a-w .merlin;
chmod a-w src/jessie/Makefile;
chmod a-w src/jessie/.merlin;
chmod a-w lib/coq/version lib/pvs/version;
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 " Compiler plugins : $enable_compiler_plugins$reason_compiler_plugins"
echo " Javascript support : $enable_js_of_ocaml$reason_js_of_ocaml"
echo "Components"
echo " Why3 library : $enable_why3_lib"
echo " GTK IDE : $enable_ide$reason_ide"
echo " Web IDE : $enable_web_ide$reason_web_ide"
echo " GMP arithmetic : $enable_zarith$reason_zarith"
echo " Compressed sessions : $enable_zip$reason_zip"
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 " 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"
echo " OCaml library path : $OCAMLINSTALLLIB/why3"
else
echo "Installable : yes"
echo " Binary path : $bindir"
echo " Library path : $libdir/why3"
echo " Data path : $datarootdir/why3"
echo " OCaml library path : $OCAMLINSTALLLIB/why3"
echo " Relocatable : $enable_relocation"
fi