aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL.doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-08 15:36:27 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-10 19:23:49 +0200
commit012ac80c38d431d68f1dacb01fbfe27bcb7f7eb0 (patch)
treea1dfaf39107e0fee091c3635d98dbd1ef1d1425e /INSTALL.doc
parente559f7553030dc3a86936794d0f80f39b0131960 (diff)
Remove tutorials.
Diffstat (limited to 'INSTALL.doc')
-rw-r--r--INSTALL.doc27
1 files changed, 7 insertions, 20 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
index f8a085280..6b920eea8 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -4,13 +4,13 @@
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.
+The reference manual is written is reStructuredText and compiled
+using Sphinx (see `doc/sphinx/README.rst`) to learn more.
+
+The documentation for the standard library is generated from
+the `.v` source files using coqdoc.
Prerequisite
------------
@@ -22,7 +22,6 @@ To produce all the documents, the following tools are needed:
- dvips
- bibtex
- makeindex
- - hevea
- Python 3
- Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/)
- sphinx_rtd_theme
@@ -35,7 +34,7 @@ Under recent Debian based operating systems (Debian 10 "Buster",
Ubuntu 18.04, ...) a working set of packages for compiling the
documentation for Coq is:
- texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx
+ texlive-latex-extra texlive-fonts-recommended python3-sphinx
python3-pexpect python3-sphinx-rtd-theme python3-bs4
python3-sphinxcontrib.bibtex python3-pip
@@ -75,15 +74,6 @@ Alternatively, you can use some specific targets:
make sphinx
to produce the HTML version 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
@@ -99,7 +89,4 @@ To install all produced documents, do:
make DOCDIR=/some/directory/for/documentation install-doc
-DOCDIR defauts to /usr/share/doc/coq
-
-
-
+DOCDIR defaults to /usr/share/doc/coq