Mentions légales du service

Skip to content

Move documentation to Sphinx (fix #441)

Guillaume Melquiond requested to merge sphinx into master

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.
Edited by Guillaume Melquiond

Merge request reports