VSCoq Legacy Extension in VSCode

Intro of the 4 most useful commands

If you open the command palette in VSCode (https://code.visualstudio.com/docs/getstarted/userinterface#_command-palette) and search for commands begin with "Coq: ", there are 4 commands, Open proof view, Interpret to Point, Step Forward, and Step Backward, which are very helpful when you "debug" your proof.

• Open proof view: this command will open a tab on the side showing the details of the current proof step
• Interpret to Point: Interpret/run the code from the beginning to the location where the cursor is
• Step Forward/Step Backward: Move 1 step further (or roll back 1 step)

On the right-hand side of the command palette, the hotkey of the corresponding command will be shown. It's highly recommended that you remember these hotkeys, so that you don't have to open the command palette every time when you step forward/backward in your proof.

The default hotkey setting on a Mac is:

• Open proof view: no hotkey, but that's fine; you only need to open it once
• Interpret to Point: ⌃ ⌥ → (Control-Option-RightArrow)
• Step Forward: ⌃ ⌥ ↓ (Control-Option-RightDown)
• Step Backward: ⌃ ⌥ ↑ (Control-Option-RightUp)

Open Proof View

After you run the command Open proof view, a new tab named "ProofView" will be opened on the side:

Interpret to Point

Interpret to a point that has no proof to show

After you run the command Interpret to Point, Coq will interpret the code from the beginning to where the cursor is.

For example, in the screenshot below, the cursor was at the end of line 95. So Coq interpreted the code from line 1 to line 95 and paused there. All the code before the cursor is shaded now.

Note that, in the proof view, it says, "Not in proof mode". That's because it interpreted to the end of the definition of next_weekday, which is not a proof, so there is nothing to show in the proof view.

Interpret to a point inside of a proof

But, if we interpret the code to a place inside of a proof, as shown in the screenshot below, the proof view will start to show the current state of the proof.

Step Forward

The Step Forward command will interpret the next proof statement, and update the state in the proof view accordingly.

Screenshot after 1 Step Forward:

Step Forward again:

Note that when the proof is completed, the proof view will show "Proof finished"

Step Backward

The Step Backward command will roll back the last interpreted proof statement, and update the state in the proof view accordingly.