Mercurial > cpdt > repo
diff src/Intro.v @ 25:26ad686e68f2
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 |
line wrap: on
line diff
--- a/src/Intro.v Mon Sep 08 12:22:22 2008 -0400 +++ b/src/Intro.v Mon Sep 08 12:42:57 2008 -0400 @@ -168,9 +168,6 @@ %\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># There is also an online HTML version available, with a hyperlink from each use of an identifier to that identifier's definition: %\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># - -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>#%}%. - The source code to the book is also freely available at: %\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># @@ -178,3 +175,16 @@ 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. *) + + +(** %\section{Chapter Source Files} + +\begin{center} \begin{tabular}{|r|l|} +\hline +\textbf{Chapter} & \textbf{Source} \\ +\hline +Some Quick Examples & \texttt{StackMachine.v} \\ +\hline +\end{tabular} \end{center} + +% *)