Move documentation to Sphinx (fix #441)
To build the HTML documentation, run sphinx-build -b html doc somewhere_else
. This might require a version of Sphinx more recent than the one packaged in Debian and Ubuntu; if so, it can be installed using pip3 install sphinx sphinxcontrib-bibtex
.
Currently, the doc
directory contains both .rst
and .tex
files. To help with the transition, choose two related files, e.g., starting.rst
and starting.tex
, and fix any discrepancy between those files. The following checklist shows the files that have been fully converted from .tex
to .rst
:
-
index.rst
(manual.tex
) -
foreword.rst
(manual.tex
) -
starting.rst
-
whyml.rst
-
api.rst
-
install.rst
-
manpages.rst
-
syntaxref.rst
-
exec.rst
-
itp.rst
(coq.tex
,isabelle.tex
,pvs.tex
) -
technical.rst
-
changes.rst
(manual.tex
)
Extra tasks:
-
Add a directive/role for transformations. -
Make sure the rendering is fine with both Latex and HTML. -
Build the documentation using the continuous integration.