Commit dcf4d669 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Switch to fine-grained dependency computations for Coq libraries.

parent 4f1dcb0e
......@@ -10,6 +10,9 @@ why3.conf
*.cmxs
*.annot
*.dep
*.vo
*.vd
*.glob
\#*\#
# /
......@@ -18,7 +21,6 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/.depend.coq-libs
/semantic.cache
/TAGS
/output_why3
......
......@@ -937,9 +937,13 @@ COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
COQVD = $(addsuffix .vd, $(COQLIBS_FILES))
%.vo: %.v
$(COQC) -R lib/coq Why3 $<
$(if $(QUIET),@echo 'Coqc $<' &&) $(COQC) -R lib/coq Why3 $<
%.vd: %.v
$(if $(QUIET),@echo 'Coqdep $<' &&) $(COQDEP) -slash -R lib/coq Why3 $< > $@
drivers/coq-realizations.aux:
echo "(* generated automatically at compilation time *)" > $@
......@@ -966,17 +970,13 @@ endif
install_local: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS)" "clean"
include .depend.coq-libs
include $(COQVD)
endif
.depend.coq-libs:
$(COQDEP) -slash -R lib/coq Why3 $(COQV) > $@
depend: .depend.coq-libs
depend: $(COQVD)
clean::
rm -f $(COQVO) $(addsuffix .glob, $(COQLIBS_FILES))
rm -f .depend.coq-libs
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
else
......
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