Mercurial > cpdt > repo

comparison src/StackMachine.v @ 269:191a66cd7cb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix PDF ToC generation; mention Set Implicit Arguments in StackMachine
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Feb 2010 08:14:39 -0500
parents b149a07b9b5b
children a636eda02176
comparison
equal deleted inserted replaced
268:f3223bde5c87 269:191a66cd7cb5
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
19 (** %\chapter{Some Quick Examples}% *) 19 (** %\chapter{Some Quick Examples}% *)
20 20
21 21
22 (** 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. 22 (** 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.
23 23
24 As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% 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{%#<tt>#.v#</tt>#%}% file in an Emacs buffer. If you do the latter, include a line [Require Import List Tactics.] 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{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book. In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% 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{%#<tt>#.v#</tt>#%}% buffer in Emacs. 24 As always, you can step through the source file %\texttt{%#<tt>#StackMachine.v#</tt>#%}% 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{%#<tt>#.v#</tt>#%}% file in an Emacs buffer. If you do the latter, include two lines [Require Import 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{%#<tt>#coqtop#</tt>#%}% with the command-line argument %\texttt{%#<tt>#-I SRC#</tt>#%}%, where %\texttt{%#<tt>#SRC#</tt>#%}% is the path to a directory containing the source for this book. In either case, you will need to run %\texttt{%#<tt>#make#</tt>#%}% 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{%#<tt>#.v#</tt>#%}% buffer in Emacs.
25 25
26 There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% 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{%#<tt>#.emacs#</tt>#%}% file, like this: 26 There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the %\texttt{%#<tt>#coqtop#</tt>#%}% 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{%#<tt>#.emacs#</tt>#%}% file, like this:
27 %\begin{verbatim}%#<pre>#(custom-set-variables 27 %\begin{verbatim}%#<pre>#(custom-set-variables
28 ... 28 ...
29 '(coq-prog-args '("-I" "/path/to/cpdt/src")) 29 '(coq-prog-args '("-I" "/path/to/cpdt/src"))