Testing Proof General on Emacs

Unfortunately there isn't a fully developed automated test mechanism yet.

A basic set of tests is to try the following:

1. Check that byte-compilation works:

           make clean
           make EMACS=myemacs
          

   This should build .elc files using myemacs.
   A bunch of warnings will be given but there should be no errors.
   After this step you'll be testing the compiled version.
2. Check that loading PG and visiting a file for your prover version works:
   
   1. Start up bare PG: emacs -q -l generic/proof-site.el
   2. Visit a file: C-x C-f isar/Example.thy
      The spash screen should appear, PG should load without any errors.
      The file should be visited and may be fontified automatically.
3. Check that starting your prover and processing the file works
   1. Make sure that your prover is configured to start with the default binary name (coqtop, isabelle, etc)
   2. Hit the button to process the whole file, or to do this step-by-step. Check undo with and .

In case of Emacs lisp errors in steps 2 or 3, please see PGEmacsDebuggingTips.