aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.doc
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-06 15:34:14 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-06 15:34:14 +0000
commit2592766937df60484f15d5050e5bfe6623c83390 (patch)
treeeb5c6f7437882f4c85b7b4ca1d340644f426e02f /INSTALL.doc
parent99ceb8c7df67a37330820e3e6fbb4a3ccab2a9a5 (diff)
Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppression de la dépendance envers aeguill (bug #1922)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL.doc')
-rw-r--r--INSTALL.doc81
1 files changed, 81 insertions, 0 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
new file mode 100644
index 000000000..3eb72e08b
--- /dev/null
+++ b/INSTALL.doc
@@ -0,0 +1,81 @@
+ The Coq documentation
+ =====================
+
+The Coq documentation includes
+
+- A Reference Manual
+- A Tutorial
+- A document presenting the Coq standard library
+- A list of questions/answers in the FAQ style
+
+The sources of the documents are mainly made of LaTeX code from which
+user-readable PostScript or PDF files, or a user-browsable bunch of
+html files are generated.
+
+Prerequisite
+------------
+
+To produce the PostScript documents, the following tools
+are needed:
+
+ - latex (latex2e)
+ - dvips
+ - bibtex
+ - makeindex
+ - pngtopnm and pnmtops (for the Reference Manual and the FAQ)
+
+To produce the PDF documents, the following tools are needed:
+
+ - pdflatex
+ - bibtex
+
+To produce the html documents, the following tools are needed:
+
+ - hevea (e.g. 1.07 works)
+
+Compilation
+-----------
+
+To produce all documentation about Coq, just run:
+
+ make doc
+
+
+Alternatively, you can use some specific targets:
+
+ make doc-ps
+ to produce all PostScript documents
+
+ make doc-pdf
+ to produce all PDF documents
+
+ make doc-html
+ to produce all html documents
+
+ make refman
+ to produce all formats of the reference manual
+
+ make tutorial
+ to produce all formats of the tutorial
+
+ make rectutorial
+ to produce all formats of the tutorial on recursive types
+
+ make faq
+ to produce all formats of the FAQ
+
+ make stdlib
+ to produce all formats of the Coq standard library
+
+
+Installation
+------------
+
+To install all produced documents, do:
+
+ make DOCDIR=/some/directory/for/documentation install-doc
+
+DOCDIR defauts to /usr/share/doc/coq-x.y were x.y is the version number
+
+
+