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 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 doc/sphinx/language/core/index.rst (limited to 'doc/sphinx/language/core') 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 -- 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 -- 1 file changed, 2 deletions(-) (limited to 'doc/sphinx/language/core') 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 -- cgit v1.2.3