Communicator

The Proof General Kit white paper [7] mentions some ideas for a communication layer protocol for PGIP named PGCOM, but it appears that little or nothing had been decided at the time of writing. Desirable features include:

• Microsoft Windows compatibility
• Network transparency
• Secure Authentication

In the absence of a standard solution Igloo makes use of the wxWindows TCP/IP networking class wxSocketClient in the communicator module.

The use of TCP for the communication channel ensures that the client and server processes may easily run on separate machines, once a few shortcomings in PGIP are overcome. For example, PGIP currently provides no mechanism for the interface to see which theories Isabelle has available. Most theories inherit (make use of) previously completed theories, so this set of available theories is information that highly useful to the user. Once this is addressed in future versions of PGIP then Igloo will be able to be extended to truly benefit from its client-server design. In the meantime, we assume that the user somehow already knows which theories are available to the server.

In order to satisfy point 3, SRP authenticationSRP: http://srp.stanford.edu/ is used. Specifically, the Tiny SRP libraryTiny SRP Library: http://members.tripod.com/professor_tom/archives/index.html is used.

The order of communication events as Igloo starts are as follows:

1. Communicator opens a TCP connection on the relevant port to the Isabelle server.
2. If the connection succeeds, the communicator initiates the authentication procedure.
3. If authentication is successful, the Isabelle server starts a new copy of Isabelle, and begins sending data from Isabelle to the network connection, and data from the network connection to Isabelle.
4. The communicator starts wading through Isabelle's initialisation output messages until it sees the first PGIP message.
5. Events triggering communication between the communicator and the Isabelle server occur:
   • When the communicator receives a PGIP message, it copies the message into a buffer, ignoring any extraneous data outside a pair of opening and closing <pgip> tags. The communicator then calls the mediator's receive_pgip method, passing a pointer to the buffer and the length of the message.
   • Triggered by events in the GUI, the mediator builds PGIP messages, and passes them to the communicator's send_msg method, and the communicator passes these over the network connection to the Isabelle server.
6. This continues until the mediator calls the communicator's disconnect method, which closes the network connection. (It is assumed that the mediator has previously sent a message to Isabelle instructing it to terminate normally.)