From a321962205a26fac6ec16929636ea748e572905e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sun, 17 Jun 2018 15:00:38 +0200 Subject: Modernize the introduction of the reference manual. --- doc/sphinx/biblio.bib | 12 ----------- doc/sphinx/introduction.rst | 52 ++++++++++++++++++++++----------------------- 2 files changed, 25 insertions(+), 39 deletions(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3e988709c..bb881da04 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -290,18 +290,6 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} -} - @Book{RC95, author = {di~Cosmo, R.}, title = {Isomorphisms of Types: from $\lambda$-calculus to information diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 75ff72c4d..5a628f4ea 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -26,37 +26,35 @@ programs called *tactics*. All services of the |Coq| proof assistant are accessible by interpretation of a command language called *the vernacular*. -Coq has an interactive mode in which commands are interpreted as the +Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file. -- The interactive mode may be used as a debugging mode in which the - user can develop his theories and proofs step by step, backtracking - if needed and so on. The interactive mode is run with the `coqtop` - command from the operating system (which we shall assume to be some - variety of UNIX in the rest of this document). +- In interactive mode, users can develop their theories and proofs step by + step, and query the system for available theorems and definitions. The + interactive mode is generally run with the help of an IDE, such + as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, + Emacs with Proof-General (available at https://proofgeneral.github.io/), + or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). + The `coqtop` read-eval-print-loop can also be used directly, for debugging + purposes. - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the `coqc` - command from the operating system. + command. -These two modes are documented in Chapter :ref:`thecoqcommands`. - -Other modes of interaction with |Coq| are possible: through an emacs shell -window, an emacs generic user-interface for proof assistant (Proof -General :cite:`ProofGeneral`) or through a customized -interface (PCoq :cite:`Pcoq`). These facilities are not -documented here. There is also a |Coq| Integrated Development Environment -described in :ref:`coqintegrateddevelopmentenvironment`. +.. seealso:: :ref:`thecoqcommands`. How to read this book ===================== -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. +This is a Reference Manual, so it is not made for a continuous reading. +We recommend using the various indexes to quickly locate the documentation +you are looking for. There is a global index, and a number of specific indexes +for tactics, vernacular commands, and error messages and warnings. +Nonetheless, the manual has some structure that is explained below. - The first part describes the specification language, |Gallina|. Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete @@ -66,7 +64,7 @@ below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in five +- The second part describes the proof engine. It is divided in six chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -77,24 +75,24 @@ below. *tactics*. The language to combine these tactics into complex proof strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. + Finally, the |SSR| proof language is presented in + Chapter :ref:`thessreflectprooflanguage`. -- The third part describes how to extend the syntax of |Coq|. It - corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. +- The third part describes how to extend the syntax of |Coq| in + Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define + new induction principles in Chapter :ref:`proofschemes`. - In the fourth part more practical tools are documented. First in Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and `coqtop` (interactive mode) with their options is described. Then, in Chapter :ref:`utilities`, various utilities that come with the |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes the |Coq| integrated development environment. + describes CoqIDE. - The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list. -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error messages. - List of additional documentation ================================ @@ -114,5 +112,5 @@ Installation The |Coq| standard library A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is given - in the additional document `Library.ps`. + (including only the specifications, the proofs are removed) is + available at https://coq.inria.fr/stdlib/. -- cgit v1.2.3 From 6631e485b86747bac15a85cd83e0c62d824ce8ce Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 20 Jun 2018 16:16:28 +0200 Subject: Add a good reference for Proof-General as suggested by Clément. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- doc/sphinx/biblio.bib | 15 +++++++++++++++ doc/sphinx/introduction.rst | 2 +- 2 files changed, 16 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index bb881da04..bfa96621f 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 5a628f4ea..73da5e802 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -34,7 +34,7 @@ are processed from a file. step, and query the system for available theorems and definitions. The interactive mode is generally run with the help of an IDE, such as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General (available at https://proofgeneral.github.io/), + Emacs with Proof-General :cite:`Asp00` (available at https://proofgeneral.github.io/), or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. -- cgit v1.2.3 From f8d1207b0d839274fb4358a0a7bd494f019cc681 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 20 Jun 2018 16:59:09 +0200 Subject: Mention Company-Coq as well. We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page. --- doc/sphinx/biblio.bib | 9 +++++++++ doc/sphinx/index.rst | 5 +++++ doc/sphinx/introduction.rst | 2 +- 3 files changed, 15 insertions(+), 1 deletion(-) (limited to 'doc/sphinx') diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index bfa96621f..3574bf675 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -305,6 +305,15 @@ the Calculus of Inductive Constructions}}, year = {1995} } +@InProceedings{Pit16, + Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, + Author = {Pit-Claudel, Clément and Courtieu, Pierre}, + Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, + Year = {2016}, + Month = jan, + Doi = {10.5281/zenodo.44331}, +} + @Book{RC95, author = {di~Cosmo, R.}, title = {Isomorphisms of Types: from $\lambda$-calculus to information diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 136f9088b..7baa4c450 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -81,3 +81,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected. + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 73da5e802..49f5db342 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -34,7 +34,7 @@ are processed from a file. step, and query the system for available theorems and definitions. The interactive mode is generally run with the help of an IDE, such as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, - Emacs with Proof-General :cite:`Asp00` (available at https://proofgeneral.github.io/), + Emacs with Proof-General :cite:`Asp00` [#PG]_, or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. -- cgit v1.2.3