COS 510: Programming Languages

Coq Installation notes

Install Coq version 8.7.1 on your computer. You'll then run the "coqide" program. (You may use Proof General or another IDE for Coq if you like, in which case the following instructions don't apply.)

After you install

Run CoqIde, the Coq Interactive Development Environment. Visit the file Basics.v. At upper left in the toolbar, click the green down-arrow a few times. Each time you do, more of the file should turn green.

Navigation shortcut: When doing proofs in CoqIDE, you can use the mouse to click on the green proof-navigation arrows in the toolbar. But it's often more convenient to use keyboard shortcuts. CoqIDE comes with a silly default for the keyboard shortcuts: control-alt-downarrow, control-alt-uparrow, etc. I find that simply control-downarrow or control-uparrow is much easier. You can change this by going to the Edit/Preferences menu, click on the Shortcuts tab, and in the box marked "Modifiers for Navigation Menu", unselect all but <ctrl>.

You may have to do this in two rounds: First, set <ctrl> as an "Allowed modifier", then restart CoqIde, then set the "Modifiers for Navigation Menu", then restart CoqIde again.

In the Font tab of the Preferences, I suggest you use Lucida Sans Unicode. Some Coq scripts (though probably not the ones for this course) use Unicode characters for mathematical symbols.

CoqIDE should then remember your preferences for next time.