Commit 8d93a81c authored by Andrei Paskevich's avatar Andrei Paskevich

configure: add checks for sqlite3

parent f8f4110c
...@@ -253,8 +253,10 @@ MNGCMX = $(addsuffix .cmx, $(MNGMODULES)) ...@@ -253,8 +253,10 @@ MNGCMX = $(addsuffix .cmx, $(MNGMODULES))
$(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3 $(MNGCMO) $(MNGCMX): INCLUDES = -I src/manager -I +sqlite3
ifeq (@enable_proof_manager@,yes)
byte: bin/manager.byte byte: bin/manager.byte
opt: bin/manager.opt opt: bin/manager.opt
endif
bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3 bin/manager.opt bin/manager.byte: INCLUDES = -I +sqlite3
...@@ -503,13 +505,13 @@ DOC = doc/manual.pdf doc/manual.html ...@@ -503,13 +505,13 @@ DOC = doc/manual.pdf doc/manual.html
doc: $(DOC) doc: $(DOC)
doc/manual.pdf: doc/manual.tex doc/version.tex doc/manual.pdf: doc/manual.tex doc/version.tex
make -C doc manual.pdf $(MAKE) -C doc manual.pdf
doc/manual.html: doc/manual.tex doc/version.tex doc/manual.html: doc/manual.tex doc/version.tex
make -C doc manual.html $(MAKE) -C doc manual.html
clean:: clean::
make -C doc clean $(MAKE) -C doc clean
########## ##########
# API DOC # API DOC
...@@ -646,7 +648,7 @@ dep: depend ...@@ -646,7 +648,7 @@ dep: depend
# export-www: # export-www:
# echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml # echo "<#def version>$(VERSION)</#def>" > /users/demons/filliatr/www/why/version.prehtml
# echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml # echo "<#def cversion>$(CVERSION)</#def>" >> /users/demons/filliatr/www/why/version.prehtml
# make -C /users/demons/filliatr/www/why install # $(MAKE) -C /users/demons/filliatr/www/why install
# #
# source: export/$(NAME).tar.gz # source: export/$(NAME).tar.gz
# cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP) # cp CHANGES CHANGES.caduceus export/$(NAME).tar.gz $(FTP)
...@@ -659,19 +661,19 @@ dep: depend ...@@ -659,19 +661,19 @@ dep: depend
# cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar # cd export; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar
# #
# tarball-for-framac: # tarball-for-framac:
# make tarball # $(MAKE) tarball
# cp export/$(NAME).tar.gz export/why-for-framac.tar.gz # cp export/$(NAME).tar.gz export/why-for-framac.tar.gz
# #
# tarball: # tarball:
# mkdir -p export # mkdir -p export
# cd export; rm -rf $(NAME) $(NAME).tar.gz # cd export; rm -rf $(NAME) $(NAME).tar.gz
# make export/$(NAME).tar.gz # $(MAKE) export/$(NAME).tar.gz
# #
# EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw # EXFILES = lib/coq*/*.v examples/*/*.v examples/*/*.mlw
# #
# export-examples: # export-examples:
# cp --parents $(EXFILES) $(WWW) # cp --parents $(EXFILES) $(WWW)
# make -C $(WWW)/examples clean depend # $(MAKE) -C $(WWW)/examples clean depend
# echo "*** faire make all dans $(WWW)/examples ***" # echo "*** faire make all dans $(WWW)/examples ***"
# #
# export-examples-c: # export-examples-c:
......
...@@ -21,57 +21,63 @@ ...@@ -21,57 +21,63 @@
# #
# autoconf input for Objective Caml programs # autoconf input for Objective Caml programs
# Copyright (C) 2001 Jean-Christophe Fillitre # Copyright (C) 2001 Jean-Christophe Fillitre
# from a first script by Georges Mariano # from a first script by Georges Mariano
# #
# This library is free software; you can redistribute it and/or # This library is free software; you can redistribute it and/or
# modify it under the terms of the GNU Library General Public # modify it under the terms of the GNU Library General Public
# License version 2, as published by the Free Software Foundation. # License version 2, as published by the Free Software Foundation.
# #
# This library is distributed in the hope that it will be useful, # This library is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of # but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
# #
# See the GNU Library General Public License version 2 for more details # See the GNU Library General Public License version 2 for more details
# (enclosed in the file LGPL). # (enclosed in the file LGPL).
# the script generated by autoconf from this input will set the following # the script generated by autoconf from this input will set the following
# variables: # variables:
# OCAMLC "ocamlc" if present in the path, or a failure # OCAMLC "ocamlc" if present in the path, or a failure, or
# or "ocamlc.opt" if present with same version number as ocamlc # "ocamlc.opt" if present with same version number as ocamlc
# OCAMLOPT "ocamlopt" (or "ocamlopt.opt" if present), or "no" # OCAMLOPT "ocamlopt" (or "ocamlopt.opt" if present), or "no"
# OCAMLBEST either "byte" if no native compiler was found, # OCAMLBEST "opt" if a native compiler was found; "byte" otherwise
# or "opt" otherwise # OCAMLDEP "ocamldep" or "ocamldep.opt"
# OCAMLDEP "ocamldep" # OCAMLLEX "ocamllex" or "ocamllex.opt"
# OCAMLLEX "ocamllex" # OCAMLYACC "ocamlyacc"
# OCAMLYACC "ocamlyac" # OCAMLDOC "ocamldoc" or "ocamldoc.opt"
# OCAMLLIB the path to the ocaml standard library # OCAMLLIB the path to the ocaml standard library
# OCAMLVERSION the ocaml version number # OCAMLVERSION the ocaml version number
# OCAMLWEB "ocamlweb" (not mandatory) # OCAMLWEB "ocamlweb" (not mandatory)
# check for one particular file of the sources # check for one particular file of the sources
# ADAPT THE FOLLOWING LINE TO YOUR SOURCES! # ADAPT THE FOLLOWING LINE TO YOUR SOURCES!
AC_INIT(src/) AC_INIT(src/)
# verbosemake feature # verbosemake
AC_ARG_ENABLE(verbose-make, AC_ARG_ENABLE(verbose-make,
[ --enable-verbose-make verbose makefile commands],, [ --enable-verbose-make verbose makefile commands],,
enable_verbose_make=no) enable_verbose_make=no)
# IDE feature # proof manager
AC_ARG_ENABLE(proof-manager,
[ --enable-proof-manager enable Why3 proof manager],,
enable_proof_manager=yes)
# IDE
AC_ARG_ENABLE(ide, AC_ARG_ENABLE(ide,
[ --enable-ide enable Why IDE],, [ --enable-ide enable Why3 IDE],,
enable_ide=yes) enable_ide=yes)
# dynlink feature # dynlink
AC_ARG_ENABLE(plugins, AC_ARG_ENABLE(plugins,
[ --enable-plugins enable Why3 plugins],, [ --enable-plugins enable Why3 plugins],,
enable_plugins=yes) enable_plugins=yes)
# Coq plugin feature # Coq plugin
AC_ARG_ENABLE(coq-support, AC_ARG_ENABLE(coq-support,
[ --enable-coq-support enable Coq support],, [ --enable-coq-support enable Coq support],,
...@@ -84,7 +90,7 @@ if uname -s | grep -q CYGWIN ; then ...@@ -84,7 +90,7 @@ if uname -s | grep -q CYGWIN ; then
EXE=.exe EXE=.exe
STRIP='echo "no strip "' STRIP='echo "no strip "'
CPULIMIT=cpulimit-win CPULIMIT=cpulimit-win
AC_MSG_RESULT(.exe) AC_MSG_RESULT(.exe)
else else
EXE= EXE=
STRIP=strip STRIP=strip
...@@ -100,7 +106,7 @@ if test "$OCAMLC" = no ; then ...@@ -100,7 +106,7 @@ if test "$OCAMLC" = no ; then
AC_MSG_ERROR(Cannot find ocamlc.) AC_MSG_ERROR(Cannot find ocamlc.)
fi fi
# we extract Ocaml version number # we extract Ocaml version number
OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` OCAMLVERSION=`$OCAMLC -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
echo "ocaml version is $OCAMLVERSION" echo "ocaml version is $OCAMLVERSION"
...@@ -108,7 +114,7 @@ case "$OCAMLVERSION" in ...@@ -108,7 +114,7 @@ case "$OCAMLVERSION" in
0.*|1.*|2.*|3.0*) 0.*|1.*|2.*|3.0*)
AC_MSG_ERROR(You need Objective Caml 3.10 or later);; AC_MSG_ERROR(You need Objective Caml 3.10 or later);;
3.10*) 3.10*)
enable_plugins=no;; enable_plugins=no;;
esac esac
if test "$enable_plugins" = "yes" ; then if test "$enable_plugins" = "yes" ; then
...@@ -205,6 +211,11 @@ else ...@@ -205,6 +211,11 @@ else
fi fi
fi fi
# checking for sqlite3
if test "$enable_proof_manager" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_proof_manager=no)
fi
# checking for lablgtk2 # checking for lablgtk2
if test "$enable_ide" = yes ; then if test "$enable_ide" = yes ; then
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no) AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
...@@ -304,8 +315,9 @@ echo "OCaml library path : $OCAMLLIB" ...@@ -304,8 +315,9 @@ echo "OCaml library path : $OCAMLLIB"
echo "Verbose make : $enable_verbose_make" echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide" echo "Why IDE : $enable_ide"
echo "Why plugins : $enable_plugins" echo "Why plugins : $enable_plugins"
echo "Why proof manager : $enable_proof_manager"
echo "Coq support : $enable_coq_support" echo "Coq support : $enable_coq_support"
if test "$enable_coq_support" = "yes" ; then if test "$enable_coq_support" = "yes" ; then
echo " Version : $COQVERSION" echo " Version : $COQVERSION"
echo " Lib : $COQLIB" echo " Lib : $COQLIB"
fi fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment