# HG changeset patch # User Adam Chlipala # Date 1285954745 14400 # Node ID e7ed2fddd29adcd2c5f635fa89e22dc092c534d7 # Parent a57e75752c80b61004147813d1312576f2ab921d Some improvements to installation instructions, based on Mitch Wand's feedback diff -r a57e75752c80 -r e7ed2fddd29a src/Intro.v --- a/src/Intro.v Tue Sep 21 09:50:33 2010 -0400 +++ b/src/Intro.v Fri Oct 01 13:39:05 2010 -0400 @@ -180,7 +180,9 @@ 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{%##templates##%}% for building a fresh set of class template files automatically from the book source. -I believe that a good graphical interface to Coq is crucial for using it productively. I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#Proof General# mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it. +I believe that a good graphical interface to Coq is crucial for using it productively. I use the %Proof General\footnote{\url{http://proofgeneral.inf.ed.ac.uk/}}%#Proof General# mode for Emacs, which supports a number of other proof assistants besides Coq. There is also the standalone CoqIDE program developed by the Coq team. I like being able to combine certified programming and proving with other kinds of work inside the same full-featured editor, and CoqIDE has had a good number of crashes and other annoying bugs in recent history, though I hear that it is improving. In the initial part of this book, I will reference Proof General procedures explicitly, in introducing how to use Coq, but most of the book will be interface-agnostic, so feel free to use CoqIDE if you prefer it. The one issue with CoqIDE, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] command, which CoqIDE does not support. It would be bad form to leave [Abort] commands lying around in a real, finished development, but I find these commands helpful in writing single source files that trace a user's thought process in designing a proof. + +The next chapter will introduce Coq with some simple examples, and the chapter starts with step-by-step instructions on getting set up to run the book chapters interactively, assuming that you have Coq and Proof General installed. *) diff -r a57e75752c80 -r e7ed2fddd29a src/StackMachine.v --- a/src/StackMachine.v Tue Sep 21 09:50:33 2010 -0400 +++ b/src/StackMachine.v Fri Oct 01 13:39:05 2010 -0400 @@ -19,17 +19,30 @@ (** %\chapter{Some Quick Examples}% *) -(** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines. We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead. I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl1, though parts may work with other versions. +(** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines. We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead. I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions. -As always, you can step through the source file %\texttt{%##StackMachine.v##%}% for this chapter interactively in Proof General. Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%##.v##%}% file in an Emacs buffer. If you do the latter, include two lines [Require Import Arith Bool List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%##coqtop##%}% with the command-line argument %\texttt{%##-I SRC##%}%, where %\texttt{%##SRC##%}% is the path to a directory containing the source for this book. In either case, you will need to run %\texttt{%##make##%}% in the root directory of the source distribution for the book before getting started. If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%##.v##%}% buffer in Emacs. +To set up your Proof General environment to process the source to this chapter, a few simple steps are required. -There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%##coqtop##%}% program. The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\texttt{%##.emacs##%}% file, like this: +%\begin{enumerate}%#
    # + +%\item %#
  1. #Get the book source from +%\begin{center}\url{http://adam.chlipala.net/cpdt/cpdt.tgz}\end{center}%#
    http://adam.chlipala.net/cpdt/cpdt.tgz
    2. # + +%\item %#
  2. #Unpack the tarball to some directory %\texttt{%##DIR##%}%.#
    3. # + +%\item %#
  3. #Run %\texttt{%##make##%}% in %\texttt{%##DIR##%}%.#
    4. # + +%\item %#
  4. #There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%##coqtop##%}% program, which provides the interactive Coq toplevel. The best way to add settings that will be shared by many source files is to add a custom variable setting to your %\texttt{%##.emacs##%}% file, like this: %\begin{verbatim}%#
    #(custom-set-variables
   ...
-  '(coq-prog-args '("-I" "/path/to/cpdt/src"))
+  '(coq-prog-args '("-I" "DIR/src"))
   ...
 )#
    #%\end{verbatim}% -The extra arguments demonstrated here are the proper choices for working with the code for this book. The ellipses stand for other Emacs customization settings you may already have. It can be helpful to save several alternate sets of flags in your %\texttt{%##.emacs##%}% file, with all but one commented out within the %\texttt{%##custom-set-variables##%}% block at any given time. +The extra arguments demonstrated here are the proper choices for working with the code for this book. The ellipses stand for other Emacs customization settings you may already have. It can be helpful to save several alternate sets of flags in your %\texttt{%##.emacs##%}% file, with all but one commented out within the %\texttt{%##custom-set-variables##%}% block at any given time.#
    5. # + +#
#%\end{enumerate}% + +As always, you can step through the source file %\texttt{%##StackMachine.v##%}% for this chapter interactively in Proof General. Alternatively, to get a feel for the whole lifecycle of creating a Coq development, you can enter the pieces of source code in this chapter in a new %\texttt{%##.v##%}% file in an Emacs buffer. If you do the latter, include two lines [Require Import Arith Bool List Tactics.] and [Set Implicit Arguments.] at the start of the file, to match some code hidden in this rendering of the chapter source, and be sure to run the Coq binary %\texttt{%##coqtop##%}% with the command-line argument %\texttt{%##-I DIR/src##%}%. If you have installed Proof General properly, it should start automatically when you visit a %\texttt{%##.v##%}% buffer in Emacs. With Proof General, the portion of a buffer that Coq has processed is highlighted in some way, like being given a blue background. You step through Coq source files by positioning the point at the position you want Coq to run to and pressing C-C C-RET. This can be used both for normal step-by-step coding, by placing the point inside some command past the end of the highlighted region; and for undoing, by placing the point inside the highlighted region. *)