Notes on ideas for refactoring PG Eclipse

Here are some notes on ways we might improve the current structure of PG Eclipse. There are two main aims:

1. Really allow support for multiple provers, in a clean & good way
2. Merge the main HEAD branch with Ahsan's broker branch, somehow

Provers as plugins

The Eclipse way of doing things would be to have support for particular provers added using an extension point supplied by the main ed.inf.proofgeneral plugin.

This could be a good approach to follow: it seems possible/likely that even with the broker architecture we may want to supply prover-specific additional support or tweaking in the front end. Also, for people to write prover-specific support or tweaks, it would make things easy if they are isolated in separate and smaller packages.

-- DavidAspinall - 04 Oct 2006

I like that-- it would be good if there would be structured way that specific provers could make use of a graphical user interface (like Eclipse) without everything going through the broker. The operations setup is nice, but not flexible enough to allow arbitrary graphical interaction, and neither do we want to offer that as it would bloat the display protocol unnecessarily. Such graphic interactions would need to be guaranteed to be stateless, I guess (in the sense that they do not change the current proof or prover state).

-- ChristophLueth - 04 Oct 2006

Oh dear, now I've implemented it (well, not quite), it turns out you don't like it! The objection is that this mechanism forces a display-specific and static way of configuring the broker --- which might normally done by editing componentconfig.xml files, or inter-broker negotiation protocols. Which work once for all displays. Also, now we may need specific plugins for each prover when the generic mechanism shouldn't require this. Quite so, that was the plan. So time for a rethink...

-- DavidAspinall - 11 Oct 2006

Thinking some more...

But still it's nice to have some more Eclipse-specific behaviours possible that may or may not be tied to particular provers. The only model so far is to extend PGIP and the broker (perhaps the prover) to allow these. But it would be good to just do this in the display.

Examples: the hiproof interface, a development graph browser.

How could we supply these as extensions to the Proof General system? One idea is to provide extension points based on other parts of the system, e.g. centred around the Document Object Model for the proof script. Then plugins could add new listeners (visualise the proof script) and contribute model update actions (manipulate the proof script).

Combine broker-generic version with direct-connect version

This would be the ideal merge of the current two branches. The idea is that a Broker-supplied connection would be used if available, and it would offer a richer proof construction experience with more high-level operations (dependency management, proof construction, richer history management, etc).

The fallback position, for a simplified installation and user experience, would be to use a direct connection which uses the primitive queue management already implemented (although maybe it needs fixes...).

The first thought (and how I once planned to do this in Emacs) would be to implement the Broker as a special kind of prover, so using the standard generic mechanisms. However, Ahsan's experience perhaps shows that the broker connection mechanism is too different for this, so it may need to be made part of the fundamental architecture. How to achieve this needs further thought.

-- DavidAspinall - 04 Oct 2006

Integrating the Broker and display

I had more thoughts about refactoring PG Eclipse. I suppose there are two ways we can go about this:

• we can either keep the external broker as possibility, but build in a

simple broker functionality (refactored from the main branch, offering connectivity to one prover and linear script management) into the plug-in as fallback;

• or we can port the broker to Java, so that we can ship the broker as

part of the Eclipse plug-in, but also use it separately.

The second approach would of course tie us much closer to Eclipse and Java. This may or may not be a good thing, but it is a strategic decision. It makes the Eclipse display primus inter pares, so to speak. The first approach makes e.g. maintaining (and running!) the Emacs display easier (I think).

In both cases, the interface between Eclipse and broker is the display protocol, modelled as an abstract class, but in the first case as seen from the interface (display commands as methods, display messages as events to be reacted upon), and in the second as seen from the broker (display messages as methods, display commands as events). In the first case, the class has two instances, one is the built-in broker and the other one a wrap of the external broker. In the second case, the class has two instances, one the Eclipse plug-in as a display, the second a wrapper for an external (i.e. non-Java) display. (Tempting: a third could be a direct connection to some web service, that'd be easier in Java too.)

-- ChristophLueth - 06 Oct 2006

Hmm... I hadn't yet thought about refactoring to consider the existing proof management code as if it were a broker in the Kit architecture, but this is appealing.

The first route sounds more tractable: we probably don't have the resource at the moment to go for a complete Broker reimplementation and I still like the possibility of implementing clever proof manipulations in a more powerful language.

But: maybe we can we allow for both? If we start by implementing a simple standalone broker in Java we (or others) could use it elsewhere as an alternative to the Haskell Brainiac Broker. This might be helpful considering the number of Proof General look-alikes that people are building and getting not-quite-right. It's possible to restrict the Java code in an Eclipse plugin to just use JFC which means only a 6Mb Java library requirement: so the Broker could go mobile and should be easy to run outside Eclipse.

Later on, the simple Java broker could be improved gradually, or we could implement a more sophisticated one. The wrapper-broker which uses Haskell is also there.

A standalone broker like this then realises its connection to other components either

1. through an API and event-firing mechanism in Java, or
2. by sending/receiving PGIP messages

Of course we don't want Eclipse to talk to itself by constructing and deconstructing PGIP messages! Another benefit here would be to design a good API view on the broker-display and broker-prover connections. The present code makes some attempt at turning bits of PGIP into an API, and we've done something like it too in Haskell. Alex Heneveld also constructed a mechanism for controlling the prover away from the Eclipse GUI.

I think we need to work on a spec for these plans quite carefully and figure out how to answer some of the thorny questions like PGFileHandling.

-- DavidAspinall - 06 Oct 2006

Maybe we should get away from the idea of "one canonical broker implementation" which is still behind the refactoring ideas as mentioned above, and take the idea of "PGIP as middleware" more serious. Thus, it might be a more useful view to have one broker implementation inside Eclipse, which can either run on its own, or connect to an external broker via the (undocumented as yet) proxy protocol. Then, the Eclipse broker would only do e.g. linear depdendency handling, but it would have all the machinery needed to connect to other components (e.g. provers, or the main broker). When connecting to the main broker, it runs as a proxy (which means it just passes on all messages).

One point about all this is that the proxy protocol is not only cute to have, it becames necessary when you run a prover on another machine (simple ssh is not enough as that does not route interrupts)-- the Prosper people have done the same with their IIL (or whatever it was called) middleware.

Note that as far as the necessary implementation work is concerned, I think this is not more then with the refactoring above. The proxy protocol is nearly trivial to do, and the other work needs to be done either way.

-- ChristophLueth - 14 Oct 2006