Commit d3529345 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Even when Coq realizations are not compiled, lib/coq/BuiltIn.vo should be, if the tactic is.

parent db532aa5
......@@ -829,6 +829,8 @@ endif
# Coq realizations
####################
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
......@@ -864,18 +866,6 @@ endif
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(if $(QUIET),@echo 'Coqc $<' &&) \
$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -R lib/coq Why3 $< > $@
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
......@@ -900,8 +890,6 @@ drivers/coq-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
opt byte: $(COQVO)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq
cp lib/coq/BuiltIn.vo $(LIBDIR)/why3/coq/
......@@ -925,22 +913,6 @@ ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
endif
depend: $(COQVD)
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp
......@@ -976,11 +948,49 @@ else
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
install_no_local::
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
COQLIBS_FILES = lib/coq/BuiltIn
endif
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(if $(QUIET),@echo 'Coqc $<' &&) \
$(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) \
$(COQDEP) -R lib/coq Why3 $< > $@
opt byte: $(COQVO)
install_local:: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS:clean%=clean)" "clean"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
endif
depend: $(COQVD)
clean-coq:
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
clean:: clean-coq
else
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
endif
install_no_local::
cp drivers/coq-realizations.aux $(DATADIR)/why3/drivers/
opt byte: drivers/coq-realizations.aux
clean::
......
......@@ -516,6 +516,12 @@ else
;;
esac
fi
AC_CHECK_PROG(COQDEP,coqdep,coqdep,no)
if test "$COQDEP" = no ; then
enable_coq_support=no
AC_MSG_WARN(Cannot find coqdep.)
reason_coq_support=" (coqdep not found)"
fi
fi
if test "$enable_coq_support" = no; then
......@@ -538,15 +544,6 @@ if test "$enable_coq_tactic" = yes -a "$CAMLP5O" = no; then
reason_coq_tactic=" (camlp5o not found)"
fi
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 coqdep.)
reason_coq_libs=" (coqdep not found)"
fi
fi
if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
......@@ -756,6 +753,7 @@ AC_SUBST(MENHIRLIB)
AC_SUBST(enable_coq_tactic)
AC_SUBST(enable_coq_libs)
AC_SUBST(enable_coq_support)
AC_SUBST(enable_coq_fp_libs)
AC_SUBST(coq_compat_version)
......
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