########################################################################## # # # 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 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/) # 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 STRIP='echo "no strip "' CPULIMIT=cpulimit-win AC_MSG_RESULT(.exe) else EXE= STRIP=strip CPULIMIT=cpulimit 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 OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *$.*$$|\1|p' ` echo "ocaml version is $OCAMLVERSION" 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 # 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 #looking for ocamlgraph library LOCALOCAMLGRAPH=no 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/src/sig.mli,OCAMLGRAPH=yes,OCAMLGRAPH=no) if test "$OCAMLGRAPH" = no ; then AC_MSG_WARN(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" LOCALOCAMLGRAPH=yes fi else OCAMLGRAPHLIB="-I +ocamlgraph" OCAMLGRAPHVER=" in Ocaml lib, subdir ocamlgraph" fi else OCAMLGRAPHLIB="" OCAMLGRAPHVER=" in Ocaml lib, main dir" fi # checking ocamlgraph version dnl AC_MSG_CHECKING(ocamlgraph version) dnl if $OCAMLC $OCAMLGRAPHLIB graph.cma config/check_ocamlgraph.ml > /dev/null 2>&1 && (test "$OCAMLBEST" = "byte" || $OCAMLOPT $OCAMLGRAPHLIB graph.cmxa config/check_ocamlgraph.ml > /dev/null 2>&1); then dnl AC_MSG_RESULT(ok) dnl OCAMLGRAPHVER="0.99"$OCAMLGRAPHVER dnl else dnl AC_MSG_RESULT(failed) dnl if test -d ocamlgraph; then dnl AC_MSG_RESULT(Switching to local ocamlgraph) dnl OCAMLGRAPHLIB="-I ocamlgraph" dnl OCAMLGRAPHVER=" in local subdir ocamlgraph" dnl LOCALOCAMLGRAPH=yes dnl else dnl AC_MSG_ERROR(You need ocamlgraph 0.99b or higher; you may need to compile from sources *http://ocamlgraph.lri.fr/*) dnl fi dnl fi dnl rm -f config/check_ocamlgraph.cmo config/check_ocamlgraph.cmi config/check_ocamlgraph.cmx config/check_ocamlgraph$EXE dnl # checking local ocamlgraph compilation dnl if test "$LOCALOCAMLGRAPH" = yes; then dnl AC_MSG_CHECKING(ocamlgraph compilation) dnl if (cd ocamlgraph; ./configure && make) > /dev/null 2>&1; then dnl AC_MSG_RESULT(ok) dnl else dnl AC_MSG_ERROR(cannot compile ocamlgraph in ocamlgraph) dnl fi dnl fi # checking for lablgtk2 AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,LABLGTK2=yes,LABLGTK2=no) # AC_CHECK_PROG(LABLGTK2,lablgtk2,yes,no) not always available (Win32) if test "$LABLGTK2" = yes ; then INCLUDEGTK2="-I +lablgtk2" fi AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true) # apron library default_apron=no APRONLIBS= AC_ARG_ENABLE(apron,[ --enable-apron=[no/yes] use APRON library for abstract interpretation [default=$default_apron]],,enable_apron=$default_apron) if test "$enable_apron" = "yes" ; then AC_CHECK_FILE(/usr/local/lib/apron.cmxa,APRONLIB="-I /usr/local/lib -I /usr/lib",APRONLIB=no) if test "$APRONLIB" = no ; then AC_CHECK_FILE(/usr/lib/apron.cmxa,APRONLIB="-I /usr/lib -I /usr/local/lib",APRONLIB=no) if test "$APRONLIB" = no ; then AC_MSG_ERROR(Cannot find APRON library.) fi fi APRONLIBS="-cclib ' -lpolka_caml -lpolkaMPQ -loct_caml -loctMPQ -lbox_caml -lboxMPQ -lapron_caml -lapron -lgmp_caml -lmpfr -lgmp -lbigarray -lcamlidl' bigarray.cmxa gmp.cmxa apron.cmxa box.cmxa polka.cmxa" ATPCMO=atp/atp.cmo fi # Frama-C AC_CHECK_PROG(FRAMAC,frama-c,yes,no) # 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 dnl AC_CHECK_PROG(CAMLP4OOPT,camlp4o.opt,camlp4o.opt,no) dnl if test "CAMLP4OOPT" != no ; then dnl AC_MSG_CHECKING(camlp4o.opt version) dnl TMPVERSION=`$CAMLP4OOPT -v 2>&1 |sed -n -e 's|.*version *$.*$$|\1|p'` dnl if test "$TMPVERSION" != $CAMLP4VERSION ; then dnl AC_MSG_RESULT(differs from camlp4o; camlp4o.opt discarded.) dnl else dnl AC_MSG_RESULT(ok) dnl CAMLP4O=$CAMLP4OOPT dnl fi dnl 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 | 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 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*|8.2*|trunk) JESSIELIBCOQ=lib/coq/jessie_why.vo cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v COQVER=v8.1 ;; *) JESSIELIBCOQ= cp -f lib/coq/WhyCoq8.v lib/coq/WhyCoqCompat.v;; esac AC_MSG_CHECKING(Coq floating-point library) case $COQVERSION in 8.2*|trunk) if test -f "$COQLIB/user-contrib/AllFloat.vo"; then AC_MSG_RESULT(yes) WHYFLOATS="lib/coq/WhyFloats.vo lib/coq/JessieFloats.vo" COQFLOATSMSG=yes else AC_MSG_RESULT(no) COQFLOATSMSG="no (Coq library AllFloat.vo not found)" fi AC_MSG_CHECKING(Coq Gappa library) if test -f "$COQLIB/user-contrib/Gappa/Gappa_tactic.vo"; then AC_MSG_RESULT(yes) WHYFLOATS="$WHYFLOATS lib/coq/JessieGappa.vo" COQGAPPAMSG=yes else AC_MSG_RESULT(no) COQGAPPAMSG="no (Coq library Gappa_tactic.vo not found)" fi ;; *) COQFLOATSMSG="no (requires Coq version >= 8.2)" COQGAPPAMSG="no (requires Coq version >= 8.2)" ;; esac ;; *) COQ=no AC_MSG_WARN(You need Coq 7.4 or later; Coq discarded);; esac fi # Alt-ergo dnl AC_CHECK_PROG(ALTERGO,alt-ergo,alt-ergo,no) dnl if test "$ALTERGO" = no ; then dnl AC_CHECK_PROG(ERGO,ergo,ergo,no) dnl if test "$ERGO" = no ; then dnl ERGOBIN=alt-ergo dnl else dnl ERGOBIN=ergo dnl fi dnl else dnl ERGOBIN=alt-ergo dnl fi # PVS AC_PATH_PROG(PVSC,pvs,no) if test "$PVSC" = no ; then PVS=no AC_MSG_WARN(Cannot find PVS.) else PVS=yes PVSLIB=`pvs -where`/lib if test "$PVSLIB" = /lib; then AC_MSG_WARN(PVS found but pvs -where did not work) 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 #Viewer for ps and pdf AC_CHECK_PROGS(PSVIEWER,gv evince) AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince) # substitutions to perform AC_SUBST(VERBOSEMAKE) 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(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_apron) AC_SUBST(APRONLIB) AC_SUBST(APRONLIBS) AC_SUBST(FRAMAC) AC_SUBST(ATPCMO) 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(ERGOBIN) AC_SUBST(PVS) AC_SUBST(PVSC) AC_SUBST(PVSLIB) AC_SUBST(MIZAR) AC_SUBST(MIZF) AC_SUBST(MIZARLIB) AC_SUBST(FORPACK) AC_SUBST(PSVIEWER) AC_SUBST(PDFVIEWER) # Finally create the Makefile from Makefile.in dnl AC_OUTPUT(Makefile) AC_OUTPUT(Makefile bench/bench) chmod a-w Makefile 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_apron" echo "Frama-C plugin : $FRAMAC" if test "$enable_apron" = "yes" ; then echo " APRON lib : $APRONLIB" fi 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 : $COQFLOATSMSG" echo " Gappa : $COQGAPPAMSG" fi # echo "Alt-ergo binary : $ERGOBIN" echo "PVS support : $PVS" if test "$PVS" = "yes" ; then echo " Bin : $PVSC" echo " Lib : $PVSLIB" fi echo "Mizar support : $MIZAR"