Coq Installation notes
You can use the computers in the Friend 009 lab (and 007 and 005),
but it's best
to install Coq on your computer.
Windows
Installation is straightforward, just
grab this and run it. You'll then run the "coqide" program.
Linux
Coq's favorite place to run is Linux. Grab the sources here and compile them.
Macintosh
For some reason, the Coq team has not bothered to make a binary installation forMacintosh. Installing from sources is quite complicated.
Here's the recipe.
Therefore, Mac users may want to skip installation for a few days,
and use the lab machines while we see if we can get the Coq team
to build an installation package.
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 "Modes for Navigation Menu", delete what's there and just hit the Control key, so it says just <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.
more to come...