# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1221254291 14400
# Node ID fd18331e5c0b30bf597da75fc955ed570ddaf542
# Parent  95e24b629ad9ddc8ee9ff20e3be610d7fbe91e79
Publishing to the web

diff -r 95e24b629ad9 -r fd18331e5c0b .hgignore
--- a/.hgignore	Fri Sep 12 16:55:37 2008 -0400
+++ b/.hgignore	Fri Sep 12 17:18:11 2008 -0400
@@ -15,3 +15,6 @@
 html/*.html
 
 templates/*.v
+
+staging/html/.dir
+cpdt.tgz
diff -r 95e24b629ad9 -r fd18331e5c0b Makefile
--- a/Makefile	Fri Sep 12 16:55:37 2008 -0400
+++ b/Makefile	Fri Sep 12 17:18:11 2008 -0400
@@ -8,7 +8,7 @@
 GLOBALS       := .coq_globals
 TEMPLATES     := $(MODULES_CODE:%=templates/%.v)
 
-.PHONY: coq clean doc dvi html templates
+.PHONY: coq clean doc dvi html templates install
 
 coq: Makefile.coq
 	make -f Makefile.coq
@@ -40,10 +40,11 @@
 latex/cpdt.pdf: latex/cpdt.dvi
 	cd latex ; pdflatex cpdt
 
-html: Makefile $(VS)
-	cd src ; coqdoc $(VS_DOC) -toc \
+html: Makefile $(VS) src/toc.html
+	cd src ; coqdoc $(VS_DOC) \
 		--glob-from ../$(GLOBALS) \
 		-d ../html
+	cp src/toc.html html/
 
 dvi:
 	xdvi latex/cpdt
@@ -52,3 +53,12 @@
 
 templates/%.v: src/%.v
 	ocaml tools/make_template.ml <$< >$@
+
+cpdt.tgz:
+	hg archive -t tgz $@
+
+install: cpdt.tgz latex/cpdt.pdf html
+	cp cpdt.tgz staging/
+	cp latex/cpdt.pdf staging/
+	cp -R html staging/
+	rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/
diff -r 95e24b629ad9 -r fd18331e5c0b src/InductiveTypes.v
--- a/src/InductiveTypes.v	Fri Sep 12 16:55:37 2008 -0400
+++ b/src/InductiveTypes.v	Fri Sep 12 17:18:11 2008 -0400
@@ -1098,9 +1098,9 @@
 
 %\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe].  [Yes] stands for certain truth, [False] for certain falsehood, and [Maybe] for an unknown situation.  Define "not," "and," and "or" for this replacement boolean algebra.  Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li>#
 
-%\item%#<li># Modify the first example language of Chapter 1 to include variables, where variables are represented with [nat].  Extend the syntax and semantics of expressions to accommodate the change.  Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable.  Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant.  Prove that constant folding preserves the meanings of expressions.#</li>#
+%\item%#<li># Modify the first example language of Chapter 2 to include variables, where variables are represented with [nat].  Extend the syntax and semantics of expressions to accommodate the change.  Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable.  Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant.  Prove that constant folding preserves the meanings of expressions.#</li>#
 
-%\item%#<li># Reimplement the second example language of Chapter 1 to use mutually-inductive types instead of dependent types.  That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type.  To keep things simple, you may consider only the binary operators that take naturals as operands.  Add natural number variables to the language, as in the last exercise, and add an "if" expression form taking as arguments one boolean expression and two natural number expressions.  Define semantics and constant-folding functions for this new language.  Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also "if" expressions with known values for their test expressions but possibly undetermined "then" and "else" cases.  Prove that constant-folding a natural number expression preserves its meaning.#</li>#
+%\item%#<li># Reimplement the second example language of Chapter 2 to use mutually-inductive types instead of dependent types.  That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type.  To keep things simple, you may consider only the binary operators that take naturals as operands.  Add natural number variables to the language, as in the last exercise, and add an "if" expression form taking as arguments one boolean expression and two natural number expressions.  Define semantics and constant-folding functions for this new language.  Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also "if" expressions with known values for their test expressions but possibly undetermined "then" and "else" cases.  Prove that constant-folding a natural number expression preserves its meaning.#</li>#
 
 %\item%#<li># Using a reflexive inductive definition, define a type [nat_tree] of infinitary trees, with natural numbers at their leaves and a countable infinity of new trees branching out of each internal node.  Define a function [increment] that increments the number in every leaf of a [nat_tree].  Define a function [leapfrog] over a natural [i] and a tree [nt].  [leapfrog] should recurse into the [i]th child of [nt], the [i+1]st child of that node, the [i+2]nd child of the next node, and so on, until reaching a leaf, in which case [leapfrog] should return the number at that leaf.  Prove that the result of any call to [leapfrog] is incremented by one by calling [increment] on the tree.#</li>#
 
diff -r 95e24b629ad9 -r fd18331e5c0b src/Intro.v
--- a/src/Intro.v	Fri Sep 12 16:55:37 2008 -0400
+++ b/src/Intro.v	Fri Sep 12 17:18:11 2008 -0400
@@ -167,7 +167,7 @@
 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>#
+%\begin{center}\url{http://adam.chlipala.net/cpdt/html/toc.html}\end{center}%#<blockquote><tt><a href="http://adam.chlipala.net/cpdt/html/toc.html">http://adam.chlipala.net/cpdt/html/toc.html</a></tt></blockquote>#
 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>#
 
diff -r 95e24b629ad9 -r fd18331e5c0b src/toc.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/toc.html	Fri Sep 12 17:18:11 2008 -0400
@@ -0,0 +1,11 @@
+<html><head>
+<title>Certified Programming with Dependent Types</title>
+</head><body>
+
+<h1>Certified Programming with Dependent Types</h1>
+
+<li><a href="Intro.html">Introduction</a>
+<li><a href="StackMachine.html">Some Quick Examples</a>
+<li><a href="InductiveTypes.html">Inductive Types</a>
+
+</body></html>
diff -r 95e24b629ad9 -r fd18331e5c0b staging/index.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/staging/index.html	Fri Sep 12 17:18:11 2008 -0400
@@ -0,0 +1,22 @@
+<html>
+<head>
+<link rel="stylesheet" type="text/css" href="/style.css">
+<title>Certified Programming with Dependent Types</title>
+</head><body>
+<h1>Certified Programming with Dependent Types</h1>
+<h2><a href="/">Adam Chlipala</a></h2>
+
+<div class="summary">
+<p>This is the web site for an in-progress textbook about practical engineering with <a href="http://coq.inria.fr/">the Coq proof assistant</a>.  The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p>
+
+<p>This is the text for a <a href="http://www.cs.harvard.edu/~adamc/cpdt/">Fall 2008 class at Harvard</a>.</p>
+</div>
+
+<div class="project">
+<ul>
+<li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
+<li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li>
+<li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
+</div>
+
+</body></html>