aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/Makefile
blob: 4693bd136cbccfc2d9c959c8e1ebf9cbc844c1f8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
include ../config/Makefile

LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \
	      -I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \
              -I ../proofs -I ../tactics -I ../pretyping \
              -I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \
              -I ../plugins/omega -I ../plugins/romega \
	      -I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \
              -I ../plugins/xml -I ../plugins/extraction \
              -I ../plugins/fourier -I ../plugins/cc \
	      -I ../plugins/funind -I ../plugins/firstorder \
              -I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \
              -I ../plugins/recdef

MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)

MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \
	../pretyping/*.mli ../interp/*.mli \
	../parsing/*.mli ../proofs/*.mli \
	../tactics/*.mli ../toplevel/*.mli)

all:: html coq.pdf

newsyntax.dvi: newsyntax.tex
	latex $<
	latex $<

coq.dvi: coq.tex
	latex coq
	latex coq

coq.tex::
	ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
	$(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex

html::
	ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
	$(MLIS) -d html -colorize-code \
	-t "Coq mlis documentation" -intro docintro -css-style style.css

%.dot: ../%
	ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@

%.png: %.dot
	dot -Tpng $< -o $@

clean::
	rm -f *~ *.log *.aux

.SUFFIXES: .tex .png

%.pdf: %.tex
	pdflatex $< && pdflatex $<