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.
- First install Eclipse (v3.4 or later, tested in 2013 on Juno 4.4.2 release). The Classic download is recommended.
- From within Eclipse, choose
New Project
-> Checkout Projects from CVS
- 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.
- Navigate to
eclipse/ed.inf.proofgeneral
- 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
- Choose existing repository location
- 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:
- Help -> Software Updates -> Find and Install
- Select Search for New Features, Next
- Choose
Europa Discovery Site
, and check the box Automatically select mirrors
for convenience in the next dialog
- Select Mylyn -> Mylyn Connector: Trac
- Accept license, download, install and then restart as recommended
Now to add the Proof General Trac repository. You should first
register.
- Server URL: http://proofgeneral.inf.ed.ac.uk/trac
- 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:
-
$ cd [the proofgeneral hosted root directory]
-
$ less trac-auth/.htpasswd
to establish the username you wish to endow with XML-RPC privileges
-
$ . env.sh
to source the trac environment
-
$ trac-install-root/bin/trac-admin trac-project-env
to start the trac-admin shell
Now from within the trac-admin shell:
-
> permission list
will show you current permissions
-
> 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)