Mercurial > cpdt > repo

comparison src/Intro.v @ 25:26ad686e68f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Real chapter titles; describe how to get Proof General to use command-line flags
author Adam Chlipala <adamc@hcoop.net>
date Mon, 08 Sep 2008 12:42:57 -0400
parents 00366a62bd00
children 65314ca099ed
comparison
equal deleted inserted replaced
24:aba1a37394c4 25:26ad686e68f2
166 (** 166 (**
167 This book is generated automatically from Coq source files using the wonderful coqdoc program. The latest PDF version is available at: 167 This book is generated automatically from Coq source files using the wonderful coqdoc program. The latest PDF version is available at:
168 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.pdf}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.pdf">http://adam.chlipala.net/cpdt/cpdt.pdf</a></tt></blockquote># 168 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.pdf}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.pdf">http://adam.chlipala.net/cpdt/cpdt.pdf</a></tt></blockquote>#
169 There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition: 169 There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition:
170 %\begin{center}\url{http://adam.chlipala.net/cpdt/html/}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/">http://adam.chlipala.net/cpdt/html/</a></tt></blockquote># 170 %\begin{center}\url{http://adam.chlipala.net/cpdt/html/}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/">http://adam.chlipala.net/cpdt/html/</a></tt></blockquote>#
171
172 The chapters of this book are named like "Module Foo," rather than having proper names, because literally the entire document is generated by coqdoc, which by default bases chapter structure on the module structure of the development being documented. The next chapter is headed "Module StackMachine" because it comes from a module named [StackMachine], which comes from a source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}%.
173
174 The source code to the book is also freely available at: 171 The source code to the book is also freely available at:
175 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote># 172 %\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/cpdt.tgz">http://adam.chlipala.net/cpdt/cpdt.tgz</a></tt></blockquote>#
176 173
177 There, you can find all of the code appearing in this book, with prose interspersed in comments, in exactly the order that you find in this document. You can step through the code interactively with your chosen graphical Coq interface. The code also has special comments indicating which parts of the chapters make suitable starting points for interactive class sessions, where the class works together to construct the programs and proofs. The included Makefile has a target %\texttt{%#<tt>#templates#</tt>#%}% for building a fresh set of class template files automatically from the book source. 174 There, you can find all of the code appearing in this book, with prose interspersed in comments, in exactly the order that you find in this document. You can step through the code interactively with your chosen graphical Coq interface. The code also has special comments indicating which parts of the chapters make suitable starting points for interactive class sessions, where the class works together to construct the programs and proofs. The included Makefile has a target %\texttt{%#<tt>#templates#</tt>#%}% for building a fresh set of class template files automatically from the book source.
178 175
179 I believe that a good graphical interface to Coq is crucial for using it productively. I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#<a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a># mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it. 176 I believe that a good graphical interface to Coq is crucial for using it productively. I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#<a href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a># mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it.
180 *) 177 *)
178
179
180 (** %\section{Chapter Source Files}
181
182 \begin{center} \begin{tabular}{|r|l|}
183 \hline
184 \textbf{Chapter} & \textbf{Source} \\
185 \hline
186 Some Quick Examples & \texttt{StackMachine.v} \\
187 \hline
188 \end{tabular} \end{center}
189
190 % *)