From 04e8a323da07c67031f4c0e23a020ba245938a0c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 26 Jul 2016 00:05:52 +0200 Subject: Rename FAQ -> FAQ.md --- FAQ.md | 316 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 316 insertions(+) create mode 100644 FAQ.md (limited to 'FAQ.md') diff --git a/FAQ.md b/FAQ.md new file mode 100644 index 00000000..0bc70b05 --- /dev/null +++ b/FAQ.md @@ -0,0 +1,316 @@ +FAQs for using/installing Proof General +======================================= + +With thanks to the anonymous authors of questions/answers below. + +For latest version, see https://github.com/ProofGeneral/PG/blob/master/FAQ +Please also check the BUGS file. + +----------------------------------------------------------------- + +Q. I use ProofGeneral with custom installations of Coq, depending + on the project I am working on. How can I change coq-prog-name + accordingly? + +A. The recommended way to set coq-prog-name is to create a file + .dir-locals.el in the top-level folder of your Coq project (or + if applicable, in the sub-folder containing the Coq source files) + with content: + + ((coq-mode . ((coq-prog-name . ".../path/to/coqtop")))) + + Then restart Emacs + (or just run: M-x proof-shell-exit RET yes RET, M-x normal-mode RET + in the Coq buffer before restarting the Coq process) in order + to take this change into account. + +----------------------------------------------------------------- + +Q. The prover process produces some useful output I'd like to + keep a note of, how do I do that? + +A. Some people cut and paste into comments in their source files. + But you can easily make new files or temporary buffers in Emacs: + + * copy text from *response* or *goals* buffer + * C-x b RET + * Switch to correct mode, e.g.: M-x isar-response-mode RET + * Paste text, the highlighting/sumbols should appear correctly. + +----------------------------------------------------------------- + +Q. Proof General fails to load with an error message on start-up, + containing text like this: + + Proof General was compiled for GNU Emacs 23.1 but + is running on Emacs 22.3: please run "make clean; make" + + What's wrong? + +A. We distribute compiled .elcs for one version of Emacs, but other + versions use different bytecode formats. You will have to delete + the compiled files and (optionally) recompile for your preferred + Emacs version. Using the Makefile: + + make clean # removes all .elc files. + + and then a command like this: + + make EMACS=emacs-22.3 + + (without the EMACS setting just uses 'emacs'). + +----------------------------------------------------------------- + +Q. I have just installed Emacs, ProofGeneral and a proof assistant. + It works but Tokens (e.g. \) are not being displayed + as symbols. + +A. You need to enable Unicode Tokens by the menu item: + + Proof-General -> Options -> Unicode Tokens + + To enable it automatically every time you use Proof General, + use + + Proof-General -> Options -> Save Options + + after doing this. + + Note that we don't do this by default, because from the system's + perspective it is difficult to determine if this will succeed --- + or just produce funny characters that confuse new users even more. + + If you are using Isabelle, the wrapper script will load Tokens + from any location, and you can enable it by passing the option + "-x true". + +----------------------------------------------------------------- + + +Q. With Unicode symbols enabled, the symbols look a mess, e.g. + compressed and overlap one another. + +A. Unfortunately this is a bug in the display engine inside + certain versions of Emacs, for example the default version + of emacs, Emacs 23.3.1 on Ubuntu 11.10, suffers. + + The solution is to switch to another version (e.g. Emacs 23.2). + (See Trac#409: http://proofgeneral.inf.ed.ac.uk/trac/ticket/409) + + You may be able to get better results with different fonts, even + without upgrading Emacs. + + Proof General uses Deja Vu Sans Mono by default because + this often works out-of-the-box. But STIX is better if you + install it. See http://www.stixfonts.org/. On Ubuntu try: + + sudo apt-get install fonts-stix + + To change to STIX, either + + M-x customize face RET unicode-tokens-symbol-font-face RET + + and edit to set the family name to "STIXGeneral", or edit + the line beginning "(defface unicode-tokens-symbol-font-face" in + lib/unicode-tokens.el. + + +----------------------------------------------------------------- + +Q. Help, I'm stuck!! Emacs keeps telling me "Cannot switch buffers in a + dedicated window" + +A. This can happen if you enabled "Use Three Panes" and then change + the panes (window) layout manually, typically by deleting another + window or frame so you only have a "dedicated" window on the + display. Don't kill Emacs! There are many ways of getting out, + e.g. + -- In single window mode, C-c C-l (proof-layout-windows) refreshes + the display + + -- In multiple window mode, if you have accidently deleted the main + window, get a new one with M-x new-frame RET + + + +----------------------------------------------------------------- + +Q. I have a problem installing/using Proof General, what can I do? + +A. Please check the documentation carefully, particularly the + requirements for a full-featured and recent Emacs version, as + mentioned in INSTALL (see "Dependency on Other Emacs Packages"). + If you still cannot solve your problem, try to contact someone + else who is using Proof General with a similar setup. The + best way to do this may be through the user mailing list for your + proof assistant. If you think the problem is Proof General related, + consult the PG Wiki and Trac pages. + + + +----------------------------------------------------------------- + +Q. I'm using Proof General for prover X, then I load a file for + prover Y. I get an error. Why? + +A. Unfortunately the architecture of Proof General is designed so + that you can only use one prover at a time in the same Emacs + session. If you want to run more than one prover at a time, + you have to run more than one Emacs. + + + +----------------------------------------------------------------- + + +Q. I'm afraid I got stuck very early on. I sent the following line: + + by (swap_res_tac [psubsetI] 1; + + Notice that I forgot the right bracket. The line went pink, the + buffer went read-only and nothing I tried would let me fix the + error. + +A. The proof process is waiting for more input because of the missing + parenthesis, but Proof General doesn't realise this and waits for a + response. You should type something in the proof shell buffer + (*isabelle*), or interrupt the process with C-c C-c or the Stop button. + + +----------------------------------------------------------------- + +Q. How can I keep the Proof General option settings across sessions? + +A. For options set in the Proof General -> Options menu use the + "Save Options" menu item (Proof General -> Options -> Save Options). + + For other options set via customize (Proof General -> Advanced -> + Customize), use the customize buttons, or M-x customize-save-customized. + + +----------------------------------------------------------------- + +Q. The "Favourites" feature to insert/send fixed strings is great, + but I'd like to define a command which takes arguments. + +A. You can do that in Elisp with a command like this: + + (proof-definvisible isar-theorem + '(format "thm %s" (read-string "theorem: ")) + [(control t)]) + + (NB: it binds the key C-c C-a C-t). See the documentation for + `proof-definvisible' and `proof-defshortcut`. + + +----------------------------------------------------------------- + +Q. Why do I get a warning "Bad version of xml.el found, ..."? + +A. Your Emacs distribution includes a version of xml.el which has + fundamental bugs. The patched version of xml.el, in lib/xml-fixed.el + has been loaded instead. This works for Proof General because it fixes + the basic bugs, but it may cause compatibility issues in other packages + (e.g. it is quite different from the latest xml.el with GNU Emacs + development versions). + + This message is probably nothing to worry about unless you are using + the same Emacs session for other packages that heavily use xml.el + (e.g. GNUS). + + +----------------------------------------------------------------- + +Q. Undo behaviour in Coq seems to stop working with very long + sequences of commands. + +A. Coq has a limited history for Undo. Change + + Coq -> Settings -> Undo Depth + + to something higher. Default is 200 (100 outside PG). + + +----------------------------------------------------------------- + + +Q. Can I join any mailing lists for Proof General? + +A. Of course, email "proofgeneral-request@informatics.ed.ac.uk" + with the line "subscribe" in the message body, to join the + users' and announcements list. + + There is also a list for developers, proofgeneral-devel: + + http://proofgeneral.inf.ed.ac.uk/mailinglist + + for more details. + + +----------------------------------------------------------------- + +Q. Emacs appears to hang when the prover process is started. + +A. One thing is to check the variable 'comint-process-echoes' which + might be non-nil for the *coq* (or other prover) buffer. It + should be nil. + + The default value of comint-process-echoes is nil. Move any + modifications of this variable away from the top level (e.g., + .emacs file, which affects the *coq*-buffer), and down to the + mode-hooks which require them (e.g. shell-mode-hook). The + variable might also have been set by Customize, it can be reset + with M-x customize-variable RET comint-process-echoes RET. + + A reason with older versions of Isabelle and Coq (before 2007) was + the emergence of UTF-8 support in linuxes with Glibc 2.2 and + later, enabled with UTF8 encoded output in your default locale. + Proof General used on 8-bit characters which are UTF8 prefixes in + the output of proof assistants. These prefix characters were not + flushed to stdout individually. + + As a workaround we can disable interpretation of UTF8 in the C + libraries. Doing this inside Proof General is unreliable; locale + settings are set/inherited in strange ways. One solution is to + run the Emacs process itself with an altered locale setting, e.g., + + $ LC_CTYPE=en_GB xemacs & + + (where $ is the shell prompt; this example is for my locale which + by default is "en_GB.UTF-8": I see this by typing "locale" at + the prompt). + + (This fix is attempted in the supplied "proofgeneral" script, as + well as making an adjustment in Proof General when the string UTF + appears in the current value of LC_CTYPE. Alternatively you can + set LC_CTYPE inside a file ~/.i18n, which will be read the shell. + Put a line such as "LC_CTYPE=en_GB" into this file. However, this + action will affect all applications. + + NB: a related issue is warnings from X-Symbol: "Emacs language + environment and system locale specify different encoding, I'll + assume `iso-8859-1'". This warning appears to be mostly harmless. + Notice that the variable `buffer-file-coding-system' may determine + the format that files are saved in. + + Another way to affect this which has been suggested is to add a line + like this to the init.el file on XEmacs: + + (prefer-coding-system 'ctext) + + but I haven't tried this. + + The above fixes should not be necessary with most recent prover + versions. Isabelle 2007 has a "Unicode-safe" interaction mode, + enabled by default (to disable, customise `proof-shell-unicode'). + This is also used by the Isabelle startup scripts. Coq 8.1 and + later do not use non-ASCII characters in output. + + + + + + +$Id$ + -- cgit v1.2.3