ALERT! FIXME: content ported from old wiki, needs validating

Prover Setup Documentation

These pages describe how to setup Proof General Eclipse for a new theorem prover.

Please also feel free to ContactUs if you are thinking of using Proof General Eclipse. We will we happy to help.

PGIP-Enabled Theorem Provers

Will your users write and edit PGIP scripts?

Should be simple. Currently not supported, but (hopefully) trivial to do so.

Using a PGIP prover with non-PGIP scripts

This is what we do with Isabelle.

Steps to set-up a new prover:

*1. Create a preference page. ** Edit plugin.xml to register the file suffix as one that should be handled by Proof General. ** Edit the file-association preference to identify your prover as the one to be used with such files. ** Create a preference pages describing how PG should interact with your prover (see below). ** Create a keywords file for syntax highlighting. ** Create a syntax description file (see Isabelle for an example).

Other Provers

Proof General can work with ''virtually any'' theorem prover that has either a command-line or socket interface. There are two options:

*1. Convert your prover to use PGIP.

The xml wrapping and un-wrapping should be fairly easy to implement, given that there are plenty of xml libraries available to help. We use [http://www.dom4j.org/ Dom4J ] inside Proof General Eclipse, and can recommend it for Java-based xml work. The main work will probably be in implementing a parser to handle requests.

** Modify Proof General to work without PGIP.

This should not be too hard, but you will need to edit some classes though. Minimally, you must implement a sub-class of the Parser class, filling in the abstract methods. You may also need to modify the SessionManager and ProverModel classes.

Note for Windows Users

Incredible as it may seem, Windows does not support 2-way command-line communication between processes. Hence Proof General cannot communicate with a command-line prover running on Windows.

To get around this you can: *1. If you work on a Windows box, but have network access to a Linux box, you can run the theorem prover remotely using TPWrapper (see PGEclipseUtilities ). ** Socket-based communication is fine. Configure/re-write your theorem prover so that it can communicate via sockets and all will be well.

Creating a preference page for your system

There are 3 steps: *1. Create a file MySystemPrefsPage.xml in the ed.inf.proofgeneral/config directory. This contains your preferences and their default values. See the existing files for the syntax. ** Create a class MySystemPrefsPage.java subclassing PrefsPageBackend. This can be done by copying PrefsPage.java and making minor changes. ** Edit plugin.xml (or a fragment.xml) to register the new preference page (see existing entries for the syntax).

Settings Files

These files are all found in the config subdirectory of the ed.inf.proofgeneral plugin.

IsabellePrefs.xml

IsabelleSyntax.xml

This file defines how Proof General parses files (and hence syntax highlighting). It consists of regular expression patterns for identifying regions.

proofGeneralPrefs.xml

colourPrefs.xml

Edit to create new colour categories.

Topic revision: r1 - 21 Aug 2006 - 14:26:32 - 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