Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Branch: master
Fetching contributors…

Cannot retrieve contributors at this time

270 lines (238 sloc) 9.032 kB
#****************************************************************************#
# The Alt-Ergo theorem prover #
# Copyright (C) 2006-2013 #
# CNRS - INRIA - Universite Paris Sud #
# #
# Sylvain Conchon #
# Evelyne Contejean #
# #
# Francois Bobot #
# Mohamed Iguernelala #
# Stephane Lescuyer #
# Alain Mebsout #
# #
# This file is distributed under the terms of the CeCILL-C licence #
#****************************************************************************#
#
# 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" (or "ocamllex.opt" if present)
# OCAMLYACC "ocamlyac"
# OCAMLLIB the path to the ocaml standard library
# OCAMLVERSION the ocaml version number
# OCAMLWEB "ocamlweb" (not mandatory)
# OCAMLWIN32 "yes"/"no" depending on Sys.os_type = "Win32"
# EXE ".exe" if OCAMLWIN32=yes, "" otherwise
# check for one particular file of the sources
# ADAPT THE FOLLOWING LINE TO YOUR SOURCES!
AC_INIT(src/main/frontend.ml)
# Check for Ocaml compilers
# we first look for ocamlc in the path; if not present, we fail
AC_CHECK_PROGS(OCAMLC,ocp-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 " " | tr -d '\\r'`
echo "ocaml library path is $OCAMLLIB"
SMTPRELUDE="/usr/local/lib/ergo/smt_prelude.mlw"
case $OCAMLVERSION in
3.10.1+rc1)
AC_MSG_ERROR(Alt-Ergo does not compile with this version of Ocaml);;
esac
# 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
#looking for ocamlgraph library
if test "$USEOCAMLFIND" = yes; then
OCAMLGRAPHLIB=$(ocamlfind query -i-format ocamlgraph)
fi
if test -n "$OCAMLGRAPHLIB";then
echo "ocamlfind found ocamlgraph in $OCAMLGRAPHLIB"
OCAMLGRAPH=yes
else
AC_CHECK_FILE($OCAMLLIB/ocamlgraph/graph.cmi,OCAMLGRAPH=yes,OCAMLGRAPH=no)
if test "$OCAMLGRAPH" = no ; then
AC_CHECK_FILE($OCAMLLIB/graph.cmi,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=""
fi
else
OCAMLGRAPHLIB="-I +ocamlgraph"
fi
fi
#looking for zarith library
if test "$USEOCAMLFIND" = yes; then
ZARITHLIB=$(ocamlfind query -i-format zarith)
fi
if test -n "$ZARITHLIB";then
echo "ocamlfind found zarith in $ZARITHLIB"
ZARITH=yes
else
AC_CHECK_FILE($OCAMLLIB/zarith/zarith.cma,ZARITH=yes,ZARITH=no)
if test "$ZARITH" = no ; then
AC_CHECK_FILE($OCAMLLIB/zarith.cma,ZARITH=yes,ZARITH=no)
if test "$ZARITH" = no ; then
AC_MSG_ERROR(Cannot find zarith library.)
else
ZARITHLIB=""
fi
else
ZARITHLIB="-I +zarith"
fi
fi
# 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_PROGS(OCAMLOPT,ocp-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_PROGS(OCAMLCDOTOPT,ocp-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_PROGS(OCAMLOPTDOTOPT,ocp-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
# checking for lablgtk2
dnl AC_CHECK_PROG(LABLGTK2,lablgtksourceview2,yes,no)
dnl if test "$LABLGTK2" = yes ; then
dnl if test -e "$OCAMLLIB/lablgtk2/lablgtksourceview2.cmxa" ; then
dnl LABLGTK2LIB="-I +lablgtk2"
dnl else
dnl LABLGTK2LIB
dnl fi
dnl fi
if test "$USEOCAMLFIND" = yes; then
LABLGTK2LIB=$(ocamlfind query -i-format lablgtk2.sourceview2)
fi
if test -n "$LABLGTK2LIB";then
echo "ocamlfind found lablgtk2.sourceview2 in $LABLGTK2LIB"
LABLGTK2=yes
ENABLEGUI="yes"
else
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,LABLGTK2=yes,LABLGTK2=no)
if test "$LABLGTK2" = no ; then
AC_MSG_RESULT(Will not be able to compile GUI. Please install the *liblablgtksourceview2-ocaml-dev* Debian package - or use the GODI caml package system *http://godi.ocaml-programming.de/* - or compile from sources *http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html*)
else
LABLGTK2LIB="-I +lablgtk2"
ENABLEGUI="yes"
fi
fi
#When LABLGTK2 is used threads is needed
if test -n "$LABLGTK2LIB";then
LABLGTK2LIB="$LABLGTK2LIB -I +threads"
fi
AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# platform
AC_MSG_CHECKING(platform)
if echo "let _ = Sys.os_type;;" | ocaml | grep -q Win32; then
AC_MSG_RESULT(Win32)
OCAMLWIN32=yes
EXE=.exe
else
OCAMLWIN32=no
EXE=
fi
# substitutions to perform
AC_SUBST(OCAMLC)
AC_SUBST(OCAMLOPT)
AC_SUBST(OCAMLDEP)
AC_SUBST(OCAMLLEX)
AC_SUBST(OCAMLYACC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
AC_SUBST(OCAMLGRAPHLIB)
AC_SUBST(ZARITHLIB)
AC_SUBST(OCAMLWEB)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(ENABLEGUI)
AC_SUBST(INCLUDEGTK2)
AC_SUBST(OCAMLWIN32)
AC_SUBST(EXE)
# Finally create the Makefile.configurable from Makefile.configurable.in
AC_OUTPUT(Makefile.configurable)
chmod a-w Makefile.configurable
Jump to Line
Something went wrong with that request. Please try again.