From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 29 Apr 2010 09:56:37 +0000
Subject: Move from ocamlweb to ocamdoc to generate mli documentation

dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.

In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.

ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html

The possibility to put graphs in pdf/html seems to be lost.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/Makefile | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 dev/Makefile

(limited to 'dev/Makefile')

diff --git a/dev/Makefile b/dev/Makefile
new file mode 100644
index 0000000000..4693bd136c
--- /dev/null
+++ b/dev/Makefile
@@ -0,0 +1,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 $<
\ No newline at end of file
-- 
cgit v1.2.3