view Makefile @ 23:c8070689f5ca

Switch [input_line] to [read_line]
author Adam Chlipala <adamc@hcoop.net>
date Fri, 05 Sep 2008 16:48:13 -0400
parents 91e247c68ee8
children aba1a37394c4
line wrap: on
line source
MODULES_NODOC := Tactics
MODULES_PROSE := StackMachine
MODULES_CODE  := StackMachine
MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
VS            := $(MODULES:%=src/%.v)
VS_DOC        := $(MODULES_DOC:%=%.v)
GLOBALS       := .coq_globals
TEMPLATES     := $(MODULES_CODE:%=templates/%.v)

.PHONY: coq clean doc dvi html templates

coq: Makefile.coq
	make -f Makefile.coq

Makefile.coq: Makefile $(VS)
	coq_makefile $(VS) \
		COQC = "coqc -I src -impredicative-set \
			-dump-glob $(GLOBALS)" \
		-o Makefile.coq

clean:: Makefile.coq
	make -f Makefile.coq clean
	rm -f Makefile.coq .depend $(GLOBALS) \
		latex/*.sty latex/cpdt.* templates/*.v

doc: latex/cpdt.dvi latex/cpdt.pdf html

latex/cpdt.tex: Makefile $(VS)
	cd src ; coqdoc --latex $(VS_DOC) \
		-p "\usepackage{url}" \
		-p "\title{Certified Programming with Dependent Types}" \
		-p "\author{Adam Chlipala}" \
		-p "\iffalse" \
		-o ../latex/cpdt.tex

latex/cpdt.dvi: latex/cpdt.tex
	cd latex ; latex cpdt ; latex cpdt

latex/cpdt.pdf: latex/cpdt.dvi
	cd latex ; pdflatex cpdt

html: Makefile $(VS)
	cd src ; coqdoc $(VS_DOC) -toc \
		--glob-from ../$(GLOBALS) \
		-d ../html

dvi:
	xdvi latex/cpdt

templates: $(TEMPLATES)

templates/%.v: src/%.v
	ocaml tools/make_template.ml <$< >$@