Computer Science 510
Programming Languages
Andrew Appel

Spring 2024

General Information Schedule Policies

Using VSCoq1, a VSCode extension for Coq

Installation and Keyboard Shortcuts

You can find info about VSCoq here, and you can install it from the VSCode marketplace. The most important keyboard shortcuts are the "step forward" and "step backward" commands. The defaults for each OS are given at the above link, but you can configure these yourself using File->Preferences->Keyboard Shortcuts. Scroll down until you see "Coq: Step Backward" and "Coq: Step Forward". As the Coq installation notes suggest, we recommend changing these to control+down and control+up, respectively.

Working with Multiple Files

Starting from Homework 1, each successive Coq file will involve definitions and theorems from previous ones. In order for VSCoq to correctly find these files, you will want to do the following:

Download and extract the entire Software Foundations tgz file from the installation page. This will create the directories lf, plf, vfa, and vc.
Make sure that each of these directories has a file called _CoqProject and a Makefile. Without these, VSCoq will not detect multiple files.
When working on a file in VSCode, use File->Open Folder to open the appropriate directory. For the first few assignments, this will be sf/lf. Do NOT use File->Open File to open the individual file (ie Induction.v) in VSCode; you will not be able to reference any previous files.
When VSCode imports a previous file, it uses the compiled .vo file created from the source .v files you are editing. If you need to update the .vo files, in the VSCode terminal (which should be set to the directory you are currently in: lf, plf, etc) you can run the command make <file>.vo or just make to compile everything. You should do this if you encounter an error like "Cannot find a physical path bound to logical path foo". You can also do this if any of the .vo files get deleted or altered for some reason.

You can also find more information about Coq compilation at the beginning of Induction.v.

Computer Science 510 Programming Languages Andrew Appel

Spring 2024

Using VSCoq1, a VSCode extension for Coq

Installation and Keyboard Shortcuts

Working with Multiple Files

Computer Science 510
Programming Languages
Andrew Appel