Library Management

In order to fully implement the method of creating new theories in Igloo, we require some additional functionality from PGIP. This is needed if we wish to truly separate the proof assistant from the user interface and allow them to run on separate machines.

A simple convention that proof assistants could use is:

• Each theory is contained within a single storage unit.
  This storage unit may typically be a file, but this is not required.

• There is a set of storage groups which contain theories that the user has access to.
  Again, this may typically be filesystem directories, but this is not required.

• Storage groups may contain other storage groups, in an acyclical manner.
  This way the interface does not need to worry about falling into an infinite loop while searching for theories.

Even if the proof assistant does not implement the conventions mentioned in the first point internally, it should not be hard to map to and from most other sensible practices.

If multiple theories are stored in a single storage unit (such as a file), all the proof assistant would need to do is scan through the file looking for theory names. Catenation of this type is regarded as generally bad practice in software engineering circles, and I claim is equally bad in theorem proving. On the other hand, if a single theory may be spread across multiple storage units, then the proof assistant should easily be able to catenate them before allowing the user interface access.

If the proof assistant does not satisfy the second point above, (theories may be stored absolutely anywhere in a general filesystem for example), then it is a safe presumption that the proof assistant has some method of easily distinguishing theories from other objects. In this case it is assumed that the proof assistant has some other method of listing

The user interface needs a way of discovering this information, so we propose to add the following elements to the PGIP schema (in RELAX NG format [1]):

• element theorylistdirs { empty }
  The user interface sends this message to the proof assistant to discover which directories hold theory files that can be used. This directory need not be the local directory that the proof assistant works with, there just needs to be a simple mapping from the proof assistants local theory storage tree to the virtual tree it tells the user interface about.

• element theorydir { dirname_attr }
  This represents a (virtual) directory that holds (virtual) theories.

• element theorydirs { theorydir+ }
  

  The proof assistant responds to a theorylistdirs message with a theorydirs message.

• element theorylist { dirname_attr }
  

  The user interface can send this message to the proof assistant to ask for a list of all theory files that exist in a named directory.

• element theoryfile { thyname_attr }
  

  This represents a theory file.

• element theories { dirname_attr, theoryfile+ }
  

  The proof assistant responds to a theorylist message with a theories message.

• element theoryshow { name_attr }
  The user interface asks to see the text within the named theory.

• element theory { text }
  The proof assistant responds to a theoryshow message with a theory message, which contains the proof text of the theory (which is specific to the proof assistant).

If these XML elements were added to PGIP's filecmd then the user interface would not need to know anything about the directory structure and location of theory files ahead of time. This is an abstraction of the current system, which makes use of the local file system commands.

This also leaves the proof assistant to implement whatever storage method for theories it chooses. In Isabelle this is the standard filesystem mechanism, but with the proposed abstraction in place this could be simply replaced with more complex and powerful storage methods. A relational database is the obvious example that springs to mind.