# HG changeset patch # User Adam Chlipala # Date 1357678112 18000 # Node ID a95af5a5999089d29a106b7bc7eb18cebfe07172 # Parent 31258618ef73c34e960eea4abd491351ab5a7e6d Exercises online diff -r 31258618ef73 -r a95af5a59990 Makefile --- a/Makefile Tue Jan 08 14:38:56 2013 -0500 +++ b/Makefile Tue Jan 08 15:48:32 2013 -0500 @@ -52,9 +52,10 @@ cpdt.tgz: hg archive -t tgz $@ -install: cpdt.tgz latex/cpdt.pdf html +install: cpdt.tgz latex/cpdt.pdf latex/exercises.pdf html cp cpdt.tgz staging/ cp latex/cpdt.pdf staging/ + cp latex/exercises.pdf staging/ex/ cp -R html staging/ rsync -az --exclude '*~' staging/* chlipala.net:sites/chlipala/adam/cpdt/ diff -r 31258618ef73 -r a95af5a59990 src/Intro.v --- a/src/Intro.v Tue Jan 08 14:38:56 2013 -0500 +++ b/src/Intro.v Tue Jan 08 15:48:32 2013 -0500 @@ -173,8 +173,7 @@ Coq is a very complex system, with many different commands driven more by pragmatic concerns than by any overarching aesthetic principle. When I use some construct for the first time, I try to give a one-sentence intuition for what it accomplishes, but I leave the details to the Coq reference manual%~\cite{CoqManual}%. I expect that readers interested in complete understanding will be consulting that manual frequently; in that sense, this book is not meant to be completely standalone. I often use constructs in code snippets without first introducing them at all, but explanations should always follow in the prose paragraphs immediately after the offending snippets. -Previous versions of the book included some suggested exercises at the ends of chapters. Since then, I have decided to remove the exercises and focus on the main book exposition. Especially in the domain of interactive theorem proving, keeping exercises at the proper difficulty level is a lot of work, I have learned! My advice to readers is to learn to use Coq by getting started applying it in their own real projects, rather than focusing on artificial exercises. -*) +Previous versions of the book included some suggested exercises at the ends of chapters. Since then, I have decided to remove the exercises and focus on the main book exposition. A database of exercises proposed by various readers of the book is ##available on the Web##%\footnote{\url{http://adam.chlipala.net/cpdt/ex/}}%. I do want to suggest, though, that the best way to learn Coq is to get started applying it in a real project, rather than focusing on artificial exercises. *) (** ** On the Tactic Library *) diff -r 31258618ef73 -r a95af5a59990 staging/ex/index.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/staging/ex/index.html Tue Jan 08 15:48:32 2013 -0500 @@ -0,0 +1,20 @@ + + + +Certified Programming with Dependent Types Exercises + +

Certified Programming with Dependent Types Exercises

+ +
+

Here lies an attempt to crowdsource the production of exercises for CPDT.

+
+ +
+

Suggested Exercises

+ +
+ + diff -r 31258618ef73 -r a95af5a59990 staging/index.html --- a/staging/index.html Tue Jan 08 14:38:56 2013 -0500 +++ b/staging/index.html Tue Jan 08 15:48:32 2013 -0500 @@ -29,6 +29,10 @@
+

Online Collection of Exercises for the Book

+
+ +

Used by: