Makefile.coq.local

VO ?= vo

.PHONY: computed
computed: $(filter $(addsuffix %,$(wildcard theories/*/Computed/)),$(VFILES:.v=.$(VO)))

.PHONY: computed-lite
computed-lite: theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.vo

.PHONY: models
models: $(filter theories/%/Model.vo,$(VFILES:.v=.$(VO)))

.PHONY: models-all
models-all: models $(filter $(addsuffix %,$(wildcard theories/*/Model/)),$(VFILES:.v=.$(VO)))

.PHONY: theorem-statements
theorem-statements: $(filter theories/%/TheoremStatement.vo,$(VFILES:.v=.$(VO)))

.PHONY: utils
utils: $(filter-out $(addsuffix %,$(dir $(wildcard theories/*/TheoremStatement.v))),$(VFILES:.v=.$(VO)))

EXTRA_COQ_CI_TARGETS := \
	theories/Util/Wf_Uint63/Instances.vo \
	#
#	theories/Util/Wf_Uint63/Proofs.vo # this one seems to loop on master :-(

.PHONY: coq-ci-target
coq-ci-target: models theorem-statements $(EXTRA_COQ_CI_TARGETS)