From 015781acfe4a2a75eeced513528b389cae9fb0a3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 23 Feb 2006 14:21:14 +0000 Subject: Mise à jour des Makefile, ajout licences, corrections mineures suite à restructuration du répertoire de documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8607 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/Makefile | 578 +++++++++++++++--------------------- doc/README | 48 ++- doc/common/title.tex | 11 +- doc/faq/FAQ.tex | 23 +- doc/refman/Reference-Manual.tex | 11 +- doc/refman/cover.html | 2 +- doc/stdlib/Library.tex | 11 +- doc/stdlib/index-list.html.template | 275 +++++++++++++++++ doc/stdlib/index-trailer.html | 2 + doc/stdlib/make-library-files | 36 +++ doc/stdlib/make-library-index | 32 ++ doc/tutorial/Tutorial.tex | 10 +- 12 files changed, 652 insertions(+), 387 deletions(-) create mode 100644 doc/stdlib/index-list.html.template create mode 100644 doc/stdlib/index-trailer.html create mode 100755 doc/stdlib/make-library-files create mode 100755 doc/stdlib/make-library-index diff --git a/doc/Makefile b/doc/Makefile index d61e02a3c8..ac1be10f19 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -1,368 +1,280 @@ # Makefile for the Coq documentation -# if coqc,coqtop,coq-tex are not in your PATH, you need the environment -# variable COQBIN to be correctly set -# (COQTOP is autodetected) -# (some files are preprocessed using Coq and some part of the documentation -# is automatically built from the theories sources) +# COQTOP needs to be set to a coq source repository # 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) +# Dvi: latex (latex2e), bibtex, makeindex # Pdf: pdflatex -# Html: -# - hevea: http://para.inria.fr/~maranget/hevea/ -# - htmlSplit: http://coq.inria.fr/~delahaye -# Rapports INRIA: dviselect, rrkit (par Michel Mauny) - - -ifeq ("$(COQBIN)","") - COQBINPATH = -else - COQBINPATH = $(COQBIN)/ -endif - -DOCCOQTOP=$(COQBINPATH)coqtop #.byte -DOCCOQC=$(COQBINPATH)coqc -COQTOP=`$(DOCCOQC) -where` -COQTEX=$(COQBINPATH)coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small -#COQWEBSTY=$(HOME)/lib/tex/ -COQWEBSTY=/usr/share/texmf/tex/latex/misc/ -HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea +# Html: hevea (http://hevea.inria.fr) >= 1.05 LATEX=latex BIBTEX=bibtex -min-crossrefs=10 MAKEINDEX=makeindex PDFLATEX=pdflatex -MKDIR=mkdir -TEST=test +HEVEALIB=/usr/local/lib/hevea:/usr/lib/hevea +TEXINPUTS=$(HEVEALIB):.: -TEXINPUTS=/usr/local/lib/rrkit/RRINPUTSDIR:$(COQWEBSTY):$(HEVEALIB):.: +DOCCOQTOP=$(COQTOP)/bin/coqtop +COQTEX=$(COQTOP)/bin/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small +COQDOC=$(COQTOP)/bin/coqdoc -INPUTS=./version.tex ./macros.tex ./title.tex ./headers.tex ./Reference-Manual.tex +VERSION=8.0pl3 +#VERSION=POSITIONNEZ-CETTE-VARIABLE -LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \ - library/Wf.tex library/Specif.tex +###################################################################### +### General rules +###################################################################### -REFMANCOQTEXFILES=\ - RefMan-gal.v.tex RefMan-ext.v.tex RefMan-mod.v.tex RefMan-tac.v.tex \ - RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \ - RefMan-syn.v.tex RefMan-oth.v.tex +all: all-html all-pdf all-ps -COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex \ - Omega.v.tex Changes.v.tex Tutorial.v.tex Polynom.v.tex \ - Setoid.v.tex Helm.tex -#SUPPRIME: Program.v.tex Natural.v.tex Correctness.v.tex +all-html:\ + tutorial/Tutorial.v.html refman/html/index.html \ + faq/html/index.html stdlib/html/index.html -REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \ - RefMan-pro.tex RefMan-com.tex RefMan-ltac.tex RefMan-uti.tex \ - RefMan-ide.tex coqide.eps coqide-queries.eps RefMan-add.tex RefMan-modr.tex \ - $(REFMANCOQTEXFILES) +all-pdf:\ + tutorial/Tutorial.v.pdf refman/Reference-Manual.pdf \ + faq/faq.v.pdf stdlib/Library.pdf -REFMAN=Reference-Manual +all-ps:\ + tutorial/Tutorial.v.ps refman/Reference-Manual.ps \ + faq/faq.v.ps stdlib/Library.ps -VERSION=8.0 -#VERSION=POSITIONNEZ-CETTE-VARIABLE +refman:\ + refman/html/index.html refman/Reference-Manual.ps refman/Reference-Manual.pdf -FTPDOCDIR=/net/pauillac/infosystems/ftp/coq/coq/V$(VERSION)/doc -WWWDOCDIR=/net/pauillac/infosystems/www/coq/doc - -FTPDOCS=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\ -# Changes.dvi.gz Changes.ps.gz - -FTPHTMLDOCS=doc-html.tar.gz - -######################### -# Principal targets -######################## - -all: check-env all-ps all-pdf - -check-env: - @if $(TEST) "$(COQBIN)" = ""; then \ - if coq-tex; then true ; \ - else echo "coq-tex not found, COQBIN undefined"; exit 1; fi; \ - fi - @if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; \ - else echo "COQTOP = $(COQTOP)"; fi - -coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex - -latex-part: all-dvi - -all-dvi: Tutorial.v.dvi Reference-Manual.dvi # faq.v.dvi Library.dvi Changes.v.dvi - -all-pdf: Tutorial.v.pdf Reference-Manual.pdf # faq.v.pdf Library.pdf Changes.v.pdf - -all-ps: Tutorial.v.ps Reference-Manual.ps # faq.v.ps Library.ps Changes.v.ps - -all-html: Tutorial.v.html Reference-Manual.html # faq.v.html Library.html Changes.v.html - -#version -version.tex: Makefile - echo "\newcommand{\coqversion}{$(VERSION)}" > version.tex - - -# dvips et dviselect existent sur loupiac -distrib: - make check-env - 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 Tutorial.ps # Library.ps # Changes.ps - gzip -f *.ps - gzip -f *.dvi - gzip -f *.pdf - gzip -f all-ps-docs.tar - -Tutorial.v.html: Tutorial.v.tex - hevea ./book-html.sty ./coq-html.sty ./Tutorial.v - -Changes.v.html: Changes.v.tex - hevea ./Changes.v.tex - -Reference-Manual.html: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib -#1.05 ? hevea -fix ./book-html.sty ./coq-html.sty ./Reference-Manual.tex -#1.04 hevea ./book-html.sty ./coq-html.sty ./Reference-Manual.tex - hevea -fix -nosymb -exec xxdate.exe ./Reference-Manual.tex - -faq.v.html: faq.v.tex - hevea ./faq.v - -coq.info: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - hevea -info ./book-html.sty ./coq-html.sty ./Reference-Manual.tex - -doc-html.tar.gz: all-html - $(MKDIR) -p coq-docs-html - rm -rf coq-docs-html/* - cp Tutorial.v.html coq-docs-html/tutorial.html - cp Reference-Manual.html coqide-queries.png coqide.png coq-docs-html - (cd coq-docs-html; hacha -o toc.html ./Reference-Manual.html; rm ./Reference-Manual.html) - cp cover.html main.html main-0.html coq-docs-html - tar cf doc-html.tar coq-docs-html - gzip -f doc-html.tar - -# Pour le site de Coq. -html-www: all-html - $(MKDIR) -p www - rm -rf www/* - cp Tutorial.v.html www/tutorial.html - cp coqide-queries.png coqide.png www - (cd www; hacha -o toc.html ../Reference-Manual.html) - cp cover.html main.html main-0.html www - ln -s main.html www/index.html - - -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 Reference-Manual.html # Changes.v.html - rm -f *.hatoc *.haux *.hcomind *.herrind *.hidx *.hind *.htacind *.htoc - - -cleanall: clean clean-html - -######################### -# Implicit rules -######################### +tutorial:\ + tutorial/Tutorial.v.html tutorial/Tutorial.v.ps tutorial/Tutorial.v.pdf -.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png +stdlib:\ + stdlib/html/index.html stdlib/Library.ps stdlib/Library.pdf + +faq:\ + faq/html/index.html faq/faq.v.ps faq/faq.v.pdf -.tex.dvi: - $(LATEX) $< - $(LATEX) $< +###################################################################### +### Implicit rules +###################################################################### -.tex.pdf: - $(PDFLATEX) $< - $(PDFLATEX) $< +.SUFFIXES: .dvi .tex .v.tex .ps .pdf .eps .png .tex.v.tex: - $(COQTEX) $< + (cd `dirname $<`; $(COQTEX) `basename $<`) .dvi.ps: - dvips -o $@ $< + (cd `dirname $<`; dvips -o `basename $@` `basename $<`) -%.eps: %.png +.png.eps: pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ +clean: + rm -f */*.dvi */*.aux */*.log */*.bbl */*.blg */*.toc \ + */*.idx */*~ */*.ilg */*.ind */*.dvi.gz */*.ps.gz */*.pdf.gz\ + */*.???idx */*.???ind */*.v.tex */*.atoc */*.lof\ + */*.hatoc */*.haux */*.hcomind */*.herrind */*.hidx */*.hind \ + */*.htacind */*.htoc */*.v.html + rm -f stdlib/index-list.html stdlib/index-body.html \ + stdlib/library.coqdoc.tex stdlib/library.files \ + stdlib/library.files.ls + rm -f refman/euclid.ml{,i} refman/heapsort.ml{,i} + rm -f common/version.tex + rm -f refman/*.eps refman/Reference-Manual.html + +cleanall: clean + rm -f */*.ps */*.pdf + rm -rf refman/html stdlib/html faq/html tutorial/tutorial.v.html + +###################################################################### +# Common +###################################################################### +COMMON=common/version.tex common/title.tex common/macros.tex -########################## -# Dependencies -########################## - -Library.dvi: $(INPUTS) library.coqweb.tex Library.tex - $(LATEX) Library - $(LATEX) Library - -Library.pdf: $(INPUTS) library.coqweb.tex Library.tex - $(PDFLATEX) Library - $(PDFLATEX) Library - -# L'option -exec xxdate.exe sert a produire la date (macro \today) -# mais ne marche pas avec hevea 1.04 -Library.html: $(INPUTS) library.coqweb.tex Library.tex - hevea ./coq-html.sty -exec xxdate.exe $(COQWEBSTY)/coqweb.sty ./Library.tex -#1.04 hevea ./coq-html.sty $(COQWEBSTY)/coqweb.sty ./Library.tex - -LIBDIRS= Logic Bool Arith ZArith Reals Lists Sets Relations \ - Wellfounded IntMap - -library.coqweb.tex: library.files - WHERE=`pwd` ; \ - cd $(COQTOP)/theories; \ - coqweb --noweb -o $$WHERE/$@ --no-preamble `cat $$WHERE/library.files` - -GALLINA=$(COQBINPATH)gallina - -# On garde la liste de tous les *.v avec dates dans library.files.ls -# Si elle a change depuis la derniere fois ou library.files n'existe pas -# on fabrique des .g (si besoin) et la liste library.files dans -# l'ordre de ls -tr des *.vo -# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création -# En supposant que make fait son boulot, ca fait un tri topologique du -# graphe des dépendances -library.files:: - rm -f library.files.ls.tmp - (cd $(COQTOP)/theories ; find $(LIBDIRS) -name "*.v" -ls) > library.files.ls.tmp - if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then \ - mv -f library.files.ls.tmp library.files.ls; \ - rm -f library.files; touch library.files; \ - ABSOLUTE=`pwd`/library.files ; \ - for rep in $(LIBDIRS) ; do \ - (cd $(COQTOP)/theories/$$rep ; \ - echo $$rep/intro.tex >> $$ABSOLUTE ; \ - VOFILES=`ls -tr *.vo` ; \ - for file in $$VOFILES ; do \ - VF=`basename $$file \.vo` ; \ - if $(TEST) \( ! -e $$VF.g \) -o \( $$VF.v -nt $$VF.g \) ; then \ - $(GALLINA) $$VF.v; fi ; \ - echo $$rep/$$VF.g >> $$ABSOLUTE ; \ - done \ - ) ; \ - done ; \ - fi - -demos-programs: -# (cd ../theories/DEMOS/PROGRAMS ; make all) - -Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex - -Tutorial.v.dvi: ./version.tex ./title.tex Tutorial.v.tex -Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex - -# RefMan-ppr.v.tex: ../tactics/eqdecide.cmo - -# RefMan-tus.v.tex: ../tactics/EqDecide.vo ../tactics/eqdecide.cmo - -Reference-Manual.ps: Reference-Manual.dvi +### Version + +common/version.tex: Makefile + echo "\newcommand{\coqversion}{$(VERSION)}" > common/version.tex + +###################################################################### +# Reference Manual +###################################################################### + +REFMANCOQTEXFILES=\ + refman/RefMan-gal.v.tex refman/RefMan-ext.v.tex \ + refman/RefMan-mod.v.tex refman/RefMan-tac.v.tex \ + refman/RefMan-cic.v.tex refman/RefMan-lib.v.tex \ + refman/RefMan-tacex.v.tex refman/RefMan-syn.v.tex \ + refman/RefMan-oth.v.tex \ + refman/Cases.v.tex refman/Coercion.v.tex refman/Extraction.v.tex \ + refman/Omega.v.tex refman/Polynom.v.tex \ + refman/Setoid.v.tex refman/Helm.tex # refman/Natural.v.tex + +REFMANTEXFILES=\ + refman/headers.tex \ + refman/Reference-Manual.tex refman/RefMan-pre.tex \ + refman/RefMan-int.tex refman/RefMan-pro.tex \ + refman/RefMan-com.tex refman/RefMan-ltac.tex \ + refman/RefMan-uti.tex refman/RefMan-ide.tex \ + refman/RefMan-add.tex refman/RefMan-modr.tex \ + $(REFMANCOQTEXFILES) \ + +REFMANEPSFILES= refman/coqide.eps refman/coqide-queries.eps + +REFMANFILES=\ + $(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) refman/biblio.bib + +REFMANPNGFILES=$(REFMANEPSFILES:.eps=.png) + +### Reference Manual (printable format) # The second LATEX compilation is necessary otherwise the pages of the index # are not correct (don't know why...) - BB -Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - $(LATEX) Reference-Manual - $(BIBTEX) Reference-Manual - $(LATEX) Reference-Manual - $(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 - $(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 $(FTPDOCS) $(FTPHTMLDOCS) $(FTPDOCDIR) - - chmod g+w $(FTPDOCDIR)/* - -faq-www-install: - cp faq.v.html $(WWWDOCDIR)/faq.html - -doc-www-install: - (cd $(WWWDOCDIR); rm -f node*.html main*.html toc.html \ - tutorial.html changes.html cover.html) - cp www/* $(WWWDOCDIR) - -# traducteur V7 -> V8 -tradv8: tradv8.ml4 - ocamlopt.opt -o $@ str.cmxa unix.cmxa -pp "camlp4o -impl" -impl $^ - -v8: tradv8 - for f in `grep -l coq_exa *tex`; do \ - echo $$f; \ - ./tradv8 $$f; mv $$f $$f.save; mv $$f.v8 $$f; \ - done +refman/Reference-Manual.dvi: $(REFMANFILES) + (cd refman;\ + $(LATEX) Reference-Manual;\ + $(BIBTEX) Reference-Manual;\ + $(LATEX) Reference-Manual;\ + $(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;\ + $(LATEX) Reference-Manual) + +refman/Reference-Manual.pdf: refman/Reference-Manual.dvi + (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) + +refman/html/index.html: refman/Reference-Manual.html $(REFMANPNGFILES) \ + refman/cover.html refman/index.html + - rm -rf refman/html + mkdir refman/html + cp $(REFMANPNGFILES) refman/html + (cd refman/html; hacha -o toc.html ../Reference-Manual.html) + cp refman/cover.html refman/html + cp refman/index.html refman/html + +###################################################################### +# Tutorial +###################################################################### + +tutorial/Tutorial.v.dvi: common/version.tex common/title.tex tutorial/Tutorial.v.tex + (cd tutorial; $(LATEX) Tutorial.v) + +tutorial/Tutorial.v.pdf: common/version.tex common/title.tex tutorial/Tutorial.v.dvi + (cd tutorial; $(PDFLATEX) Tutorial.v.tex) + +tutorial/Tutorial.v.html: tutorial/Tutorial.v.tex + (cd tutorial; hevea -exec xxdate.exe Tutorial.v) + + +###################################################################### +# FAQ +###################################################################### + +faq/faq.v.dvi: common/version.tex common/title.tex faq/faq.v.tex + (cd faq;\ + $(LATEX) faq.v;\ + $(BIBTEX) faq.v;\ + $(LATEX) faq.v;\ + $(LATEX) faq.v) + +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) + +faq/html/index.html: faq/faq.v.html + - rm -rf faq/html + mkdir faq/html + cp faq/interval_discr.v faq/axioms.png faq/html + cp faq/faq.v.html faq/html/index.html + +###################################################################### +# Standard library +###################################################################### + +GLOBDUMP=$(COQTOP)/glob.dump + +LIBDIRS=\ + Logic Bool Arith ZArith Reals \ + Lists Strings IntMap Sorting \ + Sets Relations Wellfounded + +$(GLOBDUMP): $(COQDOC) + (cd $(COQTOP); $(MAKE) GLOB="-dump-glob $(GLOBDUMP)" coqlib) + +### Standard library (browsable html format) + +stdlib/index-body.html: $(GLOBDUMP) + - rm -rf stdlib/html + mkdir stdlib/html + (cd stdlib/html;\ + $(COQDOC) -q --multi-index --body-only --html --glob-from $(GLOBDUMP)\ + -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) + mv stdlib/html/index.html stdlib/index-body.html + +stdlib/index-list.html: stdlib/index-list.html.template + ./stdlib/make-library-index stdlib/index-list.html + +stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html + cat $^ > $@ + +### 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.dvi: $(COMMON) stdlib/library.coqdoc.tex stdlib/Library.tex + (cd stdlib;\ + $(LATEX) Library;\ + $(LATEX) Library) + +stdlib/Library.pdf: $(COMMON) stdlib/library.coqdoc.tex stdlib/Library.dvi + (cd stdlib; $(PDFLATEX) Library) + +###################################################################### +# Install all documentation files +###################################################################### + +COQINSTALLPREFIX= +DOCDIR=/usr/local/share/doc/coq-8.0 +FULLDOCDIR=$(COQINSTALLPREFIX)$(DOCDIR) +HTMLINSTALLDIR=$(FULLDOCDIR)/html +PRINTABLEINSTALLDIR=$(FULLDOCDIR)/ps + +install-doc: install-meta install-doc-html install-doc-printable + +install-meta: + mkdir $(DOCDIC) + cp LICENCE $(DOCDIC)/LICENCE.doc +# cp $(COQTOP)/LICENCE $(COQTOP)/CREDITS $(COQTOP)/COPYRIGHT $(DOCDIC) +# cp $(COQTOP)/README $(COQTOP)/CHANGES $(DOCDIC) + +install-doc-html: all-html + mkdir $(HTMLINSTALLDIR) + cp -r refman/html $(HTMLINSTALLDIR)/refman + cp -r stdlib/html $(HTMLINSTALLDIR)/stdlib + cp -r tutorial/tutorial.html $(HTMLINSTALLDIR)/ + cp -r faq/html $(HTMLINSTALLDIR)/faq + +install-doc-printable: all-pdf all-ps + mkdir $(PRINTABLEINSTALLDIR) + cp -r refman/Reference-manual.pdf $(PRINTABLEINSTALLDIR) + cp -r stdlib/Library.pdf $(PRINTABLEINSTALLDIR) + cp -r tutorial/Tutorial.v.pdf $(PRINTABLEINSTALLDIR)/Tutorial.pdf + cp -r faq/faq.v.pdf $(PRINTABLEINSTALLDIR)/faq.pdf + cp -r refman/Reference-manual.ps $(PRINTABLEINSTALLDIR) + cp -r stdlib/Library.ps $(PRINTABLEINSTALLDIR) + cp -r tutorial/Tutorial.v.ps $(PRINTABLEINSTALLDIR)/Tutorial.ps + cp -r faq/faq.v.ps $(PRINTABLEINSTALLDIR)/faq.ps diff --git a/doc/README b/doc/README index 1693b1ca01..14cb6e448b 100755 --- a/doc/README +++ b/doc/README @@ -5,40 +5,26 @@ V8.0 is divided into the following documents : * Tutorial.ps: An introduction to the use of the Coq Proof Assistant; - * Reference-Manual-base.ps: 215 pp., includes - - - the description of Gallina, the language of Coq - - the description of the Vernacular, the commands of Coq - - the description of each tactic - - chapters about Grammar/Syntax extentions and Writing tactics - - index on tactics, commands and error messages - - * Reference-Manual-addendum.ps, 75 pp., includes more detailed - explanations and examples about the following topics: - - - the extended Cases (C.Cornes) - - the Coercions (A. Saïbi) - - the tactic Omega (P. Crégut) - - the Correctness tactic (J.-C. Filliâtre) - - the extraction features (J.-C. Filliâtre and P. Letouzey) - - the tactic Ring (S. Boutin and P. Loiseleur) - - the Setoid_replace tactic (C. Renard) - - Index, page and chapter numbers are shared by the two documents, in - order to make cross-references possible. There is also a on the ftp - server a Postscript file Reference-Manual-all.ps that contains the two - documents (base and addendum). + * Reference-Manual.ps: + + Base chapters: + - the description of Gallina, the language of Coq + - the description of the Vernacular, the commands of Coq + - the description of each tactic + - index on tactics, commands and error messages + + Additional chapters: + - the extended Cases (C.Cornes) + - the coercions (A. Saïbi) + - the tactic Omega (P. Crégut) + - the extraction features (J.-C. Filliâtre and P. Letouzey) + - the tactic Ring (S. Boutin and P. Loiseleur) + - the Setoid_replace tactic (C. Renard) + - etc. * Library.ps: A description of the Coq standard library; - * CHANGES: A description of the differences between version 8.0 - and previous versions - * rectypes.ps : A tutorial on recursive types by Eduardo Gimenez -Documentation is also available in the DVI format (you can get the DVI docs -separately or in the tar file all-dvi.docs.tar). - -The Reference Manual and the Tutorial are also available in HTML format +Documentation is also available in the PDF format and HTML format (online at http://coq.inria.fr or by ftp in the file doc-html.tar.gz). - diff --git a/doc/common/title.tex b/doc/common/title.tex index 8e1d1c9c9a..51e817cc51 100755 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -20,7 +20,7 @@ %To show the top for the toc in html \newcommand{\tophtml}{} -\newcommand{\coverpage}[2]{ +\newcommand{\coverpage}[3]{ \thispagestyle{empty} \begin{center} \begin{Huge} @@ -51,12 +51,9 @@ The Coq Proof Assistant\\ {\large{V\coqversion, \printingdate}}\\[20pt] %END LATEX -{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7)}}\\ -{\large{\copyright INRIA 2004-2006 ({\Coq} version 8)}}\\ -{\large{This material may be distributed only subject to the terms and -conditions set forth in the Open Publication License, v1.0 or later -(the latest version is presently available at -\ahrefurl{http://www.opencontent.org/openpub})}}. +{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7.x)}}\\ +{\large{\copyright INRIA 2004-2006 ({\Coq} versions 8.x)}}\\ +{\large{#3}} \end{flushleft} %BEGIN LATEX \newpage diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 7b8ed6d10d..5fcee708f8 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1,4 +1,8 @@ +\ifx\pdfoutput\undefined % si on est pas en pdflatex \documentclass[a4paper]{article} +\else +\documentclass[a4paper,pdftex]{article} +\fi \pagestyle{plain} % yay les symboles @@ -10,7 +14,12 @@ \usepackage{fullpage} \usepackage[latin1]{inputenc} \usepackage[english]{babel} -\usepackage{graphics} + +\ifx\pdfoutput\undefined % si on est pas en pdflatex + \usepackage[dvips]{graphicx} +\else + \usepackage[pdftex]{graphicx} +\fi %\input{../macros.tex} @@ -464,7 +473,14 @@ standard library of {\Coq}. The most interesting ones are Here is a summary of the relative strength of these axioms, most proofs can be found in directory {\tt Logic} of the standard library. -\includegraphics{axioms} +%HEVEA\imgsrc{axioms.png} +%BEGIN LATEX +\ifx\pdfoutput\undefined % si on est pas en pdflatex +\includegraphics[width=1.0\textwidth]{axioms.eps} +\else +\includegraphics[width=1.0\textwidth]{axioms.png} +\fi +%END LATEX \Question{What standard axioms are inconsistent with {\Coq}?} @@ -1621,7 +1637,7 @@ Definition R (a b:list nat) := length a < length b. \item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}). \begin{coq_example*} -Lemma Rwf : well_founded (A:=R). +Lemma Rwf : well_founded R. \end{coq_example*} \item Define the step function (which needs proofs that recursive @@ -1989,6 +2005,7 @@ This is provable without requiring any axiom because axiom $K$ directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}. \begin{coq_example*} +Require Import Arith. Scheme le_ind' := Induction for le Sort Prop. Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q. Proof. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index fa909b607a..08b5275882 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -23,9 +23,9 @@ %\includeonly{RefMan-gal.v,RefMan-ltac.v,RefMan-lib.v,Cases.v} -\input{./version.tex} -\input{./macros.tex}% extension .tex pour htmlgen -\input{./title.tex}% extension .tex pour htmlgen +\input{../common/version.tex} +\input{../common/macros.tex}% extension .tex pour htmlgen +\input{../common/title.tex}% extension .tex pour htmlgen \input{./headers.tex}% extension .tex pour htmlgen \begin{document} @@ -36,6 +36,11 @@ \tophtml{} %BEGIN LATEX \coverpage{Reference Manual}{The Coq Development Team} + {This material may be distributed only subject to the terms and + conditions set forth in the Open Publication License, v1.0 or later + (the latest version is presently available at + \ahrefurl{http://www.opencontent.org/openpub}). + Options A and B of the licence are {\em not} elected.} %END LATEX %\defaultheaders diff --git a/doc/refman/cover.html b/doc/refman/cover.html index 2a09ea2311..1d2700b1cc 100644 --- a/doc/refman/cover.html +++ b/doc/refman/cover.html @@ -22,7 +22,7 @@ The Coq Proof Assistant
V7.x © INRIA 1999-2004
V8.0 © INRIA 2004-2006
-This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). +This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected.

diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 58b2dc6df9..9fae7495b3 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,15 +3,18 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage[noweb]{coqweb} +\usepackage{coqdoc} -\input{./title} -\input{./macros} +\input{../common/version} +\input{../common/title} +\input{../common/macros} \begin{document} \coverpage{The standard library}% {\ } +{This material is distributed under the terms of the GNU Lesser +General Public License Version 2.1.} \tableofcontents @@ -53,7 +56,7 @@ is also a version of this document in HTML format on the WWW, which you can access from the \Coq\ home page at \texttt{http://coq.inria.fr/library}. -\input{library.coqweb.tex} +\input{library.coqdoc} \end{document} diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template new file mode 100644 index 0000000000..fbed33ccf7 --- /dev/null +++ b/doc/stdlib/index-list.html.template @@ -0,0 +1,275 @@ + + + + +The Coq Standard Library +</head> + +<body> + +<H1>The Coq Standard Library</H1> + +Here is a short description of the Coq standard library, which is +distributed with the system. +It provides a set of modules directly available +through the <tt>Require Import</tt> command. +<p> +The standard library is composed of the following subdirectories: + +<p> + +<dl> + <dt> <b>Init</b>: + The core library (automatically loaded when starting Coq) + <dd> +theories/Init/Notations.v +theories/Init/Datatypes.v +theories/Init/Logic.v +theories/Init/Logic_Type.v +theories/Init/Peano.v +theories/Init/Specif.v +theories/Init/Wf.v +(theories/Init/Prelude.v) + + <dt> <b>Logic</b>: + Classical logic and dependent equality + <dd> +theories/Logic/Classical_Pred_Set.v +theories/Logic/Classical_Pred_Type.v +theories/Logic/Classical_Prop.v +theories/Logic/Classical_Type.v +(theories/Logic/Classical.v) +theories/Logic/Decidable.v +theories/Logic/Eqdep_dec.v +theories/Logic/Eqdep.v +theories/Logic/JMeq.v +theories/Logic/RelationalChoice.v +theories/Logic/ClassicalChoice.v +theories/Logic/ChoiceFacts.v +theories/Logic/ClassicalDescription.v +theories/Logic/ClassicalFacts.v +theories/Logic/Berardi.v +theories/Logic/Diaconescu.v +theories/Logic/Hurkens.v +theories/Logic/ProofIrrelevance.v + + <dt> <b>Arith</b>: + Basic Peano arithmetic + <dd> +theories/Arith/Le.v +theories/Arith/Lt.v +theories/Arith/Plus.v +theories/Arith/Minus.v +theories/Arith/Mult.v +theories/Arith/Gt.v +theories/Arith/Between.v +theories/Arith/Peano_dec.v +theories/Arith/Compare_dec.v +(theories/Arith/Arith.v) +theories/Arith/Min.v +theories/Arith/Max.v +theories/Arith/Compare.v +theories/Arith/Div2.v +theories/Arith/Div.v +theories/Arith/EqNat.v +theories/Arith/Euclid.v +theories/Arith/Even.v +theories/Arith/Bool_nat.v +theories/Arith/Factorial.v +theories/Arith/Wf_nat.v + + <dt> <b>NArith</b>: + Binary positive integers + <dd> + +theories/NArith/BinPos.v +theories/NArith/BinNat.v +(theories/NArith/NArith.v) +theories/NArith/Pnat.v + + <dt> <b>ZArith</b>: + Binary integers + <dd> +theories/ZArith/BinInt.v +theories/ZArith/Zorder.v +theories/ZArith/Zcompare.v +theories/ZArith/Znat.v +theories/ZArith/Zmin.v +theories/ZArith/Zabs.v +theories/ZArith/Zeven.v +theories/ZArith/auxiliary.v +theories/ZArith/ZArith_dec.v +theories/ZArith/Zbool.v +theories/ZArith/Zmisc.v +theories/ZArith/Wf_Z.v +theories/ZArith/Zhints.v +(theories/ZArith/ZArith_base.v) +theories/ZArith/Zcomplements.v +theories/ZArith/Zsqrt.v +theories/ZArith/Zpower.v +theories/ZArith/Zdiv.v +theories/ZArith/Zlogarithm.v +(theories/ZArith/ZArith.v) +theories/ZArith/Zwf.v +theories/ZArith/Zbinary.v +theories/ZArith/Znumtheory.v + + <dt> <b>Reals</b>: + Formalization of real numbers + <dd> +theories/Reals/Rdefinitions.v +theories/Reals/Raxioms.v +theories/Reals/RIneq.v +theories/Reals/DiscrR.v +(theories/Reals/Rbase.v) +theories/Reals/RList.v +theories/Reals/Ranalysis.v +theories/Reals/Rbasic_fun.v +theories/Reals/Rderiv.v +theories/Reals/Rfunctions.v +theories/Reals/Rgeom.v +theories/Reals/R_Ifp.v +theories/Reals/Rlimit.v +theories/Reals/Rseries.v +theories/Reals/Rsigma.v +theories/Reals/R_sqr.v +theories/Reals/Rtrigo_fun.v +theories/Reals/Rtrigo.v +theories/Reals/SplitAbsolu.v +theories/Reals/SplitRmult.v +theories/Reals/Alembert.v +theories/Reals/AltSeries.v +theories/Reals/ArithProp.v +theories/Reals/Binomial.v +theories/Reals/Cauchy_prod.v +theories/Reals/Cos_plus.v +theories/Reals/Cos_rel.v +theories/Reals/Exp_prop.v +theories/Reals/Integration.v +theories/Reals/MVT.v +theories/Reals/NewtonInt.v +theories/Reals/PSeries_reg.v +theories/Reals/PartSum.v +theories/Reals/R_sqrt.v +theories/Reals/Ranalysis1.v +theories/Reals/Ranalysis2.v +theories/Reals/Ranalysis3.v +theories/Reals/Ranalysis4.v +theories/Reals/Rcomplete.v +theories/Reals/RiemannInt.v +theories/Reals/RiemannInt_SF.v +theories/Reals/Rpower.v +theories/Reals/Rprod.v +theories/Reals/Rsqrt_def.v +theories/Reals/Rtopology.v +theories/Reals/Rtrigo_alt.v +theories/Reals/Rtrigo_calc.v +theories/Reals/Rtrigo_def.v +theories/Reals/Rtrigo_reg.v +theories/Reals/SeqProp.v +theories/Reals/SeqSeries.v +theories/Reals/Sqrt_reg.v +(theories/Reals/Reals.v) + + <dt> <b>Bool</b>: + Booleans (basic functions and results) + <dd> +theories/Bool/Bool.v +theories/Bool/BoolEq.v +theories/Bool/DecBool.v +theories/Bool/IfProp.v +theories/Bool/Sumbool.v +theories/Bool/Zerob.v +theories/Bool/Bvector.v + + <dt> <b>Lists</b>: + Polymorphic lists, Streams (infinite sequences) + <dd> +theories/Lists/List.v +theories/Lists/ListSet.v +theories/Lists/TheoryList.v +theories/Lists/Streams.v +theories/Lists/MonoList.v + + <dt> <b>Sets</b>: + Sets (classical, constructive, finite, infinite, powerset, + etc.) + <dd> +theories/Sets/Classical_sets.v +theories/Sets/Constructive_sets.v +theories/Sets/Cpo.v +theories/Sets/Ensembles.v +theories/Sets/Finite_sets_facts.v +theories/Sets/Finite_sets.v +theories/Sets/Image.v +theories/Sets/Infinite_sets.v +theories/Sets/Integers.v +theories/Sets/Multiset.v +theories/Sets/Partial_Order.v +theories/Sets/Permut.v +theories/Sets/Powerset_Classical_facts.v +theories/Sets/Powerset_facts.v +theories/Sets/Powerset.v +theories/Sets/Relations_1_facts.v +theories/Sets/Relations_1.v +theories/Sets/Relations_2_facts.v +theories/Sets/Relations_2.v +theories/Sets/Relations_3_facts.v +theories/Sets/Relations_3.v +theories/Sets/Uniset.v + + <dt> <b>Relations</b>: + Relations (definitions and basic results) + <dd> +theories/Relations/Relation_Definitions.v +theories/Relations/Relation_Operators.v +theories/Relations/Relations.v +theories/Relations/Operators_Properties.v +theories/Relations/Rstar.v +theories/Relations/Newman.v + + <dt> <b>Wellfounded</b>: + Well-founded Relations + <dd> +theories/Wellfounded/Disjoint_Union.v +theories/Wellfounded/Inclusion.v +theories/Wellfounded/Inverse_Image.v +theories/Wellfounded/Lexicographic_Exponentiation.v +theories/Wellfounded/Lexicographic_Product.v +theories/Wellfounded/Transitive_Closure.v +theories/Wellfounded/Union.v +theories/Wellfounded/Wellfounded.v +theories/Wellfounded/Well_Ordering.v + + <dt> <b>Sorting</b>: + Axiomatizations of sorts + <dd> +theories/Sorting/Heap.v +theories/Sorting/Permutation.v +theories/Sorting/Sorting.v + + <dt> <b>Setoids</b>: + <dd> +theories/Setoids/Setoid.v + + <dt> <b>IntMap</b>: + Finite sets/maps as trees indexed by addresses + <dd> +theories/IntMap/Addr.v +theories/IntMap/Adist.v +theories/IntMap/Addec.v +theories/IntMap/Adalloc.v +theories/IntMap/Map.v +theories/IntMap/Fset.v +theories/IntMap/Mapaxioms.v +theories/IntMap/Mapiter.v +theories/IntMap/Mapcanon.v +theories/IntMap/Mapsubset.v +theories/IntMap/Lsort.v +theories/IntMap/Mapfold.v +theories/IntMap/Mapcard.v +theories/IntMap/Mapc.v +theories/IntMap/Maplists.v +(theories/IntMap/Allmaps.v) + +</dl> diff --git a/doc/stdlib/index-trailer.html b/doc/stdlib/index-trailer.html new file mode 100644 index 0000000000..308b1d01b6 --- /dev/null +++ b/doc/stdlib/index-trailer.html @@ -0,0 +1,2 @@ +</body> +</html> diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files new file mode 100755 index 0000000000..91e3cc3f45 --- /dev/null +++ b/doc/stdlib/make-library-files @@ -0,0 +1,36 @@ +#!/bin/sh + +# Needs COQTOP and GALLINA set + +# On garde la liste de tous les *.v avec dates dans library.files.ls +# Si elle a change depuis la derniere fois ou library.files n'existe pas +# on fabrique des .g (si besoin) et la liste library.files dans +# l'ordre de ls -tr des *.vo +# Ce dernier trie les fichiers dans l'ordre inverse de leur date de création +# En supposant que make fait son boulot, ca fait un tri topologique du +# graphe des dépendances + +LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists IntMap Relations Sets Sorting Wellfounded Setoids" + +rm -f library.files.ls.tmp +(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp +if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then + mv -f library.files.ls.tmp library.files.ls + rm -f library.files; touch library.files + ABSOLUTE=`pwd`/library.files + cd $COQTOP/theories + echo $LIBDIRS + for rep in $LIBDIRS ; do + (cd $rep + echo $rep/intro.tex >> $ABSOLUTE + VOFILES=`ls -tr *.vo` + for file in $VOFILES ; do + VF=`basename $file \.vo` + if [ \( ! -e $VF.g \) -o \( $VF.v -nt $VF.g \) ] ; then + $GALLINA $VF.v + fi + echo $rep/$VF.g >> $ABSOLUTE + done + ) + done +fi diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index new file mode 100755 index 0000000000..1da642df31 --- /dev/null +++ b/doc/stdlib/make-library-index @@ -0,0 +1,32 @@ +#!/bin/sh + +# Instantiate links to library files in index template + +FILE=$1 + +cp -f $FILE.template tmp +echo -n Building file index-list.prehtml ... +for i in $COQTOP/theories/*; do + d=`basename $i` + if [ "$d" != "Num" -a "$d" != "CVS" ]; then + for j in $i/*.v; do + b=`basename $j .v` + rm -f tmp2 + grep -q theories/$d/$b.v tmp + a=$? + if [ $a = 0 ]; then + sed -e "s/theories\/$d\/$b.v/<a href=\"Coq.$d.$b.html\">$b<\/a>/g" tmp > tmp2 + mv -f tmp2 tmp + else + echo Warning: theories/$d/$b.v is missing in the template file + fi + done + fi + rm -f tmp2 + sed -e "s/#$d#//" tmp > tmp2 + mv -f tmp2 tmp +done +a=`grep theories tmp` +if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi +mv tmp $FILE +echo Done diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index c5b977628f..7909e20f76 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1,16 +1,16 @@ -\documentclass[11pt]{book} +\documentclass[11pt,a4paper]{book} \usepackage[T1]{fontenc} \usepackage[latin1]{inputenc} \usepackage{pslatex} -\input{./version.tex} -\input{./macros.tex} -\input{./title.tex} +\input{../common/version.tex} +\input{../common/macros.tex} +\input{../common/title.tex} %\makeindex \begin{document} -\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring} +\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{} %\tableofcontents -- cgit v1.2.3