Connecting PLATO and Proof General

I had some discussions in Edinburgh in August 2006 about the possibility of connecting Proof General with the PLATO component of the new version of the OMEGA system.

PLATO was developed by Marc Wagner and Serge Autexier.

Purpose

From PG's point of view, this connection might give Proof General an appealing document-centred interface using TeXmacs. There might also be the chance to interpret the richer architecture based on OMDoc (or some version of it?) in our setting.

From PLATO/Omega's point of view, there may be the chance to connect to Isabelle and similar theorem provers.

Discussion

At the moment the architecture of the two systems overlaps somewhat. The ProofGeneralBroker is intended to manage interactive proofs-in-progress in a similar way to the PLATO system itself, although it does not yet implement development graphs.

One difference is that Proof General is designed as a framework for interpreting different many proof languages in a uniform way, and providing facilities for manipulating native proof scripts based on this. By contrast, I think that the Omega architecture would instead fix its notion of proof language and then map that down to (possibly) different provers.

-- DavidAspinall - 05 Sep 2006

First steps

• Maybe start by looking at a log of PGIP interaction between Broker and Display?
• Perhaps some use-cases for particular interactions

Second steps

We resumed some discussions at MKM 2007 with ChristophLueth as well. Some notes about the latest things in Plato and compared with PGIP:

• The PGIP display protocol seems quite close to the interaction managed by Plato, where edits in the document are sent/received as XML updates and other events (e.g. menu invocation) cause action commands to be transmitted.
• Menus are also treated as documents which can be configured by the system (i.e. not hardwired in the interface) and attached to points in the document by reference. Menus cause action commands to be sent to the prover layers, which take appropriate action (typically triggering document updates).
• Actions have a flag in the prover to say whether they should be enacted immediately in the interface (it waits for a result), or whether they may be long running
• There is no locking of the document: if an edit command overlaps with a long-running strategy the theorem prover should cancel the strategy and allow the edit.