Makefile.local

# This adds compilation of a test file, without adding it to the
# install target.
## -async-proofs-cache force avoids slowdowns in presence of Undo.

.PHONY: cleantests

tests:
	@echo -n building tests...
	$(SHOW) 'COQC LibHyps/LibHypsTest.v'
	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) -async-proofs-cache force -w -undo-batch-mode $(COQLIBS) ./LibHyps/LibHypsTest.v $(TIMING_EXTRA) 
	@echo " ==> tests passed."
	@echo -n building regression tests...
	$(SHOW) 'COQC LibHyps/LibHypsRegression.v' 
	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) -async-proofs-cache force -w -undo-batch-mode $(COQLIBS) ./LibHyps/LibHypsRegression.v $(TIMING_EXTRA) 
	@echo " ==> regression tests passed."
	@echo -n building demo file...
	$(SHOW) 'COQC Demo/demo.v > /dev/null' 
	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) -async-proofs-cache force -w -undo-batch-mode $(COQLIBS) ./Demo/demo.v $(TIMING_EXTRA) > /dev/null
	@echo " ==> regression tests passed."

cleantests:
	rm -f LibHyps/LibHypsRegression.vo LibHyps/LibHypsRegression.vok LibHyps/LibHypsRegression.vos LibHyps/LibHypsRegression.glob
	rm -f LibHyps/LibHypsTest.vo LibHyps/LibHypsTest.vok LibHyps/LibHypsTest.vos LibHyps/LibHypsTest.glob
	rm -f Demo/*.vo Demo/*.vok Demo/*.vos Demo/*.glob

clean::
	rm -f LibHyps/*.vo LibHyps/*.vos LibHyps/*.vok LibHyps/*.glob LibHyps/*.aux
	rm -f LibHyps/.*.vo LibHyps/.*.aux

### Local Variables: ***
### mode: makefile ***
### End: ***