#################################################################### # # # The Why3 Verification Platform / The Why3 Development Team # # Copyright 2010-2019 -- 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 ) else if uname -s | grep -q MINGW ; then EXE=.exe STRIP=strip AC_MSG_RESULT(.exe ) else EXE= STRIP=strip AC_MSG_RESULT() 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=zip else 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 lablgtk3 if test "$enable_ide" != yes ; then reason_ide=" (disabled by user)" else DIR= if test "$USEOCAMLFIND" = yes; then DIR=$(ocamlfind query lablgtk3) if test -n "$DIR"; then echo "ocamlfind found lablgtk3 in $DIR" LABLGTKINCLUDE="-I $DIR -I +threads" fi fi if test -z "$DIR"; then LABLGTKINCLUDE="-I +lablgtk3 -I +threads" DIR="$OCAMLLIB/lablgtk3" AC_CHECK_FILE($DIR/lablgtk.cma,,enable_ide=no) fi AC_CHECK_FILE($DIR/gtkButton.cmi,,enable_ide=no) if test "$enable_ide" = yes; then GTKVERSION=3 reason_ide=" (gtk3)" else AC_MSG_WARN([Lib lablgtk3 not found, trying lablgtk2.]) enable_ide=retry fi fi # checking for lablgtk2 if test "$enable_ide" = retry; then enable_ide=yes DIR= if test "$USEOCAMLFIND" = yes; then DIR=$(ocamlfind query lablgtk2) if test -n "$DIR"; then echo "ocamlfind found lablgtk2 in $DIR" LABLGTKINCLUDE="-I $DIR" fi fi if test -z "$DIR"; then LABLGTKINCLUDE="-I +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" = yes; then GTKVERSION=2 reason_ide=" (gtk2)" else AC_MSG_WARN([Lib lablgtk2 not found, IDE disabled.]) reason_ide=" (lablgtk2/3 not found)" fi fi # checking for lablgtksourceview if test "$enable_ide" = yes ; then DIR= if test "$USEOCAMLFIND" = yes; then case $GTKVERSION in 2) LIB_SOURCEVIEW=lablgtksourceview2 PKG_SOURCEVIEW=lablgtk2.sourceview2 DIR=$(ocamlfind query $PKG_SOURCEVIEW) if test -z "$DIR"; then PKG_SOURCEVIEW=lablgtksourceview2 DIR=$(ocamlfind query $PKG_SOURCEVIEW) fi ;; 3) LIB_SOURCEVIEW=lablgtk3_sourceview3 PKG_SOURCEVIEW=lablgtk3-sourceview3 DIR=$(ocamlfind query $PKG_SOURCEVIEW) ;; *) AC_MSG_ERROR(Unknown gtk version $GTKVERSION) ;; esac if test -n "$DIR";then echo "ocamlfind found $PKG_SOURCEVIEW in $DIR" fi fi if test -z "$DIR"; then DIR="$OCAMLLIB/lablgtk$GTKVERSION" AC_CHECK_FILE($DIR/lablgtksourceview$GTKVERSION.cma,,enable_ide=no) fi AC_CHECK_FILE($DIR/gSourceView$GTKVERSION.cmi,,enable_ide=no) if test "$enable_ide" = no; then AC_MSG_WARN([Lib lablgtksourceview not found, IDE disabled.]) reason_ide=" (lablgtksourceview not found)" else LABLGTKINCLUDE="$LABLGTKINCLUDE -I $DIR" fi fi if test "$enable_ide" = yes ; then case $GTKVERSION in 2) LABLGTKLIB="lablgtk" ;; 3) LABLGTKLIB="threads lablgtk3" ;; *) AC_MSG_ERROR(Unknown gtk version $GTKVERSION) ;; esac LABLGTKLIB="$LABLGTKLIB $LIB_SOURCEVIEW" LABLGTKPKG="lablgtk$GTKVERSION lablgtk$GTKVERSION.init $PKG_SOURCEVIEW" else LABLGTKLIB= LABLGTKPKG= LABLGTKINCLUDE= 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)" else JSOFOCAMLPKG="js_of_ocaml js_of_ocaml.ppx" 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=" (Javascript support 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" ;; 8.9*) coq_compat_version="COQ89" ;; *) 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.Version BinNat." \ "Goal (30100 <= 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 >= 3.1 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=2018 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 2018*) enable_isabelle_support=yes ISABELLEVERSION=2018 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 2017 or later; Isabelle discarded) reason_isabelle_support=" (need version >= 2017)" ;; 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(LABLGTKLIB) AC_SUBST(LABLGTKPKG) AC_SUBST(LABLGTKINCLUDE) AC_SUBST(GTKVERSION) AC_SUBST(enable_web_ide) AC_SUBST(enable_js_of_ocaml) AC_SUBST(JSOFOCAMLPKG) 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