NAME = theory

default: coq

all: doc coq

doc: $(NAME).ps $(NAME).pdf

show:
	@echo '$(VALUE)="$($(VALUE))"'
NOTHING =
SPACE = $(NOTHING) $(NOTHING)

include build/Makefile.coq

COQC = coqc
COQDOC = coqdoc
COQDEP = coqdep

VS := $(wildcard src/*.v src/*/*.v)

coq: $(patsubst src/%.v,build/%.vo,$(VS))

%.glob: %.vo
	@:

%.vo: %.v
	$(COQC) -R build "" $<

GENERATED_TEX := $(patsubst src/%.v,tex/%.tex,$(wildcard src/*.v))

$(NAME).ps: $(NAME).dvi
	touch $@

$(NAME).pdf: $(NAME).ps
	ps2pdf $< $@

$(NAME).dvi: *.tex $(GENERATED_TEX)
# These first 2 lines are a hack, needed because latexmk doesn't
# handle metapost
	latexmk -C theory
	latexmk theory
	latexmk -C theory
	mpost figures
	latexmk -ps theory

# XXX glob removed for now
# tex/%.tex: %.v %.glob coqdoc.v coqdoc.glob
tex/%.tex: src/%.v src/coqdoc.v build/coqdoc.glob
	$(COQDOC) --latex --body-only --parse-comments src/coqdoc.v \
	  $< -o tex/$*.full_tex
# Ugly hack to remove empty coqdoccode environments:
	sed -n '1h; 1!H; $$ { g; s/\\begin{coqdoccode}\( \|\n\|\\coqdocemptyline\)*\\end{coqdoccode}//g; p }' < tex/$*.full_tex > $@

clean:
	rubber -p --clean $(NAME)
	rm -f tex/*
	rm -f *.log
	rm -f *.thm
	rm -f $(NAME).pdf
	rm -f figures.*
	rm -rf build

update: $(NAME).pdf
	scp $< community.haskell.org:/srv/projects/camp/files

build/%.v:
	mkdir -p $(dir $@)
	ln -s $(shell echo $(dir $@) | sed "s#[^/]\+#..#g")$(patsubst build/%,src/%,$@) $@

build/Makefile.coq: | $(patsubst src/%,build/%,$(VS))
	$(COQDEP) -R build "" $(patsubst src/%,build/%,$(VS)) > $@

.PHONY: default all clean update coq depend