Commit 12a3d007 authored by Andrei Paskevich's avatar Andrei Paskevich

add dependency on menhir (not on the library) + a bit of cleanup

parent c35b73a0
......@@ -56,6 +56,12 @@ OCAMLVERSION = @OCAMLVERSION@
CAMLP5O = @CAMLP5O@
ifeq (@enable_menhirlib@,yes)
MENHIR = @MENHIR@ --table
else
MENHIR = @MENHIR@
endif
#PSVIEWER = @PSVIEWER@
#PDFVIEWER = @PDFVIEWER@
......@@ -75,10 +81,18 @@ else
DYNLINK =
endif
ifeq (@enable_menhirlib@,yes)
INCLUDES += -I +menhirLib
MENHIRLIB = menhirLib
else
MENHIRLIB =
endif
EXTOBJS = $(MENHIRLIB)
EXTLIBS = str unix nums $(DYNLINK)
EXTCMA = $(addsuffix .cma,$(EXTLIBS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS))
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
###############
# main target
......@@ -142,7 +156,7 @@ LIBMLI = $(addsuffix .mli, $(LIBMODULES))
LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
$(LIBCMX): OFLAGS += -for-pack Why
# build targets
......@@ -273,51 +287,45 @@ install::
# IDE
###############
IDE_FILES = scheduler
IDE_MAIN_FILE = gmain
IDE_FILES = scheduler gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
IDEMAIN = $(addprefix src/ide/, $(IDE_MAIN_FILE))
IDEML = $(addsuffix .ml, $(IDEMODULES))
IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))
IDEMAINML = $(addsuffix .ml, $(IDEMAIN))
$(IDECMO) $(IDECMX) $(addsuffix .cmx, $(IDEMAIN)) $(addsuffix .cmo, $(IDEMAIN)): INCLUDES = -thread -I src/ide -I +threads
# -I +sqlite3
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
src/ide/gmain.cmo src/ide/gmain.cmx: INCLUDES += -I +lablgtk2
# build targets
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt: bin/whyide.opt
endif
bin/whyide.opt bin/whyide.byte: INCLUDES = -thread -I +lablgtk2
# -I +sqlite3
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2
# -I +sqlite3
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
# sqlite3
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX) src/ide/gmain.cmx
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx $^
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
# sqlite3.cmxa
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO) src/ide/gmain.cmo
bin/whyide.byte: src/why.cma $(PGMCMO) $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
lablgtk.cma lablgtksourceview2.cma gtkThread.cmo $^
# sqlite3.cma
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
# depend and clean targets
include .depend.ide
.depend.ide:
$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) $(IDEMAINML) > $@
$(OCAMLDEP) -slash -I src -I src/ide $(IDEML) $(IDEMLI) > $@
depend: .depend.ide
......@@ -385,31 +393,25 @@ clean::
# Tptp2why
########
MENHIR=@MENHIR@
TPTPGENERATED = src/tptp2why/tptpLexer.ml \
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli
TPTP_FILES = tptpTree tptpParser tptpLexer tptpTranslate tptp2why
TPTP_DIR=src/tptp2why/
TPTPMODULES = $(addprefix $(TPTP_DIR), $(TPTP_FILES))
TPTPMODULES = $(addprefix src/tptp2why/, $(TPTP_FILES))
TPTPML = $(addsuffix .ml, $(TPTPMODULES))
TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR) -I src/core/
$(TPTPML) $(TPTPMLI): OCAMLYACC = $(MENHIR)
$(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
# build targets
ifeq (@enable_tptp2why_support@,yes)
byte: bin/tptp2why.byte
opt: bin/tptp2why.opt
endif
src/tptp2why/tptpParser.ml src/tptp2why/tptpParser.mli: OCAMLYACC = $(MENHIR)
bin/tptp2why.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
......@@ -422,14 +424,12 @@ bin/tptp2why.byte: src/why.cma $(TPTPCMO) src/main.cmo
# depend and clean targets
ifeq (@enable_tptp2why_support@,yes)
include .depend.tptp2why
.depend.tptp2why: $(TPTPGENERATED)
$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@
depend: .depend.tptp2why
endif
clean::
rm -f $(TPTPGENERATED)
......
......@@ -59,12 +59,6 @@ AC_ARG_ENABLE(verbose-make,
[ --enable-verbose-make verbose makefile commands],,
enable_verbose_make=no)
# rust prover
AC_ARG_ENABLE(rust-prover,
[ --enable-rust-prover enable Why3 rust prover],,
enable_rust_prover=yes)
# IDE
AC_ARG_ENABLE(ide,
......@@ -83,6 +77,12 @@ AC_ARG_ENABLE(coq-support,
[ --enable-coq-support enable Coq support],,
enable_coq_support=yes)
# Menhir library
AC_ARG_ENABLE(menhirlib,
[ --enable-menhirlib enable Menhir library],,
enable_menhirlib=yes)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -213,6 +213,11 @@ if test "$OCAMLYACC" = no ; then
AC_MSG_ERROR(Cannot find ocamlyacc.)
fi
AC_CHECK_PROG(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
AC_MSG_ERROR(Cannot find menhir.)
fi
AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,true)
if test "$OCAMLDOC" = true ; then
AC_MSG_WARN(Cannot find ocamldoc)
......@@ -225,13 +230,14 @@ fi
AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
# checking for sqlite3
if test "$enable_rust_prover" = yes ; then
AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_rust_prover=no)
# checking for libmenhir
if test "$enable_menhirlib" = yes ; then
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
fi
# checking for lablgtk2
# checking for sqlite3 and lablgtk2
if test "$enable_ide" = yes ; then
#AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,,enable_ide=no)
AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtksourceview2.cma,,enable_ide=no)
fi
......@@ -271,16 +277,6 @@ if test "$CAMLP5O" = no; then
enable_coq_support=no
fi
# tptp2why
AC_CHECK_PROG(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no; then
enable_tptp2why_support=no
else
enable_tptp2why_support=yes
fi
# hypothesis_selection
if test "$enable_hypothesis_selection" = yes; then
......@@ -310,6 +306,7 @@ AC_SUBST(OCAMLOPT)
AC_SUBST(OCAMLDEP)
AC_SUBST(OCAMLLEX)
AC_SUBST(OCAMLYACC)
AC_SUBST(MENHIR)
AC_SUBST(OCAMLDOC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
......@@ -323,7 +320,6 @@ dnl AC_SUBST(OCAMLWEB)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(enable_rust_prover)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)
......@@ -333,8 +329,7 @@ AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(MENHIR)
AC_SUBST(enable_tptp2why_support)
AC_SUBST(enable_menhirlib)
AC_SUBST(enable_hypothesis_selection)
......@@ -361,13 +356,12 @@ echo "OCaml library path : $OCAMLLIB"
echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide"
echo "Why plugins : $enable_plugins"
echo "Why rust prover : $enable_rust_prover"
echo "Coq support : $enable_coq_support"
if test "$enable_coq_support" = "yes" ; then
echo " Version : $COQVERSION"
echo " Lib : $COQLIB"
fi
echo "tptp2why support : $enable_tptp2why_support"
echo "Menhir library : $enable_menhirlib"
echo "hypothesis selection : $enable_hypothesis_selection"
echo "profiling : $ENABLE_PROFILING"
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