path: root/FAQ

FAQs for using Proof General 
============================

With thanks to the anonymous authors of questions/answers below.

For latest version, see http://proofgeneral.inf.ed.ac.uk/FAQ
Please also check the BUGS file.

-----------------------------------------------------------------

Q. Emacs appears to hang when the prover process is started.

A. This is caused by UTF-8 support in recent linuxes with glibc 2.2 or later
   (e.g in Red Hat 8.0, 9, Fedora Core 1,2,3, Suse 9.1, ...)

   Glibc 2.2 and later may be enabled with UTF8 encoded output in your
   default locale.  Unfortunately Proof General relies on 8-bit
   characters which are UTF8 prefixes in the output of proof
   assistants (inc Coq, Isabelle).  These prefix characters are not
   flushed to stdout individually.  As a workaround we must find a way
   to disable interpretation of UTF8 in the C libraries that Coq and
   friends use.

   Doing this inside PG/Emacs seems tricky; locale settings are
   set/inherited in strange ways.  One solution is to run the Emacs
   process itself with an altered locale setting, for example,
   starting XEmacs by typing:

   $  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 is fixed in the startup shell script in recent development
   versions of Proof General: the supplied "proofgeneral" script makes an
   adjustment if it sees the string UTF in the current value of
   LC_CTYPE and an adjustment is made inside the Emacs environment.

   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.


   UPDATE for PG Version 3.6pre and 3.7:

   Some provers now have a Unicode-safe interaction mode.  You can set
   `proof-shell-unicode' to try to enable communication with the 
   prover which does not use non-ASCII 8-bit characters for markup.
   This is supported in Isabelle > Isabelle 2005.  Then the locale
   setting will not matter.

   In Coq, set coq-utf-safe by 

   (setq coq-utf-safe t)

   in your .emacs or init.el file.  (This mechanism may be integrated
   with `proof-shell-unicode' soon.)
  

-----------------------------------------------------------------

Q. Proof General fails to load with an error message on start-up: 

     error: "File `.../ProofGeneral/generic/proof-autoloads.elc' was 
     not compiled in Emacs"

   What's wrong?

A. We distribute .elcs for GNU Emacs, so you will have to delete
   them and (optionally) recompile for XEmacs.  Using the Makefile:

     Use 'make clean' to remove all .elc files.  
     Use 'make compile' to recompile .elc files.
 
   Check that the Makefile sets EMACS to your Emacs executable
   (or simply run 'make compile EMACS=emacs')
   

-----------------------------------------------------------------

Q. Proof General fails to load with an error message like this: 

     file mode specification error: (file-error "cannot open load file" "executable")

   What's wrong?

A. You're missing some Emacs (probably XEmacs) packages.  See
   the section "Dependency on Other Emacs Packages" in INSTALL.

-----------------------------------------------------------------

Q. Proof General shows a warning like this when started:

      (1) (file-mode-spec/warning) Error in File mode specification: Invalid argument: Invalid tag set, (mule-fonts)

  Backtrace follows:

    canonicalize-tag-set((mule-fonts))

   Also/alternatively, I notice junk in the output display with funny
   accented characters.  What's wrong?

A. You're probably using a 21.5.x beta version of XEmacs which is
   incompatible with X-Symbol (both the version distributed with
   XEmacs and the version distributed with Proof General).  
   Please update to a 2007 development release of Proof General
   which has added some compatibility patches for XEmacs 21.5.

-----------------------------------------------------------------




Q. Where have my buffers gone?   They used to be on the Buffers menu!

A. The PG "associated buffers" which display the proof state and
prover responses (and trace information when used) are now hidden from
the XEmacs tabs and buffer menus, to reduce clutter.

The idea is that you should only rarely need to select the buffer to
display explicitly.  Sometimes Emacs does its own thing, though!  To
find the buffers you can use the convenient keystrokes `C-c C-o'
(proof-display-some-buffers) or `C-c C-l' (proof-layout-windows).
See the manual for more details about the display mechanisms.

The buffers are hidden from menus by the standard Emacs mechanism of
beginning their names with a space.  So if you are looking for
"*prover-goals*" by keyboard `C-x b' the buffer is now called 
" *prover-goals*".  


-----------------------------------------------------------------

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. XEmacs appears to hang on certain malformed inputs to the prover.

A. This symptom may be caused by using non-Mule versions of XEmacs.
   Please make sure you use a Mule-enabled version.

-----------------------------------------------------------------

Q. XEmacs 21.4 displays a progress bar during fontification which
   sometimes gets stuck or messes up the display.  
   Is this a Proof General bug?  What can I do?

A. This is an XEmacs bug.  Things are better in morea recent patches 
   of 21.4, make sure you have the latest version.  You can prevent
   the use of the ugly widget, for example by adding 

     (setq progress-feedback-use-echo-area t)

   inside your configuration file `.xemacs/init.el'.

-----------------------------------------------------------------

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
   da+pg-support@inf.ed.ac.uk 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 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, 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. 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 x-symbol-decode-recode

   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. There are X-Symbol fonts at sizes of 12, 14, 18 and 24.  The standard size
   is 14, and 12 is used for subscripts.  The font size can be changed by
   adding

  (setq x-symbol-font-sizes '(("" 24 18)))

   to your .emacs, which causes the special fonts to come up in size
   24 and 18 for subscripts; the normal font can be changed manually.  By
   choosing other sizes, it is also possible to scale the existing fonts.
   Note that the larger fonts are not perfect.

   If you use Isabelle (both isa or isar) you can specify the X-Symbol font
   size through the -f option of the start-up-script.  The size is passed to
   emacs through the environment variable XSYMBOL_FONTSIZE, which can be used
   to configure the normal font in your .emacs.

-----------------------------------------------------------------

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. 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'.

-----------------------------------------------------------------


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
   Visit http://proofgeneral.inf.ed.ac.uk/mailinglist for more details.



$Id$