Commit 47a250ed authored by MARCHE Claude's avatar MARCHE Claude

Zarith support: fixed compilation of Why3 Coq tactic

parent f983f9eb
......@@ -77,7 +77,7 @@ endif
# external libraries common to all binaries
EXTOBJS =
EXTLIBS = str unix @BIGINTLIB@ dynlink
EXTLIBS = str unix @BIGINTLIB@ dynlink
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
......@@ -102,12 +102,13 @@ endif
# Why3 library
##############
LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
LIBGENERATED = src/util/config.ml src/util/bigInt.ml \
src/util/rc.ml src/parser/lexer.ml \
src/parser/parser.mli src/parser/parser.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/session/xml.ml
LIB_UTIL = config util opt lists strings extmap extset exthtbl weakhtbl \
LIB_UTIL = config bigInt util opt lists strings extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
......@@ -165,16 +166,18 @@ $(LIBDEP): $(LIBGENERATED)
ifeq (@enable_zarith@,yes)
src/util/bigInt.ml: src/util/bigInt_ocamlnum.ml src/util/bigInt_zarith.ml
src/util/bigInt.ml: config.status src/util/bigInt_zarith.ml
cp src/util/bigInt_zarith.ml src/util/bigInt.ml
else
src/util/bigInt.ml: src/util/bigInt_ocamlnum.ml
src/util/bigInt.ml: config.status src/util/bigInt_ocamlnum.ml
cp src/util/bigInt_ocamlnum.ml src/util/bigInt.ml
endif
clean::
rm -f src/util/bigInt.ml
# build targets
......@@ -797,11 +800,11 @@ src/coq-tactic/coqCompat.ml: src/coq-tactic/coqCompat@coq_compat_version@.ml
lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
$(OCAMLOPT) $(OFLAGS) -o $@ -shared @BIGINTLIB@.cmxa $^
lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) -a $(BFLAGS) -o $@ $^
$(OCAMLC) -a $(BFLAGS) -o $@ @BIGINTLIB@.cma $^
src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
......@@ -809,12 +812,12 @@ src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -byte -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -byte @BIGINTINCLUDE@ -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
$(if $(QUIET),@echo 'Coqc $<' &&) \
WHY3CONFIG="" $(COQC) -opt -I lib/coq-tactic/ $< && \
WHY3CONFIG="" $(COQC) -opt @BIGINTINCLUDE@ -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......
......@@ -346,6 +346,7 @@ if test "$enable_zarith" = yes; then
fi
if test -n "$BIGINTINCLUDE"; then
echo "ocamlfind found zarith in $BIGINTINCLUDE"
BIGINTINCLUDE="-I $BIGINTINCLUDE"
else
BIGINTINCLUDE="+zarith"
AC_CHECK_FILE($OCAMLLIB/zarith/zarith.cma,,enable_zarith=no)
......@@ -710,6 +711,7 @@ AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
AC_SUBST(META_OCAMLGRAPH)
AC_SUBST(enable_zarith)
AC_SUBST(BIGINTINCLUDE)
AC_SUBST(BIGINTLIB)
......
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