diff options
Diffstat (limited to 'FAQ')
| -rw-r--r-- | FAQ | 194 |
1 files changed, 194 insertions, 0 deletions
@@ -0,0 +1,194 @@ +FAQs for using Proof General +============================ + +For latest version, see http://www.proofgeneral.org/FAQ + +Credits to the anonymous authors of questions/answers below. + +----------------------------------------------------------------- + +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, send a message to + support@proofgeneral.org in the first instance. + +----------------------------------------------------------------- + +Q. I'm using Proof General for prover X, then I load a file for prover Y. + The buffer doesn't enter the mode for prover Y. Why not? + +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 have just installed Emacs, ProofGeneral and a proof assistant. + It works but X-Symbol is not being activated. + +A. Once X-Symbol is picked up by Emacs (e.g. is working for TeX), + you should enable it inside Proof General by the menu item: + + Proof-General -> Options -> X-Symbol + + To enable it automatically every time you use Proof General, + type + + M-x customize-variable RET isar-x-symbol-enable RET + + and change/set/save the setting to `on'. + + 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 X-Symbol + from any location, and you can enable it by passing the option + "-x true". + +----------------------------------------------------------------- + +Q. I notice that editing Isabelle files in Proof General with XEmacs + 21.4 is very slow. Can this be fixed? + +A. You could consider adding the following line to your init file: + + (setq lookup-syntax-properties nil) + + This hack bypasses some very slow code in the font-lock system, but + it also disables some syntax-related features, so use with care. + +----------------------------------------------------------------- + + +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, but Proof General + doesn't realise this and waits for a response. You + should type something in the proof shell, 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. I'm experiencing debilitating performance problems with font-lock + and X-Symbol under XEmacs 21.4. Can you help? + +A. There are some settings that can improve things: + + [ FIXME ] + +----------------------------------------------------------------- + +Q. How do I use Proof General for Isabelle classic instead of Isabelle/Isar? + +A. There are several ways: + + 1. Use the Isabelle settings mechanism, invoke with "Isabelle" + 2. Set the environment variable PROOFGENERAL_ASSISTANTS=isa + before starting Emacs. + 3. Put the line (* -*- isa -*- *) at the top of your files. + + Unfortunately Isabelle/Isar and Isabelle classic are two quite + separate Proof General instances. Ideally they should be + combined into one, if anyone fancies some elisp hacking... + + +----------------------------------------------------------------- + +Q. When using X-Symbol, why do I sometimes see funny characters like + \233 in the buffer? + +A. These are part of the 8 bit character codes used by X Symbol to + get symbols from particular fonts. Sometimes X-Symbol forgets to + fontify the buffer properly to make it use the right fonts. + (That's being rather unkind to X-Symbol: several things can + go wrong one way or another). + + To fix, type + + M-x font-lock-fontify-buffer + + or M-x x-symbol-fontify. If that doesn't work, type M-x + font-lock-mode twice to turn font-lock off then on. + Or reload the file. + + Note that X-Symbol is more robust when used with XEmacs/Mule. + + Read the X-Symbol documentation for (much) more information. + http://x-symbol.sourceforge.net/man/ + +----------------------------------------------------------------- + +Q. I would like to use the X-Symbol fonts in PG not just at the + standard size but also for larger sizes since I use PG during + talks, where I set the font size to 24. + +A. Nobody has designed large versions of the X-Symbol fonts but it is + possible to scale-up the existing ones, by adding + + (setq x-symbol-xsymb1-fonts + '(("-xsymb-xsymb1-medium-r-normal-*-*-240-*-*-*-*-xsymb-xsymb1") + ("-xsymb-xsymb1_sub-medium-r-normal-*-*-180-*-*-*-*-xsymb-xsymb1") + ("-xsymb-xsymb1_sup-medium-r-normal-*-*-180-*-*-*-*-xsymb-xsymb1"))) + + (setq x-symbol-xsymb0-fonts + '(("-adobe-symbol-medium-r-normal-*-*-240-*-*-*-*-adobe-fontspecific" + "-xsymb-xsymb0-medium-r-normal--*-240-75-75-p-85-adobe-fontspecific") + ("-xsymb-xsymb0_sub-medium-r-normal--18-180-75-75-p-74-adobe-fontspecific" + "-adobe-symbol_sub-medium-r-normal-*-*-180-*-*-*-*-adobe-fontspecific") + ("-xsymb-xsymb0_sup-medium-r-normal--18-180-75-75-p-74-adobe-fontspecific" + "-adobe-symbol_sup-medium-r-normal-*-*-180-*-*-*-*-adobe-fontspecific"))) + + to your .emacs, which causes the special fonts to come up in size + 24; the normal font you can change manually. Of course you can also + select smaller sizes. Most of the symbols look reasonable, except + that they appear almost bold. + + For more information about this, see the X-Symbol FAQ, at + http://x-symbol.sourceforge.net/man/x-symbol_8.html#SEC100 + +----------------------------------------------------------------- + +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 + user's and announcements list. + + There is also a list for developers, proofgeneral-devel + Visit http://www.proofgeneral.org/mailinglist for more details. + + +----------------------------------------------------------------- + + +Q. I see spurious ^M characters at the end of lines in the + windows showing output from the prover. How can I remove + them? + +A. Customize the value of `proof-shell-strip-crs-from-output'. + +----------------------------------------------------------------- + +$Id$ + |