# -*- Makefile -*-

# --------------------------------------------------------------------
NAME     := xhl
SUBDIRS  := reals
INCFLAGS := -R reals/src SsrReals
INCFLAGS += -R finmap SsrReals
INCFLAGS += -R src $(NAME)
COQFILES := \
	src/notations.v \
	src/inhabited.v \
	src/xtactics.v \
	src/xbigops.v \
	src/passn.v \
	src/pwhile.v \
	src/psemantic.v \
	src/range.v\
	src/ellora.v \
	src/sound.v \
	src/complete.v

include Makefile.common

# --------------------------------------------------------------------
this-clean::
	rm -f src/*.glob src/*.d src/*.vo src/*.vio src/.*.aux

this-distclean::
	rm -f $(shell find . -name '*~')

# --------------------------------------------------------------------
.PHONY: count dist

# --------------------------------------------------------------------
DISTDIR = xhl
TAROPT  = --posix --owner=0 --group=0

dist:
	if [ -e $(DISTDIR) ]; then rm -rf $(DISTDIR); fi
	$(MAKE) -C reals dist
	./scripts/distribution.py $(DISTDIR) MANIFEST
	tar -xof reals/alternate-reals.tar.bz2 -C $(DISTDIR)
	mv $(DISTDIR)/alternate-reals $(DISTDIR)/reals
	BZIP2=-9 tar $(TAROPT) -cjf $(DISTDIR).tar.bz2 $(DISTDIR)
	rm -rf $(DISTDIR)

count:
	@coqwc $(COQFILES) | tail -1 | \
	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
