From e8a88a294f02217e0c66656dfd1bc3b5646e8517 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 11 Mar 2018 00:06:12 +0100 Subject: [Sphinx] Move introduction to new infrastructure --- Makefile.doc | 2 +- doc/refman/RefMan-int.tex | 143 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/introduction.rst | 143 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 144 insertions(+), 145 deletions(-) delete mode 100644 doc/refman/RefMan-int.tex create mode 100644 doc/sphinx/introduction.rst diff --git a/Makefile.doc b/Makefile.doc index a98f35a1c..587c5ccbf 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -70,7 +70,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ + RefMan-pre.tex RefMan-com.tex \ RefMan-uti.tex RefMan-ide.tex RefMan-modr.tex \ AsyncProofs.tex RefMan-ssr.tex) \ $(REFMANCOQTEXFILES) \ diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex deleted file mode 100644 index f802a3595..000000000 --- a/doc/refman/RefMan-int.tex +++ /dev/null @@ -1,143 +0,0 @@ -%BEGIN LATEX -\setheaders{Introduction} -%END LATEX -\chapter*{Introduction} -%HEVEA\cutname{introduction.html} - -This document is the Reference Manual of version \coqversion{} of the \Coq\ -proof assistant. A companion volume, the \Coq\ Tutorial, is provided -for the beginners. It is advised to read the Tutorial first. -A book~\cite{CoqArt} on practical uses of the \Coq{} system was published in 2004 and is a good support for both the beginner and -the advanced user. - -%The system \Coq\ is designed to develop mathematical proofs. It can be -%used by mathematicians to develop mathematical theories and by -%computer scientists to write formal specifications, -The \Coq{} system is designed to develop mathematical proofs, and -especially to write formal specifications, programs and to verify that -programs are correct with respect to their specification. It provides -a specification language named \gallina. Terms of \gallina\ can -represent programs as well as properties of these programs and proofs -of these properties. Using the so-called \textit{Curry-Howard - isomorphism}, programs, properties and proofs are formalized in the -same language called \textit{Calculus of Inductive Constructions}, -that is a $\lambda$-calculus with a rich type system. All logical -judgments in \Coq\ are typing judgments. The very heart of the Coq -system is the type-checking algorithm that checks the correctness of -proofs, in other words that checks that a program complies to its -specification. \Coq\ also provides an interactive proof assistant to -build proofs using specific programs called \textit{tactics}. - -All services of the \Coq\ proof assistant are accessible by -interpretation of a command language called \textit{the vernacular}. - -\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. - -\begin{itemize} -\item 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 {\tt coqtop} command from the operating system (which we shall - assume to be some variety of UNIX in the rest of this document). -\item 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 {\tt coqc} command from the operating system. - -\end{itemize} -These two modes are documented in Chapter~\ref{Addoc-coqc}. - -Other modes of interaction with \Coq{} are possible: through an emacs -shell window, an emacs generic user-interface for proof assistant -({\ProofGeneral}~\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 -Chapter~\ref{Addoc-coqide}. - -\section*{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. - -\begin{itemize} -\item The first part describes the specification language, - Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension} - describe the concrete syntax as well as the meaning of programs, - theorems and proofs in the Calculus of Inductive - Constructions. Chapter~\ref{Theories} describes the standard library - of \Coq. Chapter~\ref{Cic} is a mathematical description of the - formalism. Chapter~\ref{chapter:Modules} describes the module system. - -\item The second part describes the proof engine. It is divided in - five chapters. Chapter~\ref{Vernacular-commands} presents all - commands (we call them \emph{vernacular commands}) that are not - directly related to interactive proving: requests to the - environment, complete or partial evaluation, loading and compiling - files. How to start and stop proofs, do multiple proofs in parallel - is explained in Chapter~\ref{Proof-handling}. In - Chapter~\ref{Tactics}, all commands that realize one or more steps - of the proof are presented: we call them \emph{tactics}. The - language to combine these tactics into complex proof strategies is - given in Chapter~\ref{TacticLanguage}. Examples of tactics are - described in Chapter~\ref{Tactics-examples}. - -%\item The third part describes how to extend the system in two ways: -% adding parsing and pretty-printing rules -% (Chapter~\ref{Addoc-syntax}) and writing new tactics -% (Chapter~\ref{TacticLanguage}). - -\item The third part describes how to extend the syntax of \Coq. It -corresponds to the Chapter~\ref{Addoc-syntax}. - -\item In the fourth part more practical tools are documented. First in - Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode) - and \texttt{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{Addoc-coqide} describes the \Coq{} integrated - development environment. - -\item 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. -\end{itemize} - -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error -messages. - -\section*{List of additional documentation} - -This manual does not contain all the documentation the user may need -about \Coq{}. Various informations can be found in the following -documents: -\begin{description} - -\item[Tutorial] - A companion volume to this reference manual, the \Coq{} Tutorial, is - aimed at gently introducing new users to developing proofs in \Coq{} - without assuming prior knowledge of type theory. In a second step, the - user can read also the tutorial on recursive types (document {\tt - RecTutorial.ps}). - -\item[Installation] A text file INSTALL that comes with the sources - explains how to install \Coq{}. - -\item[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 {\tt Library.ps}. - -\end{description} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index fc1c01cf2..1bd79d511 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -85,7 +85,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX %\defaultheaders -\include{RefMan-int}% Introduction \include{RefMan-pre}% Credits %BEGIN LATEX diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst new file mode 100644 index 000000000..f802a3595 --- /dev/null +++ b/doc/sphinx/introduction.rst @@ -0,0 +1,143 @@ +%BEGIN LATEX +\setheaders{Introduction} +%END LATEX +\chapter*{Introduction} +%HEVEA\cutname{introduction.html} + +This document is the Reference Manual of version \coqversion{} of the \Coq\ +proof assistant. A companion volume, the \Coq\ Tutorial, is provided +for the beginners. It is advised to read the Tutorial first. +A book~\cite{CoqArt} on practical uses of the \Coq{} system was published in 2004 and is a good support for both the beginner and +the advanced user. + +%The system \Coq\ is designed to develop mathematical proofs. It can be +%used by mathematicians to develop mathematical theories and by +%computer scientists to write formal specifications, +The \Coq{} system is designed to develop mathematical proofs, and +especially to write formal specifications, programs and to verify that +programs are correct with respect to their specification. It provides +a specification language named \gallina. Terms of \gallina\ can +represent programs as well as properties of these programs and proofs +of these properties. Using the so-called \textit{Curry-Howard + isomorphism}, programs, properties and proofs are formalized in the +same language called \textit{Calculus of Inductive Constructions}, +that is a $\lambda$-calculus with a rich type system. All logical +judgments in \Coq\ are typing judgments. The very heart of the Coq +system is the type-checking algorithm that checks the correctness of +proofs, in other words that checks that a program complies to its +specification. \Coq\ also provides an interactive proof assistant to +build proofs using specific programs called \textit{tactics}. + +All services of the \Coq\ proof assistant are accessible by +interpretation of a command language called \textit{the vernacular}. + +\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. + +\begin{itemize} +\item 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 {\tt coqtop} command from the operating system (which we shall + assume to be some variety of UNIX in the rest of this document). +\item 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 {\tt coqc} command from the operating system. + +\end{itemize} +These two modes are documented in Chapter~\ref{Addoc-coqc}. + +Other modes of interaction with \Coq{} are possible: through an emacs +shell window, an emacs generic user-interface for proof assistant +({\ProofGeneral}~\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 +Chapter~\ref{Addoc-coqide}. + +\section*{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. + +\begin{itemize} +\item The first part describes the specification language, + Gallina. Chapters~\ref{Gallina} and~\ref{Gallina-extension} + describe the concrete syntax as well as the meaning of programs, + theorems and proofs in the Calculus of Inductive + Constructions. Chapter~\ref{Theories} describes the standard library + of \Coq. Chapter~\ref{Cic} is a mathematical description of the + formalism. Chapter~\ref{chapter:Modules} describes the module system. + +\item The second part describes the proof engine. It is divided in + five chapters. Chapter~\ref{Vernacular-commands} presents all + commands (we call them \emph{vernacular commands}) that are not + directly related to interactive proving: requests to the + environment, complete or partial evaluation, loading and compiling + files. How to start and stop proofs, do multiple proofs in parallel + is explained in Chapter~\ref{Proof-handling}. In + Chapter~\ref{Tactics}, all commands that realize one or more steps + of the proof are presented: we call them \emph{tactics}. The + language to combine these tactics into complex proof strategies is + given in Chapter~\ref{TacticLanguage}. Examples of tactics are + described in Chapter~\ref{Tactics-examples}. + +%\item The third part describes how to extend the system in two ways: +% adding parsing and pretty-printing rules +% (Chapter~\ref{Addoc-syntax}) and writing new tactics +% (Chapter~\ref{TacticLanguage}). + +\item The third part describes how to extend the syntax of \Coq. It +corresponds to the Chapter~\ref{Addoc-syntax}. + +\item In the fourth part more practical tools are documented. First in + Chapter~\ref{Addoc-coqc}, the usage of \texttt{coqc} (batch mode) + and \texttt{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{Addoc-coqide} describes the \Coq{} integrated + development environment. + +\item 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. +\end{itemize} + +At the end of the document, after the global index, the user can find +specific indexes for tactics, vernacular commands, and error +messages. + +\section*{List of additional documentation} + +This manual does not contain all the documentation the user may need +about \Coq{}. Various informations can be found in the following +documents: +\begin{description} + +\item[Tutorial] + A companion volume to this reference manual, the \Coq{} Tutorial, is + aimed at gently introducing new users to developing proofs in \Coq{} + without assuming prior knowledge of type theory. In a second step, the + user can read also the tutorial on recursive types (document {\tt + RecTutorial.ps}). + +\item[Installation] A text file INSTALL that comes with the sources + explains how to install \Coq{}. + +\item[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 {\tt Library.ps}. + +\end{description} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3