########################################################################## # # # The Why/Caduceus/Krakatoa tool suite for program certification # # Copyright (C) 2002-2006 # # Jean-François COUCHOT # # Mehdi DOGGUY # # Jean-Christophe FILLIÂTRE # # Thierry HUBERT # # Claude MARCHÉ # # Yannick MOY # # # # This software is free software; you can redistribute it and/or # # modify it under the terms of the GNU General Public # # License version 2, as published by the Free Software Foundation. # # # # 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. # # # # See the GNU General Public License version 2 for more details # # (enclosed in the file GPL). # # # ########################################################################## # # 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). # 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 either "byte" if no native compiler was found, # or "opt" otherwise # OCAMLDEP "ocamldep" # OCAMLLEX "ocamllex" # OCAMLYACC "ocamlyac" # OCAMLLIB the path to the ocaml standard library # OCAMLVERSION the ocaml version number # LABLGTK2 "yes" is available, "no" otherwise # OCAMLWEB "ocamlweb" (not mandatory) # check for one particular file of the sources # ADAPT THE FOLLOWING LINE TO YOUR SOURCES! AC_INIT(src/monad.mli) # verbosemake feature AC_ARG_ENABLE(verbosemake,[ --enable-verbosemake verbose makefile commands],VERBOSEMAKE=yes,VERBOSEMAKE=no) if test "$VERBOSEMAKE" = yes ; then AC_MSG_RESULT(Make will be verbose.) fi # Check for arch/OS AC_MSG_CHECKING(executable suffix) if uname -s | grep -q CYGWIN ; then EXE=.exe AC_MSG_RESULT(.exe) else EXE= AC_MSG_RESULT() 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 and library path OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` echo "ocaml version is $OCAMLVERSION" OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d " "` echo "ocaml library path is $OCAMLLIB" case $OCAMLVERSION in 0.*|1.*|2.00|3.00*|3.01*|3.02*|3.03*|3.04*|3.05*|3.06*|3.07*) AC_MSG_ERROR(You need Objective 3.08 or later);; 3.08.2) FORPACK="" OCAMLV=3082;; 3.08*) FORPACK="" OCAMLV=308;; *) FORPACK="-for-pack Graph";; esac # 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.) 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 #looking for ocamlgraph library AC_CHECK_FILE($OCAMLLIB/graph.cmi,OCAMLGRAPH=yes,OCAMLGRAPH=no) if test "$OCAMLGRAPH" = no ; then AC_CHECK_FILE($OCAMLLIB/ocamlgraph/graph.cmi,OCAMLGRAPH=yes,OCAMLGRAPH=no) if test "$OCAMLGRAPH" = no ; then AC_CHECK_FILE(ocamlgraph/sig.mli,OCAMLGRAPH=yes,OCAMLGRAPH=no) if test "$OCAMLGRAPH" = no ; then AC_MSG_ERROR(Cannot find ocamlgraph library. Please install the *libocamlgraph-ocaml-dev* Debian package - or use the GODI caml package system *http://godi.ocaml-programming.de/* - or compile from sources *http://ocamlgraph.lri.fr/*) else OCAMLGRAPHLIB="-I ocamlgraph" OCAMLGRAPHVER=" in local subdir ocamlgraph" AC_MSG_CHECKING(ocamlgraph compilation) if (cd ocamlgraph; ./configure && make) > /dev/null 2>&1; then AC_MSG_RESULT(ok) else AC_MSG_ERROR(cannot compile ocamlgraph in ocamlgraph) fi fi else OCAMLGRAPHLIB="-I +ocamlgraph" OCAMLGRAPHVER=" in Ocaml lib, subdir ocamlgraph" fi else OCAMLGRAPHLIB="" OCAMLGRAPHVER=" in Ocaml lib, main dir" fi # checking ocamlgraph version AC_MSG_CHECKING(ocamlgraph version) if $OCAMLC $OCAMLGRAPHLIB graph.cma config/check_ocamlgraph.ml > /dev/null 2>&1; then AC_MSG_RESULT(ok) OCAMLGRAPHVER="0.99"$OCAMLGRAPHVER else AC_MSG_ERROR(OcamlGraph$OCAMLGRAPHVER is too old. You need ocamlgraph 0.99 or higher; you may need to compile from sources *http://ocamlgraph.lri.fr/*) fi # checking for lablgtk2 AC_CHECK_PROG(LABLGTK2,lablgtk2,yes,no) if test "$LABLGTK2" = yes ; then if test -d "$OCAMLLIB/lablgtk2" ; then INCLUDEGTK2="-I +lablgtk2" else LABLGTK2=no fi fi AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true) # Octagon library default_octagon=no AC_ARG_ENABLE(octagon,[ --enable-octagon=[no/yes] using abstract interpretation [default=$default_octagon]],,enable_octagon=$default_octagon) if test "$enable_octagon" = "yes" ; then cd octagon ./configure --with-num=float --with-ocaml=$OCAMLLIB if test $? -ne 0; then AC_MSG_ERROR(Problem with octagon configuration (did you install g++ ?)) fi chmod 755 oct-config cd .. OCTAGONLIB=octagon/ocamllib/oct.cma STATIC="-cclib -static" else OCTAGONLIB= STATIC= fi # camlp4 AC_CHECK_PROG(CAMLP4O,camlp4o,camlp4o,no) if test "$CAMLP4O" = no ; then AC_MSG_ERROR(Cannot find camlp4o.) fi CAMLP4LIB=`camlp4o -where` CAMLP4VERSION=`$CAMLP4O -v 2>&1 | sed -n -e 's|.*version *\(.*\)$|\1|p'` AC_MSG_CHECKING(camlp4 version) if test "$CAMLP4VERSION" != "$OCAMLVERSION" ; then AC_MSG_ERROR(differs from ocaml version) else AC_MSG_RESULT(ok) fi AC_CHECK_PROG(CAMLP4OOPT,camlp4o.opt,camlp4o.opt,no) if test "CAMLP4OOPT" != no ; then AC_MSG_CHECKING(camlp4o.opt version) TMPVERSION=`$CAMLP4OOPT -v 2>&1 |sed -n -e 's|.*version *\(.*\)$|\1|p'` if test "$TMPVERSION" != $CAMLP4VERSION ; then AC_MSG_RESULT(differs from camlp4o; camlp4o.opt discarded.) else AC_MSG_RESULT(ok) CAMLP4O=$CAMLP4OOPT fi fi WHYFLOATS= # Coq AC_CHECK_PROG(COQC,coqc,coqc,no) if test "$COQC" = no ; then COQ=no AC_MSG_WARN(Cannot find coqc.) else COQ=yes AC_CHECK_PROG(COQDEP,coqdep,coqdep,true) if test "$COQDEP" = true ; then AC_MSG_ERROR(Cannot find coqdep.) fi COQLIB=`coqc -where` AC_MSG_CHECKING(Coq version) COQVERSION=`coqc -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' ` case $COQVERSION in # 7.3.1) # AC_MSG_RESULT($COQVERSION) # COQC7=$COQC # COQVER=v7 # WHYLIBCOQ=lib/coq-v7 # cp -f lib/coq-v7/WhyCoq73.v lib/coq-v7/WhyCoqCompat.v;; # 7.3.1*|7.4*) 7.4*) AC_MSG_RESULT($COQVERSION) COQC7=$COQC COQVER=v7 WHYLIBCOQ=lib/coq-v7 cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v;; 8.*|trunk) AC_MSG_RESULT($COQVERSION) COQC7="$COQC -v7" COQC8=$COQC COQVER=v8 WHYLIBCOQ=lib/coq cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v case $COQVERSION in 8.1*|trunk) JESSIELIBCOQ=lib/coq/jessie_why.vo cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v;; *) JESSIELIBCOQ= cp -f lib/coq/WhyCoq8.v lib/coq/WhyCoqCompat.v;; esac AC_MSG_CHECKING(Coq floating-point library) if test -f $COQLIB/user-contrib/AllFloat.vo; then AC_MSG_RESULT(yes) WHYFLOATS=lib/coq/WhyFloats.vo else AC_MSG_RESULT(no) fi;; *) COQ=no AC_MSG_WARN(You need Coq 7.4 or later; Coq discarded);; esac fi # PVS AC_CHECK_PROG(PVSC,pvs,pvs,no,,/sbin/pvs) if test "$PVSC" = no ; then PVS=no AC_MSG_WARN(Cannot find PVS.) else PVS=yes PVSFILE=`which pvs` PVSLIB=`sed -n -e "s/PVSPATH=\(.*\)/\1/p" $PVSFILE`/lib if test "$PVSLIB" = /lib; then PVS=no; fi fi # Mizar AC_CHECK_PROG(MIZF,mizf,mizf,no) if test "$MIZF" = no; then MIZAR=no AC_MSG_WARN(Cannot find Mizar.) else MIZAR=yes AC_MSG_CHECKING(Mizar library) if test -d "$MIZFILES"; then MIZARLIB=$MIZFILES AC_MSG_RESULT($MIZARLIB) else if test -d /usr/local/lib/mizar; then MIZARLIB=$MIZFILES AC_MSG_RESULT($MIZARLIB) else AC_MSG_WARN(Cannot find Mizar library; please set \$MIZFILES) MIZAR=no fi fi fi # substitutions to perform AC_SUBST(VERBOSEMAKE) AC_SUBST(EXE) AC_SUBST(OCAMLC) AC_SUBST(OCAMLOPT) AC_SUBST(OCAMLDEP) AC_SUBST(OCAMLLEX) AC_SUBST(OCAMLYACC) AC_SUBST(OCAMLBEST) AC_SUBST(OCAMLVERSION) AC_SUBST(OCAMLV) AC_SUBST(OCAMLLIB) AC_SUBST(OCAMLGRAPHLIB) AC_SUBST(LABLGTK2) AC_SUBST(INCLUDEGTK2) AC_SUBST(OCAMLWEB) # AC_SUBST(CAMLP4O) # AC_SUBST(CAMLP4LIB) AC_SUBST(enable_octagon) AC_SUBST(OCTAGONLIB) AC_SUBST(STATIC) AC_SUBST(COQ) AC_SUBST(COQC7) AC_SUBST(COQC8) AC_SUBST(COQDEP) AC_SUBST(COQLIB) AC_SUBST(COQVER) AC_SUBST(WHYLIBCOQ) AC_SUBST(WHYFLOATS) AC_SUBST(JESSIELIBCOQ) AC_SUBST(PVS) AC_SUBST(PVSC) AC_SUBST(PVSLIB) AC_SUBST(MIZAR) AC_SUBST(MIZF) AC_SUBST(MIZARLIB) AC_SUBST(FORPACK) # Finally create the Makefile from Makefile.in AC_OUTPUT(Makefile bench/bench) chmod a-w Makefile bench/bench chmod a+x bench/bench # Summary echo echo " Summary" echo "-----------------------------------------" echo "OCaml version : $OCAMLVERSION" echo "OCaml library path : $OCAMLLIB" echo "OcamlGraph lib : $OCAMLGRAPHVER" echo "Verbose make : $VERBOSEMAKE" echo "Abstract interpretation : $enable_octagon" echo "GWhy : $LABLGTK2" echo "Coq support : $COQ" if test "$COQ" = "yes" ; then echo " Version : $COQVER ($COQVERSION)" if test "$JESSIELIBCOQ" = ""; then echo " : (Jessie Coq proofs disabled, requires >= 8.1)" fi echo " Lib : $COQLIB" echo " Floats : ${WHYFLOATS:-no}" fi echo "PVS support : $PVS" if test "$PVS" = "yes" ; then echo " Lib : $PVSLIB" fi echo "Mizar support : $MIZAR"