aboutsummaryrefslogtreecommitdiff
path: root/ide/coqide/FAQ
diff options
context:
space:
mode:
authorMaxime Dénès2020-05-16 17:07:37 +0200
committerMaxime Dénès2020-06-02 18:53:33 +0200
commit33021618a06a94563d28691940f02a55bd9d358d (patch)
tree9d0cab0e9ffc2f1499ec1d49b142a758d7f80fee /ide/coqide/FAQ
parentdb768e6828af62e06eb03d36509be6f8fc1efbf3 (diff)
Move CoqIDE to its own folder
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
Diffstat (limited to 'ide/coqide/FAQ')
-rw-r--r--ide/coqide/FAQ54
1 files changed, 54 insertions, 0 deletions
diff --git a/ide/coqide/FAQ b/ide/coqide/FAQ
new file mode 100644
index 0000000000..c8b0a5d328
--- /dev/null
+++ b/ide/coqide/FAQ
@@ -0,0 +1,54 @@
+ CoqIde FAQ
+
+Q0) What is CoqIde?
+R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations.
+
+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 CoqIde.
+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
+CoqIde.
+To enable these notations automatically start coqide with
+ coqide -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 "<CONTROL><SHIFT>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 CoqIde, 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.
+