Mercurial > cpdt > repo
changeset 489:a95af5a59990
Exercises online
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Jan 2013 15:48:32 -0500 |
| parents | 31258618ef73 |
| children | c8a3cb24bae9 |
| files | Makefile src/Intro.v staging/ex/index.html staging/index.html |
| diffstat | 4 files changed, 27 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- 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/
--- 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 #<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 *)
--- /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 @@ +<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>
--- 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 @@ </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> <li>CIS 670 at Penn <a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/">(Fall 2012)</a></li>