GUI

The Igloo GUI is split into two primary windows. The main Igloo window (figure 4.4) is designed to allow the user to connect to an Isabelle server, and create new theories. These features rely on one area that PGIP currently ignores. Therefore, this functionality is left largely unimplemented for the moment, and another solution is offered in the meantime. This solution can be seen in §A figures A.4, A.5 and A.6.

Figure 4.4: Igloo's main window

• The Igloo menu provides two choices, Quit which exits Igloo, and Options which will be used to define options and preferences for the user. The Options window has not yet been designed, since the final options that will be available to the user cannot be determined until PGIP has been finalised.

• The Proof Engine menu provides two choices, that enable the user to Connect or Disconnect from a proof assistant.

• The Theory menu is the method used to start a new theory, until PGIP enables the library management features we desire. When this happens, the menu will be removed, and the create button will serve its purpose. A proposed amendment to PGIP that would allow this window to be implemented fully is given in §5.1.

• The Edit menu currently only provides one option, Undo which will allow the user to remove the previously added theory from the selected theories pane. Since this pane is not currently operational, neither is this menu option.

• The Help menu is provided to allow the user to access help with Igloo or the proof assistant. In the client/server model we have chosen for Igloo, since the proof assistant may not be running on the local machine, there is also the possibility that the help for that proof assistant might not be available locally either. It is suggested that a PGIP command could request a URL where the help can be accessed. This URL could point to the standard documentation for the proof assistant, or a local network cached copy.

The rest of this window requires the amendments to PGIP suggested in §5.1:

• The Use button will add the currently selected theory in the theory directory pane to the list of theories to inherit in the selected theories pane.

• The Create button will create a new theory using the theories in the selected theories pane, and open a Proof Window for this theory.

• The Display button will open up a theory file viewer for the theory that it selected in the theory directory pane.

• The Edit button will open up a theory file editor for the theory that it selected in the theory directory pane. This will be a simple file editor, which will allow the user to remove theorems, and inherited theories, and then force the proof assistant to reload and recheck the theory.

• The Find button and text entry field next to it will allow the user to search for theories that contain a particular text string. A temporary listing of matching theories will be shown in the theory directory pane.

The second major window is the Proof Window, seen in figure 4.5.

Figure 4.5: Igloo's proof window

• The Theory menu allows the user to create new theorems, or to close the theory.

• The Proof Steps menu allows the user to apply proof steps, such as tactics, or subgoal reordering steps, or to undo the previous proof step.

• The theorem list allows the user to pause work on one theorem, and resume work on another.

• The proof step pane provides a display of the proof in progress. This is a set of proof states (all previous proof states for the proof can be seen, or hidden as required).

• The proof engine diagnostics is used to display error and warning messages. These messages are only expected to be received from the proof assistant when there is a problem with Igloo or the proof assistant itself. Most errors should be avoided by the direct manipulation method of applying proof steps (there is little room for syntax errors, for example). This text field may also be used to allow expert users to send commands to the proof assistant in its native language. It is not currently clear how to do this with PGIP at the moment. Perhaps a rawcommand element could be added to the proofcmd (§B.1) entity.

A sample proof may be found in appendix A.