diff options
| author | notin | 2006-03-14 15:01:00 +0000 |
|---|---|---|
| committer | notin | 2006-03-14 15:01:00 +0000 |
| commit | f548bcddd7aca88889978c092747e4427017cd43 (patch) | |
| tree | 8dbfc2f39774a0dbfd49b9ad1e978a632f1391c1 /doc/Makefile | |
| parent | f31923c002943eebd7601871658cd636f7f2de4e (diff) | |
r8637@thot: notin | 2006-03-14 16:00:49 +0100
- intégration de doc dans le Makefile principal
- correction d'une incompatibilité avec Tetex 3.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 32 |
1 files changed, 14 insertions, 18 deletions
diff --git a/doc/Makefile b/doc/Makefile index bf21022a76..e4b7e2fe97 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -7,6 +7,9 @@ # Pdf: pdflatex # Html: hevea (http://hevea.inria.fr) >= 1.05 +include ../config/Makefile + + LATEX=latex BIBTEX=bibtex -min-crossrefs=10 MAKEINDEX=makeindex @@ -19,7 +22,6 @@ DOCCOQTOP=$(COQTOP)/bin/coqtop COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small COQDOC=$(COQTOP)/bin/coqdoc -VERSION=8.0pl3 #VERSION=POSITIONNEZ-CETTE-VARIABLE ###################################################################### @@ -62,13 +64,13 @@ rectutorial:\ .SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png -.tex.v.tex: +%.v.tex: %.tex (cd `dirname $<`; $(COQTEX) `basename $<`) -.dvi.ps: +%.ps: %.dvi (cd `dirname $<`; dvips -o `basename $@` `basename $<`) -.png.eps: +%.eps: %.png pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ clean: @@ -145,13 +147,13 @@ refman/Reference-Manual.dvi: $(REFMANFILES) $(LATEX) Reference-Manual;\ $(LATEX) Reference-Manual) -refman/Reference-Manual.pdf: refman/Reference-Manual.dvi +refman/Reference-Manual.pdf: refman/Reference-Manual.tex (cd refman; $(PDFLATEX) Reference-Manual.tex) ### Reference Manual (browsable format) refman/Reference-Manual.html: refman/Reference-Manual.dvi # to ensure bbl file - (cd refman; hevea -fix -nosymb -exec xxdate.exe ./Reference-Manual.tex) + (cd refman; hevea -fix -exec xxdate.exe ./Reference-Manual.tex) refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \ refman/cover.html refman/index.html @@ -191,7 +193,7 @@ faq/FAQ.v.pdf: common/version.tex common/title.tex faq/FAQ.v.dvi faq/axioms.png (cd faq; $(PDFLATEX) FAQ.v.tex) faq/FAQ.v.html: faq/FAQ.v.dvi # to ensure FAQ.v.bbl - (cd faq; hevea -fix -nosymb FAQ.v.tex) + (cd faq; hevea -fix FAQ.v.tex) faq/html/index.html: faq/FAQ.v.html - rm -rf faq/html @@ -205,10 +207,7 @@ faq/html/index.html: faq/FAQ.v.html GLOBDUMP=$(COQTOP)/glob.dump -LIBDIRS=\ - Logic Bool Arith ZArith Reals \ - Lists Strings IntMap Sorting \ - Sets Relations Wellfounded +LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations Sorting Wellfounded IntMap ### Standard library (browsable html format) @@ -228,13 +227,10 @@ stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/ind ### Standard library (printable format - produces > 350 pages) -stdlib/library.files: - (cd stdlib; GALLINA=gallina ./make-library-files) - -stdlib/Library.coqdoc.tex: stdlib/library.files - WHERE=`pwd`/stdlib; cd $(COQTOP)/theories; \ - $(COQDOC) -q --body-only --latex -o $$WHERE/Library.coqdoc.tex \ - -R `pwd`/$(COQTOP)/theories Coq `cat $$WHERE/library.files` +stdlib/Library.coqdoc.tex: + (for dir in $(LIBDIRS) ; do \ + $(COQDOC) -q --gallina --body-only --latex --stdout \ + -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done) stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex (cd stdlib;\ |