CoqIde configuration to input special characters - coq/coq GitHub Wiki
(Part of the Coq FAQ)
NOTE: CoqIDE now offers builtin support for non-ASCII characters, superseeding most of the contents of this page.
See https://coq.inria.fr/refman/practical-tools/coqide.html#using-unicode-symbols
CoqIde is a GTK-based GUI for Coq.
If in Gnome, run the gnome configuration editor (gconf-editor
) and set key gtk-key-theme
to Emacs
in the category desktop/gnome/interface
.
Otherwise, you need to find where the gtk-key-theme-name
option is located in your configuration, and set it to Emacs
. Usually, it is in the $(HOME)/.gtkrc-2.0
file.
Set the GDK_USE_XFT
variable to 1
. This is by default with Gtk >= 2.2
. If some of your fonts are not
available, set GDK_USE_XFT
to 0
.
Thanks to the notation features in Coq, you just need to insert these lines in your Coq buffer:
Notation "∀ x .. y , p" := (forall x, .. (forall y, p) ..)
(at level 200, x binder) : type_scope.
Notation "∃ x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
(at level 200, x binder) : type_scope.
Copy/Paste of these lines from this file will not work outside of CoqIde. You need to load a file containing these lines or to enter the ∀ using an input method (see below). To try it, just use Require Import utf8
inside CoqIde. To enable these notations automatically start CoqIde with coqide -l utf8
.
In the ide
subdirectory of the Coq library, you will find a sample utf8.v
with some pretty simple notations.
First solution, using the iBus input method:
- type
sudo apt-get install ibus-table-latex
- then you must log out and log back in
- open "system settings" panel, go to menu "text entry"
- click the "+" button to add a new input source
- select "Other (LaTeX) (IBus)"
- look at which shortcut is registered for switching languages; alternatively, you can switch language from the global menu bar by clicking on the some icon saying, e.g. "Us" or "Fr".
- When LaTex input is selected, typing a backslash will trigger a completion box. Type the first letters, then type space to validate.
- For a simple backslash, just type backslash then space.
Alternatives:
- you may use another input method editor such as SCIM.
- you could type
<CONTROL><SHIFT>2200
to enter a forall in the script window. 2200 is the hexadecimal code for forall in unicode charts and is encoded as in UTF-8. 2203 is for exists. See http://www.unicode.org for more codes. - you could rebind
<AltGr>a
to forall and<AltGr>e
to exists. Under X11, one can add those lines in the file/.xmodmaprc
:
! forall
keycode 24 = a A a A U2200 NoSymbol U2200 NoSymbol
! exists
keycode 26 = e E e E U2203 NoSymbol U2203 NoSymbol
and then run xmodmap /.xmodmaprc
.
You can register a key to switch the keyboard to greek letters for the next keystroke. For example, to register the key "F12", execute in a terminal:
xmodmap -e 'keycode 96 = dead_greek dead_greek dead_greek dead_greek'
If you like to use another key, you can find its code by typing the command xmodmap -pke
.
Two solutions are offered:
-
Edit $XDG_CONFIG_HOME/coq/coqide.keys
(which is usually$HOME/.config/coq/coqide.keys
) by hand; or - if your system supports it, from CoqIde you may select a menu entry and press the desired shortcut.
The encoding option is related to the way files are saved. Keep it as UTF-8 until it becomes important for you to exchange files with non UTF-8 aware applications. If you choose something else than UTF-8, then missing characters will be encoded by \x{....}
or \x{........}
where each dot is a hex digit. The number between braces is the hexadecimal UNICODE index for the missing character.
Some users may experience problems with unwanted automatic templates while using Coqide. This is due to a change in the modifier keys available through GTK. The easiest way to get rid of the problem is to manually edit your coqiderc
file (either /home/<user>/.config/coq/coqiderc
in Linux, or C:\Documents and Settings\<user>\.config\coq\coqiderc
in Windows) and replace any occurrences of MOD4
with MOD1
.