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:
- Really allow support for multiple provers, in a clean & good way
- 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
- through an API and event-firing mechanism in Java, or
- 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