RocqIDE FAQ
TODO: Put the relevant info
in the doc
and delete this file.
Q0) What is RocqIDE?
R0: A powerful graphical interface for Coq. See
https://rocq-prover.org/refman/practical-tools/coqide.html. for more information.
Q1) How to enable Emacs keybindings?
R1: Insert
gtk-key-theme-name =
"Emacs"
in your gtkrc file. The location
of this file is system-dependent.
If you
're running
Gnome, you may use the graphical configuration tools.
Q2) How to enable antialiased fonts?
R2) 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.
Q4) How to use those
Forall and Exists pretty symbols?
R4) Thanks to the Notation features
in Coq, you just need to insert these
lines
in your Coq Buffer :
======================================================================
Notation
"∀ x : t, P" := (
forall x:t, P) (at level 200, x ident).
Notation
"∃ x : t, P" := (
exists x:t, P) (at level 200, x ident).
======================================================================
Copy/Paste
of these lines
from this file will
not work outside
of RocqIDE.
You need to load a file
containing these lines
or to enter the
"∀"
using an input method (see Q5). To try it just use
"Require utf8" from inside
RocqIDE.
To enable these notations automatically start rocqide
with
rocqide -l utf8
In the ide subdir
of Coq
library, you will find a sample utf8.v
with some
pretty simple notations.
Q5) How to define an input method for non ASCII symbols?
R5)-First solution :
type "2200" to enter a
forall in the script widow.
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.
-Second solution : Use an input method editor, such as SCIM
or iBus. The latter offers
a module for LaTeX-like inputting.
Q6) How to customize the shortcuts for menus?
R6) Two solutions are offered:
- Edit $XDG_CONFIG_HOME/coq/coqide.keys
by hand
or
-
If your system allows it,
from RocqIDE, you may select a menu entry
and press the
desired shortcut.
Q7) What encoding should I use? What is this \x{iiii}
in my file?
R7) 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 an hex. digit.
The number between braces is the hexadecimal UNICODE index for the
missing character.
