From 47a250ed3fbe6ea9aed85b39f28a5ef050964f5d Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Sat, 15 Feb 2014 17:43:51 +0100
Subject: [PATCH] Zarith support: fixed compilation of Why3 Coq tactic

---
 Makefile.in  | 21 ++++++++++++---------
 configure.in |  2 ++
 2 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index 9f9292326..5562c003c 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -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
diff --git a/configure.in b/configure.in
index 2cadbb982..56c4fb7e3 100644
--- a/configure.in
+++ b/configure.in
@@ -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)
 
-- 
GitLab