Commit e319df40 authored by Adam Chlipala's avatar Adam Chlipala

Exercises online

parent f0916dd9
......@@ -52,9 +52,10 @@ templates/%.v: src/%.v tools/make_template.ml
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/
......
......@@ -173,8 +173,7 @@ Readers with no prior Coq experience can ignore the preceding discussion! I hop
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 #<a href="http://adam.chlipala.net/cpdt/ex/">#available on the Web#</a>#%\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 *)
......
<html>
<head>
<link rel="stylesheet" type="text/css" href="/style.css">
<title>Certified Programming with Dependent Types Exercises</title>
</head><body>
<h1><a href="..">Certified Programming with Dependent Types</a> Exercises</h1>
<div class="summary">
<p>Here lies an attempt to crowdsource the production of exercises for CPDT.</p>
</div>
<div class="project">
<h2>Suggested Exercises</h2>
<ul>
<li> <a href="exercises.pdf">Snapshot of exercises that were included in CPDT when I decided to stop maintaining exercises</a> (<a href="http://adam.chlipala.net/">Adam Chlipala</a>)</li>
<li> <a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/">Homeworks from CIS 670 at Penn in Fall 2012</a> (<a href="http://www.cis.upenn.edu/~bcpierce/">Benjamin Pierce</a> and students in the class)</li>
</ul>
</div>
</body></html>
......@@ -28,6 +28,10 @@
</ul>
</div>
<div class="project">
<h2><a href="ex/">Online Collection of Exercises for the Book</a></h2>
</div>
<div class="project">
<h2>Used by:</h2>
<ul>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment