Add a configure option for compiling and installing Coq realizations.

Makefile.in

@@ -54,6 +54,8 @@ OCAMLDOC  = @OCAMLDOC@
 OCAMLLIB  = @OCAMLLIB@
 OCAMLBEST = @OCAMLBEST@
 OCAMLVERSION = @OCAMLVERSION@
+COQC      = @COQC@
+COQDEP    = @COQDEP@
 
 CAMLP5O   = @CAMLP5O@
 
@@ -209,7 +211,6 @@ clean::
 
 install_no_local::
 	mkdir -p $(BINDIR)
-	mkdir -p $(LIBDIR)/why3/coq
 	mkdir -p $(DATADIR)/why3/images
 	mkdir -p $(DATADIR)/why3/emacs
 	mkdir -p $(DATADIR)/why3/lang
@@ -782,7 +783,7 @@ endif
 # Coq plugin
 ##############
 
-ifeq (@enable_coq_support@,yes)
+ifeq (@enable_coq_plugin@,yes)
 
 COQGENERATED = src/coq-plugin/g_whytac.ml
 
@@ -816,19 +817,58 @@ src/coq-plugin/g_whytac.ml: src/coq-plugin/g_whytac.ml4
 
 # depend and clean targets
 
-include .depend.coq
+include .depend.coq-plugin
 
-.depend.coq: $(COQGENERATED)
+.depend.coq-plugin: $(COQGENERATED)
 	$(OCAMLDEP) -slash -I src -I src/coq-plugin $(COQML) > $@
 
-depend: .depend.coq
+depend: .depend.coq-plugin
 
 clean::
 	rm -f src/coq-plugin/*.cm[iox] src/coq-plugin/*.o
 	rm -f src/coq-plugin/*.cma src/coq-plugin/*.cmxs
 	rm -f src/coq-plugin/*.annot src/coq-plugin/*~
 	rm -f $(COQGENERATED)
-	rm -f .depend.coq
+	rm -f .depend.coq-plugin
+
+endif
+
+####################
+# Coq realizations
+####################
+
+ifeq (@enable_coq_libs@,yes)
+
+COQLIBS_REAL_FILES = Abs MinMax Real Square
+COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
+
+COQLIBS_FILES = $(COQLIBS_REAL)
+
+COQV  = $(addsuffix .v,  $(COQLIBS_FILES))
+COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
+
+%.vo: %.v
+	$(COQC) -R lib/coq Why3 $<
+
+all: $(COQVO)
+
+install_no_local::
+	mkdir -p $(LIBDIR)/why3/coq
+	mkdir -p $(LIBDIR)/why3/coq/real
+	cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
+
+install_local: $(COQVO)
+
+include .depend.coq-libs
+
+.depend.coq-libs:
+	$(COQDEP) -slash -R lib/coq Why3 $(COQV) > $@
+
+depend: .depend.coq-libs
+
+clean::
+	rm -f $COQVO $(addsuffix .glob, $(COQLIBS_FILES))
+	rm -f .depend.coq-libs
 
 endif
 
@@ -1126,12 +1166,6 @@ clean::
 # .ml4.ml:
 # 	$(CAMLP4) pr_o.cmo -impl $< > $@
 
-# lib/coq/%.vo: lib/coq/%.v
-# 	$(COQC8) -I lib/coq $<
-
-# lib/coq-v7/%.vo: lib/coq-v7/%.v
-# 	$(COQC7) -I lib/coq-v7 $<
-
 # jc/jc_ai.ml: jc/jc_annot_inference.ml jc/jc_annot_fail.ml Makefile
 # 	if test "@enable_apron@" = "yes" ; then \
 # 	  echo "# 1 \"jc/jc_annot_inference.ml\"" > jc/jc_ai.ml; \

configure.in

@@ -77,11 +77,15 @@ AC_ARG_ENABLE(bench,
     [  --enable-bench          enable Why3 benchmarking tool],,
     enable_bench=yes)
 
-# Coq plugin
+# Coq plugin and libraries
 
-AC_ARG_ENABLE(coq-support,
-    [  --enable-coq-support    enable Coq support],,
-    enable_coq_support=yes)
+AC_ARG_ENABLE(coq-plugin,
+    [  --enable-coq-plugin     enable Coq plugin],,
+    enable_coq_plugin=yes)
+
+AC_ARG_ENABLE(coq-libs,
+    [  --enable-coq-libs       enable Coq realizations],,
+    enable_coq_libs=yes)
 
 # TPTP parser
 
@@ -363,7 +367,7 @@ dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
 
 # Coq
 
-if test "$enable_coq_support" = no; then
+if test "$enable_coq_plugins" = no -a "$enable_coq_libs" = no; then
     enable_coq_support=no
     AC_MSG_WARN(coq support disabled)
     reason_coq_support=" (disabled by user)"
@@ -391,21 +395,36 @@ else
         esac
     fi
 fi
-if test "$enable_coq_support" = yes; then
-   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_support=no)
-   if test "$enable_coq_support" = no; then
-      reason_coq_support=" ($COQLIB/kernel/term.cmi not found)"
+
+if test "$enable_coq_support" = no; then
+   enable_coq_plugin=no
+   enable_coq_libs=no
+fi
+
+if test "$enable_coq_plugin" = yes; then
+   AC_CHECK_FILE($COQLIB/kernel/term.cmi,,enable_coq_plugin=no)
+   if test "$enable_coq_plugin" = no; then
+      reason_coq_plugin=" ($COQLIB/kernel/term.cmi not found)"
    fi
 fi
 
-if test "$CAMLP5O" = no; then
-   enable_coq_support=no
-   reason_coq_support=" (camlp5o not found)"
+if test "$enable_coq_plugin" = yes -a "$CAMLP5O" = no; then
+   enable_coq_plugin=no
+   reason_coq_plugin=" (camlp5o not found)"
 fi
 
 # coq-plugin currently disabled
-enable_coq_support=no
-reason_coq_support=" (not yet implemented)"
+enable_coq_plugin=no
+reason_coq_plugin=" (not yet implemented)"
+
+if test "$enable_coq_libs" = yes; then
+   AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
+   if test "$COQDEP" = no ; then
+      enable_coq_libs=no
+      AC_MSG_WARN(Cannot find coqc.)
+      reason_coq_libs=" (coqdep not found)"
+   fi
+fi
 
 # hypothesis_selection
 
@@ -483,7 +502,8 @@ AC_SUBST(SQLITE3LIB)
 AC_SUBST(enable_bench)
 AC_SUBST(META_OCAMLGRAPH)
 
-AC_SUBST(enable_coq_support)
+AC_SUBST(enable_coq_plugin)
+AC_SUBST(enable_coq_libs)
 
 AC_SUBST(COQC)
 AC_SUBST(COQDEP)
@@ -528,10 +548,12 @@ echo "Verbose make            : $enable_verbose_make"
 echo "Why IDE                 : $enable_ide $reason_ide"
 echo "Why bench tool          : $enable_bench"
 echo "Why documentation       : $enable_doc"
-echo "Coq plugin support      : $enable_coq_support $reason_coq_support"
+echo "Coq support             : $enable_coq_support $reason_coq_support"
 if test "$enable_coq_support" = "yes" ; then
    echo "    Version             : $COQVERSION"
    echo "    Lib                 : $COQLIB"
+   echo "    Plugin support      : $enable_coq_plugin $reason_coq_plugin"
+   echo "    Realization support : $enable_coq_libs $reason_coq_libs"
 fi
 echo "TPTP parser             : $enable_whytptp"
 echo "Menhir library          : $enable_menhirlib"

lib/coq/.gitignore

+*.vo
+*.glob