Coq Installation notes

You can use OIT cluster computers, but it's best to install Coq on your computer.

Installation is straightforward, from this web site. Make sure you're getting Coq 8.4pl5 (though some other version of 8.4 might do). You'll then run the "coqide" program.

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>.

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.