Mercurial > cpdt > repo
comparison src/Intro.v @ 535:dac7a2705b00
...and back to working in 8.4 again
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 05 Aug 2015 14:57:14 -0400 |
| parents | ed829eaa91b2 |
| children | 71b85aaae868 |
comparison
equal
deleted
inserted
replaced
| 534:ed829eaa91b2 | 535:dac7a2705b00 |
|---|---|
| 201 | 201 |
| 202 %\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the <<coqtop>> program, which provides the interactive Coq toplevel. One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}%<<.emacs>> file, like this: | 202 %\item %#<li>#There are some minor headaches associated with getting Proof General to pass the proper command line arguments to the <<coqtop>> program, which provides the interactive Coq toplevel. One way to add settings that will be shared by many source files is to add a custom variable setting to your %\index{.emacs file@\texttt{.emacs} file}%<<.emacs>> file, like this: |
| 203 << | 203 << |
| 204 (custom-set-variables | 204 (custom-set-variables |
| 205 ... | 205 ... |
| 206 '(coq-prog-args '("-I" "DIR/src")) | 206 '(coq-prog-args '("-R" "DIR/src" "Cpdt")) |
| 207 ... | 207 ... |
| 208 ) | 208 ) |
| 209 >> | 209 >> |
| 210 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 <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time. | 210 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 <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time. |
| 211 | 211 |
| 212 Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply. Here is an example that could be written in such a file to enable use of the book source. Note the need to include an argument that starts Coq in Emacs support mode. | 212 Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply. Here is an example that could be written in such a file to enable use of the book source. Note the need to include an argument that starts Coq in Emacs support mode. |
| 213 << | 213 << |
| 214 ((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src"))))) | 214 ((coq-mode . ((coq-prog-args . ("-emacs-U" "-R" "DIR/src" "Cpdt"))))) |
| 215 >> | 215 >> |
| 216 #</li># | 216 #</li># |
| 217 | 217 |
| 218 #</ol>#%\end{enumerate}% | 218 #</ol>#%\end{enumerate}% |
| 219 | 219 |
| 220 Every chapter of this book is generated from a commented Coq source file. You can load these files and run through them step-by-step in Proof General. Be sure to run the Coq binary <<coqtop>> with the command-line argument <<-I DIR/src>>. If you have installed Proof General properly, the Coq mode should start automatically when you visit a <<.v>> buffer in Emacs, and the above advice on <<.emacs>> settings should ensure that the proper arguments are passed to <<coqtop>> by Emacs. | 220 Every chapter of this book is generated from a commented Coq source file. You can load these files and run through them step-by-step in Proof General. Be sure to run the Coq binary <<coqtop>> with the command-line argument <<-R DIR/src Cpdt>>. If you have installed Proof General properly, the Coq mode should start automatically when you visit a <<.v>> buffer in Emacs, and the above advice on <<.emacs>> settings should ensure that the proper arguments are passed to <<coqtop>> by Emacs. |
| 221 | 221 |
| 222 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. | 222 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. |
| 223 %\index{Proof General|)}% *) | 223 %\index{Proof General|)}% *) |
| 224 | 224 |
| 225 (** %\section{Chapter Source Files} | 225 (** %\section{Chapter Source Files} |