Sources for Proof General Eclipse

If you'd like to help us develop and extend Proof General Eclipse, you'll want to get the sources. Unsurprisingly, you'll need to work inside Eclipse, using the PDE (plugin development environment), which comes as part of the Eclipse for RCP/Plugin-Developers package of Eclipse, available from http://www.eclipse.org/downloads/.

Because the sources are under development by several people, if you are interested in working on the source please ContactUs before making any significant extensions or enhancements so we don't have difficulties merging changes. Smaller patches and fixes to the HEAD branch would be welcome.

Our sources are kept in the ProofGeneralCVSRepository and we don't plan on making separate source releases. If you hope to make significant contributions and would like CVS write access, please ContactUs to ask.

Checking out the plugin projects

If you wish to experiment with the code, you will need to download the plugin sources as an Eclipse project.

1. First install Eclipse (v3.4 or later, tested in 2013 on Juno 4.4.2 release). The Classic download is recommended.
2. From within Eclipse, choose New Project -> Checkout Projects from CVS
3. Create a new repository location with the following properties:
   

           Host: cvs.inf.ed.ac.uk 
           Path: /disk/cvs/proofgen 
           User: anon 
           Password: anon 
           Server Type: pserver

   If you have an account on our CVS server you can use that instead.
4. Navigate to eclipse/ed.inf.proofgeneral
5. Check out ed.inf.proofgeneral as a project in your workspace

This downloads PG Eclipse as a working project, rather than an installed plugin. Your normal Eclipse session will not have Proof General available. Instead, you access Proof General by running the project as an Eclipse Application -- which starts up a second "runtime" copy of Eclipse, with the Proof General project installed as a plugin. This allows you to edit the Proof General code and run your own modified code.

As well as the main plugin, you will need to download some prover plugins. Again, choose New Project -> Projects from CVS

1. Choose existing repository location
2. Choose using an existing module and browse to eclipse/ed.inf.proofgeneral.prover.isabelle, selecting this

The other prover plugins are in the same location, beginning with ed.inf.proofgeneral.prover. You can also select these at the same time as checking out the main plugin.

Please note that the plugin mechanism for prover configuration is meant just as a way of organising the code and per-prover configuration easily; it is not intended that extensive per-prover code be added to these plugins as it goes against the spirit of PGIP! Also, you should not rely on the prover configuration mechanism staying the same as we plan to move it to use the same component configuration mechanism in PGIP currently used by the broker.

Hints on compiling, running

Generally Eclipse compiles everything automatically and if you are lucky the class path settings will all work out. To test the program, you need to open a product file (e.g. pg-isabelle.product in the main plugin), and choose "Launch an Eclipse Application" or "Launch and Eclipse Application in Debug Mode" from the Overview tab.

• Some further hints are in the project in the README.txt file.
• See PGEclipseBuildRunRelease for more on building and our release mechanisms
  • To try these out, you need the projects ed.inf.proofgeneral.update-site and ed.inf.proofgeneral.feature
• For Proof General specifics, see PGEclipseDevelopment and the development documents in devel-doc

Connecting to Proof General Trac in Mylyn

To use the task management tool Mylyn with the Proof General Trac task tracking system, you must first add the Trac connector to Mylyn:

1. Help -> Software Updates -> Find and Install
2. Select Search for New Features, Next
3. Choose Europa Discovery Site, and check the box Automatically select mirrors for convenience in the next dialog
4. Select Mylyn -> Mylyn Connector: Trac
5. Accept license, download, install and then restart as recommended

Now to add the Proof General Trac repository. You should first register.

1. Server URL: http://proofgeneral.inf.ed.ac.uk/trac
2. Enter credentials

This should connect you (via XML-RPC) to the trac repository.

Note that any user who wishes to use XML-RPC communication with Trac requires the appropriate permission, to be added with the trac-admin tool (More information on this can be found at pgtrac:TracPermissions).

On the proofgeneral server, execute the following:

1. $ cd [the proofgeneral hosted root directory]
2. $ less trac-auth/.htpasswd to establish the username you wish to endow with XML-RPC privileges
3. $ . env.sh to source the trac environment
4. $ trac-install-root/bin/trac-admin trac-project-env to start the trac-admin shell

Now from within the trac-admin shell:

1. > permission list will show you current permissions
2. > permission add XML_RPC to grant this permission to the chosen user. This should immediately grant ticket access through Mylyn.

(note for PG maintainers: the configuration of trac/XML-RPC for Mylyn is delicate, see http://trac-hacks.org/ticket/1075 for patches)