Configuration of CoqIDE

Pierre Letouzey edited this page Oct 17, 2017 · 1 revision
Clone this wiki locally

The default key bindings of CoqIDE are often problematic because they conflict with the window manager. Moreover, the default bindings are not efficient at all: the most useful action requires pressing a combination of 3 keys... Fortunately, it is straightforward to update the bindings.

Configuring the alternative set of bindings

(For Coq version >= 8.4 only)

Close all running instances of CoqIDE, then download and install the modified configuration file as follows:

  • On Linux, copy the file coqide.keys into the folder ~/.config/coq/
  • On Windows, copy the file coqide.keys either into the folder %HOME%\.config\coq if HOME is defined, or into the folder C:\Program Files\Coq\config (assuming you used the default installation path).
  • On MacOS, the alternative set of bindings has not been tested; see below how to modify the bindings yourself.

The alternative set of bindings

After you copied the modified configuration file, the new bindings are as follows:

Execute until cursor F5
Execute backward one step F6
Execute forward one step F7
Execute to the end F8
Run make F9
Reach next error F10
Interrupt execution F11
Reset execution F12

How to manually modify the bindings

You can edit the binding files coqide.keys yourself. (It is located in ~/.config/coq/ or C:\Program Files\Coq\config\). To modify a binding, edit the corresponding line by removing the semi-column at the beginning of the line and changing the shortcut. Example:

before ;(gtk_accel_path "/Navigation/_Go to/" "<CTRL><ALT>Right")
after (gtk_accel_path "/Navigation/_Go to/" "F5")

Other tips for Coqide

Copy-pasting: to copy a piece of text from proof context or from the error message pannel, you cannot use the CTRL+C key binding, however the key binding CTRL+INSERT does work.

Focus: CoqIDE can be slowed down a lot by the Focus command. Do not use it. Instead, use "admit" to skip subgoals until you can view the one that you are interested in.