Mercurial > cpdt > repo

comparison src/Intro.v @ 21:00366a62bd00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper title and copyright pages
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 16:37:51 -0400
parents c0cbf324ec7d
children 26ad686e68f2
comparison
equal deleted inserted replaced
20:c0cbf324ec7d 21:00366a62bd00
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (** %\fi
11
12 \begin{document}
13
14 \maketitle
15
16 \thispagestyle{empty}
17 \mbox{}\vfill
18 \begin{center}% *)
19
10 (** 20 (**
21
22 Copyright Adam Chlipala 2008.
11 23
12 This work is licensed under a 24 This work is licensed under a
13 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 25 Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
14 Unported License. 26 Unported License.
15 The license text is available at: 27 The license text is available at:
16 %\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}% 28 %\begin{center} \url{http://creativecommons.org/licenses/by-nc-nd/3.0/} \end{center}%
17 #<a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">http://creativecommons.org/licenses/by-nc-nd/3.0/</a># 29 #<a href="http://creativecommons.org/licenses/by-nc-nd/3.0/">http://creativecommons.org/licenses/by-nc-nd/3.0/</a>#
18 30
19 *) 31 *)
32
33 (** %\vfill\mbox{}
34 \end{center}
35
36 \tableofcontents
37
38 \chapter{Introduction}% *)
39
40
20 41
21 42
22 (** * Whence This Book? *) 43 (** * Whence This Book? *)
23 44
24 (** 45 (**
146 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:
147 %\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>#
148 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:
149 %\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>#
150 171
151 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. 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>#%}%.
152 173
153 The source code to the book is also freely available at: 174 The source code to the book is also freely available at:
154 %\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># 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>#
155 176
156 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. 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.