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/language/core/index.rst | 39 ++++++++++++++++++++++++++++++++ doc/sphinx/language/extensions/index.rst | 28 +++++++++++++++++++++++ 2 files changed, 67 insertions(+) create mode 100644 doc/sphinx/language/core/index.rst create mode 100644 doc/sphinx/language/extensions/index.rst (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..c78c0737db --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,39 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter `), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +This chapter is divided in several sub-chapters: + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..5b5c2ab737 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,28 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter `. + +This chapter is divided in several sub-chapters: + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands -- cgit v1.2.3 From 1be31dea4cfd31522898edc07fee0829fea7c68d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 19 Mar 2020 15:51:18 +0100 Subject: Adapt to sub-TOC not showing in PDF output. --- doc/sphinx/language/core/index.rst | 2 -- doc/sphinx/language/extensions/index.rst | 2 -- 2 files changed, 4 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index c78c0737db..07dcfff444 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -27,8 +27,6 @@ users may rely on external plugins that provide advanced and complex tactics without fear of these tactics being buggy, because the kernel will have to check their output. -This chapter is divided in several sub-chapters: - .. toctree:: :maxdepth: 1 diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst index 5b5c2ab737..f22927d627 100644 --- a/doc/sphinx/language/extensions/index.rst +++ b/doc/sphinx/language/extensions/index.rst @@ -13,8 +13,6 @@ chapter, we present these language extensions and we give some explanations on how this language is translated down to the core language presented in the :ref:`previous chapter `. -This chapter is divided in several sub-chapters: - .. toctree:: :maxdepth: 1 -- cgit v1.2.3