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

6 files changed, 70 insertions, 64 deletions

diff --git a/Makefile b/Makefile
index 6edd5ca47d..45a91e1e00 100644
--- a/Makefile
+++ b/Makefile
@@ -1240,19 +1240,25 @@ install-latex:
 # Literate programming (with ocamlweb)
 ###########################################################################
 
-.PHONY: doc
+.PHONY: doc devdoc
 
-doc: doc/coq.tex
-	$(MAKE) -C doc coq.ps minicoq.dvi
+doc: coq
+	(cd doc; make all)
 
-doc/coq.tex:
+clean::
+	(cd doc; make clean)
+
+devdoc: dev/doc/coq.tex
+	$(MAKE) -C dev/doc coq.ps minicoq.dvi
+
+dev/doc/coq.tex:
 	ocamlweb -p "\usepackage{epsfig}" \
-	doc/macros.tex doc/intro.tex \
+	dev/doc/macros.tex dev/doc/intro.tex \
 	lib/{doc.tex,*.mli} kernel/{doc.tex,*.mli} library/{doc.tex,*.mli} \
 	pretyping/{doc.tex,*.mli} interp/{doc.tex,*.mli} \
 	parsing/{doc.tex,*.mli} proofs/{doc.tex,*.mli} \
 	tactics/{doc.tex,*.mli} toplevel/{doc.tex,*.mli} \
-	-o doc/coq.tex
+	-o dev/doc/coq.tex
 
 clean::
 	rm -f doc/coq.tex
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;\
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5fcee708f8..f4adc6e9c2 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1,7 +1,8 @@
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\documentclass[a4paper]{article}
-\else
+\RequirePackage{ifpdf}
+\ifpdf   % si on est en pdflatex
 \documentclass[a4paper,pdftex]{article}
+\else
+\documentclass[a4paper]{article}
 \fi
 \pagestyle{plain}
 
@@ -15,10 +16,10 @@
 \usepackage[latin1]{inputenc}
 \usepackage[english]{babel}
 
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-  \usepackage[dvips]{graphicx}
-\else
+\ifpdf   % si on est en pdflatex
   \usepackage[pdftex]{graphicx}
+\else
+  \usepackage[dvips]{graphicx}
 \fi
 
 %\input{../macros.tex}
@@ -475,10 +476,10 @@ proofs can be found in directory {\tt Logic} of the standard library.
 
 %HEVEA\imgsrc{axioms.png}
 %BEGIN LATEX
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\includegraphics[width=1.0\textwidth]{axioms.eps}
-\else
+\ifpdf   % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{axioms.png}
+\else
+\includegraphics[width=1.0\textwidth]{axioms.eps}
 \fi
 %END LATEX
 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index d1497f1620..ea19f3de45 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -19,10 +19,10 @@ obviously no meaning for \CoqIDE{} being ignored.
 \begin{center}
 %HEVEA\imgsrc{coqide.png}
 %BEGIN LATEX
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\includegraphics[width=1.0\textwidth]{coqide.eps}
-\else
+\ifpdf   % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide.eps}
 \fi
 %END LATEX
 \end{center}
@@ -124,10 +124,10 @@ arguments.
 \begin{center}
 %HEVEA\imgsrc{coqide-queries.png}
 %BEGIN LATEX
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
-\else
+\ifpdf  % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide-queries.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
 \fi
 %END LATEX
 \end{center}
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index ddc4b46ffb..b125720d34 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -1,8 +1,10 @@
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\documentclass[11pt,a4paper]{book}
+\RequirePackage{ifpdf}
+\ifpdf
+  \documentclass[11pt,a4paper,pdftex]{book}
 \else
-\documentclass[11pt,a4paper,pdftex]{book}
+  \documentclass[11pt,a4paper]{book}
 \fi
+
 \usepackage[latin1]{inputenc}
 \usepackage[T1]{fontenc}
 \usepackage{times}
@@ -13,11 +15,13 @@
 \usepackage{alltt}
 \usepackage{hevea}
 
+\usepackage{ifpdf}
+
 % for coqide
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-  \usepackage[dvips]{graphicx}
-\else
+\ifpdf   % si on est pas en pdflatex
   \usepackage[pdftex]{graphicx}
+\else
+  \usepackage[dvips]{graphicx}
 \fi
 
 
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index edda403aad..ee14589cf3 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -28,26 +28,25 @@ of this library). It provides a set of modules directly available
 through the \verb!Require! command.
 
 The standard library is composed of the following subdirectories:
-\medskip
-\begin{tabular}{lp{12cm}}
-  {\bf Logic}   & Classical logic and dependent equality \\
-  {\bf Bool}    & Booleans (basic functions and results) \\
-  {\bf Arith}   & Basic Peano arithmetic \\
-  {\bf ZArith}  & Basic integer arithmetic \\
-  {\bf Reals}   & Classical Real Numbers and Analysis \\
-  {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
+\begin{description}
+  \item[Logic]  Classical logic and dependent equality
+  \item[Bool]   Booleans (basic functions and results)
+  \item[Arith]  Basic Peano arithmetic
+  \item[ZArith] Basic integer arithmetic
+  \item[Reals]  Classical Real Numbers and Analysis
+  \item[Lists]  Monomorphic and polymorphic lists (basic functions and
                   results), Streams (infinite sequences defined 
-                  with co-inductive types) \\
-  {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
-                  etc.) \\
-  {\bf Relations}   & Relations (definitions and basic results). \\
-  {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness). \\
-  {\bf Wellfounded} & Well-founded relations (basic results). \\
-  {\bf IntMap}      & Representation of finite sets by an efficient
-                      structure of map (trees indexed by binary integers).\\
-
-\end{tabular}
-\medskip
+                  with co-inductive types)
+  \item[Sets]   Sets (classical, constructive, finite, infinite, power set,
+                  etc.)
+  \item[Relations] Relations (definitions and basic results).
+  \item[Sorting] Sorted list (basic definitions and heapsort
+                 correctness). 
+  \item[Wellfounded] Well-founded relations (basic results).
+  \item[IntMap]       Representation of finite sets by an efficient
+                     structure of map (trees indexed by binary integers).
+\end{description}
+
 
 Each of these subdirectories contains a set of modules, whose
 specifications (\gallina{} files) have