next up previous contents
Next: GUI Up: System Design Previous: PGIP and PGML   Contents


Isabelle Server

The task of the Isabelle server is to provide easy access for a PGIP client to an instance of Isabelle, which may or may not be running on the same machine. This client/server segmentation also forces the coupling between Isabelle and the mediator modules to be as loose as possible. The only data travelling between the two is PGIP data. Since the mediator is a single point of control for all communication with Isabelle, it should incur minimal cost to attach this code to another proof assistants which support PGIP in the future.

The current implementation is a simple shell script that listens for connections on a particular TCP port, and forks an instance of Isabelle when a client connects. While this client remains connected, no further clients are able to connect. When the client finally disconnects, the shell script closes the socket and begins listening again. The network transport is provided by netcat, a unix utility which shovels data across network connections. The version of netcat used incorporates the Tiny SRP secure authentication library.


next up previous contents
Next: GUI Up: System Design Previous: PGIP and PGML   Contents
2003-11-08

Valid HTML 3.2! Valid CSS!