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'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. Simply use the ordinary XEmacs menu: Options -> Save Options In GNU Emacs, you can do M-x customize-save-customized or use the Custom->Save menu in a customize buffer. ----------------------------------------------------------------- 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$