# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220279140 14400
# Node ID 7ac7f922e78e8df18188ca83668070c7fdf42627
# Parent  6cc7a8fd4a8cbd6b4dd7f6bdda4963759b36f853
First cut at Intro done

diff -r 6cc7a8fd4a8c -r 7ac7f922e78e book/Makefile
--- a/book/Makefile	Mon Sep 01 10:00:09 2008 -0400
+++ b/book/Makefile	Mon Sep 01 10:25:40 2008 -0400
@@ -21,7 +21,7 @@
 	rm -f Makefile.coq .depend $(GLOBALS) \
 		latex/*.sty latex/cpdt.*
 
-doc: latex/cpdt.dvi html
+doc: latex/cpdt.dvi latex/cpdt.pdf html
 
 latex/cpdt.tex: $(VS)
 	cd src ; coqdoc --latex $(VS_DOC) \
@@ -31,6 +31,9 @@
 latex/cpdt.dvi: latex/cpdt.tex
 	cd latex ; latex cpdt ; latex cpdt
 
+latex/cpdt.pdf: latex/cpdt.dvi
+	cd latex ; pdflatex cpdt
+
 html: $(VS)
 	cd src ; coqdoc $(VS_DOC) -toc \
 		--glob-from ../$(GLOBALS) \
diff -r 6cc7a8fd4a8c -r 7ac7f922e78e book/src/Intro.v
--- a/book/src/Intro.v	Mon Sep 01 10:00:09 2008 -0400
+++ b/book/src/Intro.v	Mon Sep 01 10:25:40 2008 -0400
@@ -138,3 +138,22 @@
 
 A good portion of the book is about how to formalize programming languages, compilers, and proofs about them.  I depart significantly from today's most popular methodology for pencil-and-paper formalism among programming languages researchers.  There is no need to be familiar with operational semantics, preservation and progress theorems, or any of the material found in courses on programming language semantics but not in basic discrete math and logic courses.  I will use operational semantics very sparingly, and there will be no preservation or progress proofs.  Instead, I will use a style that seems to work much better in Coq, which can be given the fancy-sounding name %\textit{%#<i>#foundational type-theoretic semantics#</i>#%}% or the more populist name %\textit{%#<i>#semantics by definitional compilers#</i>#%}%.
 *)
+
+
+(** * Using This Book *)
+
+(**
+This book is generated automatically from Coq source files using the wonderful coqdoc program.  The latest PDF version is available at:
+%\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.  This chapter is headed "Module Intro" because it comes from a module named [Intro], which comes from a fascinating source file %\texttt{%#<tt>#Intro.v#</tt>#%}% containing nothing but specially-formatted coqdoc comments.
+
+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>#
+
+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.
+
+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.
+*)