From f5be988da566d0a48c67bd81be6d32376b3ba2a5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 13 Feb 2020 18:47:42 +0100 Subject: [refman] Move chapters into new structure. As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle --- doc/sphinx/using/libraries/index.rst | 24 ++++++++++++++++++++++++ doc/sphinx/using/tools/index.rst | 20 ++++++++++++++++++++ 2 files changed, 44 insertions(+) create mode 100644 doc/sphinx/using/libraries/index.rst create mode 100644 doc/sphinx/using/tools/index.rst (limited to 'doc/sphinx/using') diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst new file mode 100644 index 0000000000..2228df5ab8 --- /dev/null +++ b/doc/sphinx/using/libraries/index.rst @@ -0,0 +1,24 @@ +.. _libraries: + +===================== +Libraries and plugins +===================== + +Coq is distributed with a standard library and a set of internal +plugins (most of which provide tactics that have already been +presented in :ref:`writing-proofs`). This chapter presents this +standard library and some of these internal plugins which provide +features that are not tactics: + +.. toctree:: + :maxdepth: 1 + + ../../language/coq-library + ../../addendum/extraction + ../../addendum/miscellaneous-extensions + +In addition, Coq has a rich ecosystem of external libraries and +plugins. These libraries and plugins can be browsed online through +the `Coq Package Index `_ and +installed with the `opam package manager +`_. diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst new file mode 100644 index 0000000000..4381c4d63d --- /dev/null +++ b/doc/sphinx/using/tools/index.rst @@ -0,0 +1,20 @@ +.. _tools: + +================================ +Command-line and graphical tools +================================ + +This chapter presents the command-line tools that users will need to +build their Coq project, the documentation of the CoqIDE standalone +user interface and the documentation of the parallel proof processing +feature that is supported by CoqIDE and several other user interfaces. +A list of available user interfaces to interact with Coq is available +on the `Coq website `_. + +.. toctree:: + :maxdepth: 1 + + ../../practical-tools/coq-commands + ../../practical-tools/utilities + ../../practical-tools/coqide + ../../addendum/parallel-proof-processing -- cgit v1.2.3