diff options
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 273 |
1 files changed, 0 insertions, 273 deletions
diff --git a/doc/Makefile b/doc/Makefile deleted file mode 100644 index 611e38d3e2..0000000000 --- a/doc/Makefile +++ /dev/null @@ -1,273 +0,0 @@ -# To compile documentation, you need the following tools: -# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils) -# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz) -# Pdf: pdflatex -# Html: -# - hevea: http://para.inria.fr/~maranget/hevea/ -# - htmlSplit: http://coq.inria.fr/~delahaye -# Rapports INRIA: dviselect, rrkit (par Michel Mauny) - -include ../config - -LATEX=latex -BIBTEX=bibtex -MAKEINDEX=makeindex -PDFLATEX=pdflatex -DOCCOQTOP="../bin/$(ARCH)/coqtop -full -bindir ../bin/$(ARCH)/ -libdir ../" -DOCCOQC=../bin/$(ARCH)/coqc -full -bindir ../bin/$(ARCH)/ -libdir ../ -COQTEX=../bin/$(ARCH)/coq-tex -image $(DOCCOQTOP) -v -sl -small -TEXINPUTS=$(COQTOP)/tools/coq-tex:/usr/local/lib/rrkit/RRINPUTSDIR:.: -ZLIBS=-I ../src/lib/util -I ../src/parsing -I ../src/meta -I ../src/constr \ - -I ../src/typing -I ../src/proofs -I ../src/env -I ../src/tactics \ - -I ../tactics - -INPUTS=./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex - -LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \ - library/Wf.tex library/Specif.tex - -REFMANCOQTEXFILES=\ - RefMan-gal.v.tex RefMan-ext.v.tex RefMan-tac.v.tex \ - RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \ - RefMan-syn.v.tex RefMan-ppr.v.tex RefMan-tus.v.tex - -COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex Program.v.tex\ - Omega.v.tex Natural.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \ - Programs.v.tex - -REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \ - RefMan-pro.tex RefMan-oth.tex \ - RefMan-com.tex RefMan-uti.tex RefMan-add.tex \ - $(REFMANCOQTEXFILES) - -REFMAN=Reference-Manual - -#VERSION=V6.3.1 -VERSION=POSITIONNEZ-CETTE-VARIABLE -FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/$(VERSION)/doc -WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc - -FTPDOCS=Changes.dvi.gz Changes.ps.gz \ - Reference-Manual-base.ps.gz Reference-Manual-base.dvi.gz \ - Reference-Manual-addendum.ps.gz Reference-Manual-addendum.dvi.gz\ - Reference-Manual-all.ps.gz Reference-Manual-all.dvi.gz\ - Library.dvi.gz Library.ps.gz\ - Tutorial.dvi.gz Tutorial.ps.gz\ - README all-ps-docs.tar.gz - -FTPHTMLDOCS=doc-html.tar.gz - -######################### -# Principal targets -######################## - -all: demos-programs all-dvi all-pdf - -coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex - -latex-part: all-dvi - -all-dvi: Tutorial.v.dvi Reference-Manual.dvi Library.dvi Changes.v.dvi - -all-pdf: Tutorial.v.pdf Reference-Manual.pdf Library.pdf Changes.v.pdf - -all-ps: Tutorial.v.ps Reference-Manual.ps Library.ps Changes.v.ps - -all-html: Tutorial.v.html Reference-Manual.html Changes.v.html - - -# dvips et dviselect existent sur loupiac -distrib: - make clean-coq demos-programs - make clean-latex all-dvi all-ps all-pdf compress-latex - make clean-html all-html doc-html.tar.gz html-www - -compress-latex: - sh Reference-Manual.sh - mv -f Reference-Manual.ps Reference-Manual-all.ps - mv -f Tutorial.v.ps Tutorial.ps - mv -f Tutorial.v.dvi Tutorial.dvi - mv -f Reference-Manual.dvi Reference-Manual-all.dvi - mv -f Changes.v.ps Changes.ps - mv -f Changes.v.dvi Changes.dvi - - mv -f Tutorial.v.pdf Tutorial.pdf - - mv -f Changes.v.pdf Changes.pdf - tar cf all-ps-docs.tar Reference-Manual-base.ps \ - Reference-Manual-addendum.ps Changes.ps Tutorial.ps Library.ps - gzip *.ps - gzip *.dvi - gzip *.pdf - gzip all-ps-docs.tar - -Tutorial.v.html: Tutorial.v.tex - hevea ./book-html.sty ./coq-html.sty ./Tutorial.v.tex - -Changes.v.html: Changes.v.tex - hevea ./Changes.v.tex - -Reference-Manual.html: - hevea ./book-html.sty ./coq-html.sty ./Reference-Manual.tex - -doc-html.tar.gz: all-html - - $(MKDIR) coq-docs-html - rm -rf coq-docs-html/* - cp Tutorial.v.html coq-docs-html/tutorial.html - cp Changes.v.html coq-docs-html/changes.html - cp Reference-Manual.html coq-docs-html - (cd coq-docs-html;\ - htmlsplit -N -T "The Coq Proof Assistant Reference Manual"\ - ./Reference-Manual.html; rm ./Reference-Manual.html) - cp cover.html coq-docs-html - tar cf doc-html.tar coq-docs-html - gzip doc-html.tar - -# Pour le site de Coq. -html-www: all-html - - $(MKDIR) www - rm -rf www/* - cp Tutorial.v.html www/tutorial.html - cp Changes.v.html www/changes.html - cp Reference-Manual.html www - (cd www;\ - htmlsplit -N -T "The Coq Proof Assistant Reference Manual"\ - -n ../icons/next.gif -p ../icons/prev.gif -r ../icons/root.gif\ - -s ../icons/sub.gif ./Reference-Manual.html;\ - rm ./Reference-Manual.html) - cp cover.html www - - -clean-refman: - rm -f Reference-Manual.toc Reference-Manual.idx Reference-Manual.atoc\ - Reference-Manual.aux Reference-Manual.bbl Reference-Manual.blg\ - Reference-Manual.ilg Reference-Manual.ind\ - Reference-Manual.tacidx Reference-Manual.tacind\ - Reference-Manual.comidx Reference-Manual.comind\ - Reference-Manual.erridx Reference-Manual.errind\ - Reference-Manual.dvi Reference-Manual.ps\ - Reference-Manual.sh\ - $(REFMANFILES:.tex=.aux) $(REFMANFILES:.tex=.log)\ - $(COQTEXFILES:.tex=.aux) $(COQTEXFILES:.tex=.log) - -clean-latex: clean-refman - rm -f *.dvi *.aux *.log *.bbl *.blg *.ps *.toc *.idx *~ *.ilg *.ind\ - *.dvi.gz *.ps.gz *.pdf *.pdf.gz - -clean-coq: - rm -f *.v.tex avl.ml heapsort.ml euclid.ml library/libdoc.tex *.cm[io] - -clean: clean-coq clean-latex - -clean-html: - rm -f Tutorial.v.html Changes.v.html Reference-Manual.html - -cleanall: clean clean-html - -######################### -# Implicit rules -######################### - -.SUFFIXES: .dvi .tex .v.tex .ps .pdf - -.tex.dvi: - $(LATEX) $< - $(LATEX) $< - -.tex.pdf: - $(PDFLATEX) $< - $(PDFLATEX) $< - -.tex.v.tex: - $(COQTEX) $< - -.dvi.ps: - dvips -o $@ $< - - -########################## -# Dependencies -########################## - -Library.dvi: $(INPUTS) library/libdoc.tex Library.tex -Library.pdf: $(INPUTS) library/libdoc.tex Library.tex - -library/libdoc.tex: - (cd ../theories ; make doc) - -demos-programs: - (cd ../theories/DEMOS/PROGRAMS ; make all) - -Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex - -Tutorial.v.dvi: ./title.tex Tutorial.tex -Tutorial.v.pdf: ./title.tex Tutorial.tex - -RefMan-ppr.v.tex: ../tactics/eqdecide.cmo - -RefMan-tus.v.tex: ../tactics/EqDecide.vo ../tactics/eqdecide.cmo - -Reference-Manual.ps: Reference-Manual.dvi - -Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - rm -f Reference-Manual.sh - $(LATEX) Reference-Manual - rm Reference-Manual.sh - $(BIBTEX) Reference-Manual - $(LATEX) Reference-Manual - rm Reference-Manual.sh - $(BIBTEX) Reference-Manual - $(LATEX) Reference-Manual - rm Reference-Manual.sh - $(MAKEINDEX) Reference-Manual - $(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind - $(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind - $(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind - $(LATEX) Reference-Manual - rm Reference-Manual.sh - $(LATEX) Reference-Manual - -Reference-Manual.pdf: Reference-Manual.dvi - rm -f Reference-Manual.sh - $(PDFLATEX) Reference-Manual.tex - -quick: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - rm -f Reference-Manual.sh - $(LATEX) Reference-Manual - - -################### -# RT -################### -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -Reference-Manual-RT.dvi: Reference-Manual.dvi RefMan-cover.tex - dviselect -i Reference-Manual.dvi -o RefMan-body.dvi 3: - $(LATEX) RefMan-cover.tex - set a=`tail -1 Reference-Manual.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - if test "$$a = 0";\ - then rrkit RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\ - fi - -# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny) -Tutorial-RT.dvi : Tutorial.v.dvi Tutorial-cover.tex - dviselect -i Tutorial.v.dvi -o Tutorial-body.dvi 3: - $(LATEX) Tutorial-cover.tex - set a=`tail -1 Tutorial.v.log`;\ - set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\ - if test "$$a = 0";\ - then rrkit Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\ - fi - -################ doc ftp and www installation ############ -doc-ftp-www-install: doc-ftp-install doc-www-install - -doc-ftp-install: - - mkdir $(FTPDOCDIR) - cp $(ALLFTPDOCS) $(FTPHTMLDOCS) $(FTPDOCDIR) - chmod g+w $(FTPDOCDIR)/* - -doc-www-install: - (cd $(WWWDOCDIR); rm -f node*.html main*.html toc.html \ - tutorial.html changes.html cover.html) - cp www/* $(WWWDOCDIR) |