# HG changeset patch # User Adam Chlipala # Date 1352658977 18000 # Node ID 6769ef9688f217002ee24e117dd21a9d70aa2ce1 # Parent 417450cccedabca19e5a56f75cf1f509dca10917 Updated description of CoqIDE limitations diff -r 417450ccceda -r 6769ef9688f2 src/Intro.v --- a/src/Intro.v Thu Oct 25 08:40:42 2012 -0400 +++ b/src/Intro.v Sun Nov 11 13:36:17 2012 -0500 @@ -159,7 +159,7 @@ A traditional printed version of the book is slated to appear from MIT Press in the future. The online versions will remain available at no cost even after the printed book is released, and I intend to keep the source code up-to-date with bug fixes and compatibility changes to track new Coq releases. -%\index{graphical interfaces to Coq}%I believe that a good graphical interface to Coq is crucial for using it productively. I use the %\index{Proof General}%{{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 %\index{CoqIDE}%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. 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] or ##%\coqdockw{%Restart%}%## commands, which CoqIDE does not support. It would be bad form to leave such 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. +%\index{graphical interfaces to Coq}%I believe that a good graphical interface to Coq is crucial for using it productively. I use the %\index{Proof General}%{{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 %\index{CoqIDE}%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. 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 before version 8.4, regarding running through the book source, is that I will sometimes begin a proof attempt but cancel it with the Coq [Abort] or ##%\coqdockw{%Restart%}%## commands, which CoqIDE did not support until recently. It would be bad form to leave such 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. *) (** ** Reading This Book *)