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 arrowbdown button to process the whole file, or arrowbright to do this step-by-step. Check undo with arrowbup and arrowbleft.

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

Topic revision: r1 - 23 Aug 2006 - 18:44:37 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies