COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
COQINCLUDES := -Q . predaware \
               -R ../vericert/src vericert \
               $(foreach d, $(COMPCERTRECDIRS), -R ../vericert/lib/CompCert/$(d) compcert.$(d)) \
               -R ../vericert/lib/CompCert/flocq Flocq \
               -R ../vericert/lib/CompCert/MenhirLib MenhirLib

COQMAKE := coq_makefile

VS := Main.v

all: Makefile.coq _CoqProject $(VS)
	$(MAKE) -f Makefile.coq

Main.v: main.org
	@echo "TANGLE" $<
	@emacs -batch -find-file main.org -funcall org-babel-tangle

%.pdf: %.mkiv
	@echo "CONTEXT" $<
	@context $<

Makefile.coq: force
	@echo "COQMAKE Makefile.coq"
	@$(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq

_CoqProject: force
	@echo "CREATE _CoqProject"
	@echo "$(COQINCLUDES)" >_CoqProject

force:

clean:
	git clean -dfx

.PHONY: force all clean