Software Foundations in Coq

• Hints on Using Coq for OPLSS 2013
• Suggested Exercises

• the Coq compiler (coqc)
• the read-eval-print loop (coqtop)
• the standard libraries
• some form of integrated development environment (IDE); see more details below
• miscellaneous other tools
• the Reference Manual and Standard Library documentation.

Choosing an IDE

• Proof General (PG) is a generic IDE proof assistants that runs under Emacs. If you are already an emacs user (or want to become one), I strongly recommend this option, because it is reliable and easy to install.
• CoqIDE is a standalone tool designed specifically for use with Coq, and is part of the standard source release (and some binary releases). It is based on GTK and implemented in Ocaml. CoqIDE is a reasonable option if you don't know (or you dislike) emacs, but it is less reliable and can be hard to build and install.

Coq Installation

• linux. Use a package manager if you can: e.g., there are 8.4pl2 versions of Coq (with and without CoqIDE) on Debian/testing, and an 8.4pl1 (apparently without CoqIDE) on gentoo. Otherwise, you'll need to compile from source from the Download page. Once you have the necessary prerequisites installed, this is usually straightforward except for CoqIDE, which often has build problems.
• MacOS. You should use coqide-8.4pl2.dmg from the Download page if you can, but the binaries it installs do not work for me under MacOS 10.7 (better results have been reported under MacOS 10.8). An earlier version that does work for me under 10.7 is here: coqide-8.4.dmg. Macports claims to have an 8.4pl2 package available including CoqIDE. If you don't need CoqIDE, the coq-8.4.dmg file from the Download page should work, or you can build from source (again, building CoqIDE from source is often problematic), or fetch from homebrew (which has 8.4pl2, but without CoqIDE).
• Windows. The coq-installer-8.4pl2-win-0.exe installer on the Download page reportedly works. If you are using CoqIDE, make sure you install 8.4pl2; earlier 8.4 versions have serious bugs that make CoqIDE almost usable. If you want to use PG instead of CoqIDE, you may need to add the Coq bin directory to your path.

IDE Configuration

• Execute one tactic step forward.
• Undo one tactic step backward.
• "Goto" the cursor position, executing forward or undoing backward as necessary.
• Interrupt the current command or tactic (important when the underlying coqtop becomes slow or unresponsive).

• PG: In my experience, 3-pane mode doesn't work too reliably; using just 2 panes is generally fine. Use the Coq pull-down menu to toggle the pane mode.
• PG: To handle the fairly large Coq files in Software Foundations, you'll need to increase the "undo limit" by putting adding something like '(coq-default-undo-limit 10000) to your .emacs file.
• CoqIDE: Be warned that the autosave feature (enabled by default) has often been unreliable in the past, and the IDE crashes fairly often. Use explicit saves, early and often!