Commit 15ea5190 authored by Andrei Paskevich's avatar Andrei Paskevich

fix configure and Makefile

thanks to Frédéric Herbreteau for the patch!

The TPTP plugin does not load (Linux 64bit) when compiled with
the Menhir library. For the moment, let us leave it as it is.
The use of the library is not necessary and is off by default.
parent b8392be7
......@@ -57,15 +57,11 @@ OCAMLVERSION = @OCAMLVERSION@
CAMLP5O = @CAMLP5O@
ifeq (@enable_menhirlib@,yes)
MENHIR = @MENHIR@ --table
else
MENHIR = @MENHIR@
endif
ifeq (@enable_menhirlib@,yes)
MENHIRINC = -I +menhirLib
MENHIR = @MENHIR@ --table
MENHIRINC = -I @MENHIRLIB@
MENHIRLIB = menhirLib
else
MENHIR = @MENHIR@
MENHIRINC =
MENHIRLIB =
endif
......@@ -152,9 +148,9 @@ LIBDIRS = util core parser driver transform printer
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
ifeq (@enable_hypothesis_selection@,yes)
LIB_TRANSFORM += hypothesis_selection
INCLUDES += -I +ocamlgraph
EXTLIBS += ocamlgraph/graph
LIB_TRANSFORM += hypothesis_selection
INCLUDES += -I @OCAMLGRAPHLIB@
EXTLIBS += graph
endif
LIBML = $(addsuffix .ml, $(LIBMODULES))
......@@ -529,7 +525,7 @@ opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
......@@ -579,7 +575,7 @@ REPLAYERMLI = $(addsuffix .mli, $(REPLAYERMODULES))
REPLAYERCMO = $(addsuffix .cmo, $(REPLAYERMODULES))
REPLAYERCMX = $(addsuffix .cmx, $(REPLAYERMODULES))
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
$(REPLAYERCMO) $(REPLAYERCMX): INCLUDES += -I src/ide
# build targets
......@@ -643,7 +639,7 @@ $(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/ide -I src/bench -I @SQLITE3LIB@
byte: bin/why3bench.byte
opt: bin/why3bench.opt
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I +sqlite3
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
bin/why3bench.opt: src/why.cmxa $(PGMCMX) $(BENCHCMX)
......@@ -930,11 +926,11 @@ testl-type: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte --type-only tests/test-pgm-jcf.mlw
test-api: src/why.cma
ocaml $(EXTCMA) src/why.cma -I src examples/use_api.ml \
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
bts12244: src/why.cma
ocaml $(EXTCMA) src/why.cma -I src examples/bts12244.ml
ocaml -I src/ $(INCLUDES) $(EXTCMA) src/why.cma examples/bts12244.ml
## Examples : Plugins ##
......
......@@ -274,7 +274,18 @@ fi
# checking for libmenhir
if test "$enable_menhirlib" = yes ; then
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
if test "$USEOCAMLFIND" = yes; then
MENHIRLIB=$(ocamlfind query menhirLib)
fi
if test -n "$MENHIRLIB"; then
echo "ocamlfind found menhir library in $MENHIRLIB"
else
MENHIRLIB="+menhirLib"
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
if test "$enable_menhirlib" = no; then
AC_MSG_WARN(Lib menhir not found.)
fi
fi
fi
# checking for rubber
......@@ -288,7 +299,7 @@ fi
# checking for lablgtk2
if test "$enable_ide" = yes ; then
if test "$USEOCAMLFIND" == yes; then
if test "$USEOCAMLFIND" = yes; then
LABLGTK2LIB=$(ocamlfind query lablgtk2)
fi
if test -n "$LABLGTK2LIB";then
......@@ -311,7 +322,7 @@ fi
# checking for sqlite3
if test "$enable_ide" = yes ; then
if test "$USEOCAMLFIND" == yes; then
if test "$USEOCAMLFIND" = yes; then
SQLITE3LIB=$(ocamlfind query sqlite3)
fi
if test -n "$SQLITE3LIB";then
......@@ -328,9 +339,17 @@ fi
# checking for sqlite3
if test "$enable_bench" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_bench=no)
if test "$enable_bench" = no; then
AC_MSG_WARN(Lib sqlite3 not found, why3bench disabled.)
if test "$USEOCAMLFIND" = yes; then
SQLITE3LIB=$(ocamlfind query sqlite3)
fi
if test -n "$SQLITE3LIB"; then
echo "ocamlfind found sqlite3 in $SQLITE3LIB"
else
SQLITE3LIB="+sqlite3"
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_bench=no)
if test "$enable_bench" = no; then
AC_MSG_WARN(Lib sqlite3 not found, why3bench disabled.)
fi
fi
fi
......@@ -387,7 +406,18 @@ reason_coq_support=" (not yet implemented)"
# hypothesis_selection
if test "$enable_hypothesis_selection" = yes; then
AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,,enable_hypothesis_selection=no)
if test "$USEOCAMLFIND" = yes; then
OCAMLGRAPHLIB=$(ocamlfind query ocamlgraph)
fi
if test -n "$OCAMLGRAPHLIB"; then
echo "ocamlfind found ocamlgraph in $OCAMLGRAPHLIB"
else
OCAMLGRAPHLIB="+ocamlgraph"
AC_CHECK_FILE($OCAMLLIB/ocamlgraph/,,enable_hypothesis_selection=no)
if test "$enable_hypothesis_selection" = no; then
AC_MSG_WARN(Lib ocamlgraph not found, hypothesis selection disabled.)
fi
fi
fi
if test "$enable_local" = no; then
......@@ -442,7 +472,7 @@ AC_SUBST(OCAMLVERSION)
AC_SUBST(OCAMLLIB)
dnl AC_SUBST(OCAMLV)
dnl AC_SUBST(FORPACK)
dnl AC_SUBST(OCAMLGRAPHLIB)
AC_SUBST(OCAMLGRAPHLIB)
dnl AC_SUBST(OCAMLWEB)
AC_SUBST(enable_profiling)
......@@ -450,6 +480,7 @@ AC_SUBST(enable_profiling)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(MENHIRLIB)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
......
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