The Stateless Display Protocol

To rephrase the display protocol in a less stateful way (along the lines of the REST style), we categorize the existing messages into resources. Each resource corresponds to a type in the Relax schema of the new display protocol.

Communcation

The view here is of the broker as a web service (of sort), but that does not necessarily mean it only speaks HTTP. In fact, this may not be the ideal choice of communication channel anyway, since (in contradiction of one of the REST axioms) the broker is actually pushing messages (when the prover does something, when a new prover appears etc.) This asynchronicity (resulting from the asynchronicity of the provers) is really crucial in interactive theorem proving (see the Prosper work), and hence PGIP.

There are two ways of communicating with the broker:

  • Over a socket or other bidirectional channel. In this case, you just send PGIP messages, and get (back) PGIP messages, as before. The only change here is that now PGIP display messages will have a target resource file, which take the role of the URI, unifying different attributes like proverid etc. before.
  • Over HTTP. In this case, each resource corresponds to a URI. The display can retrieve a message in the format specified in the RelaxNG schema, which describes the state of the resource. The display may repeatedly ask for new messages, but there also needs to be a channel (an RSS feed?) where the display is informed about changes as they happen.

Resources

Resources are organised hierarchically. The root of the hierarchy is obviously our good old friend, the broker. Each resource has attributes, which can actually be proper elements in the corresponding type in the RelaxNG schema.

  • The Broker has the following attributes
    • A list of links to all known provers
    • messages
    • a global menu, or another way to access global operations such as "load file" or "shutdown broker"
    • global configurations (are there any?)
    • Version of PGIP spoken (needed?)
  • A prover has the following attributes:
    • a list of links to all files loaded by this prover
    • a status: busy, ready or exited.
    • a list of links to all known preferences
    • a list of links to all known identifiers
    • a list of links to all known objtypes ?
    • messages
    • a menu
    • a configuration for this prover, which specifies
      • a list of links to known types
      • an icon
      • help document(s) and more.
    • component specification data:
      • how to start it
      • system attributes
      • an identifier
    • an objtype has the following attributes (we could/should use XML Schema types here, but still need most of these attributes)
      • a name
      • a description
      • an icon
      • a list of links to objtypes contained herein (never understood that)
      • a list of links to preferences
    • an identifier has the following attributes:
      • a name
      • a value (a string)
    • a preference has the following attributes:
      • a name
      • a category
      • a pgipvalue
  • A file has following attributes:
    • a list of links to all text spans in the file
    • a file status (saved/modified)
  • A text span, corresponding to a single atomic command, has the following attributes:
    • a status (unparsed/being parsed/parsed/being processed/processed/outdated)
    • its text value

Remark and discussion points:

  • I don't think text spans should be organised hierarchically, although of course a structure with openblock and closeblock can be given. Should have a look at how Plato does this-- do they build proper XML trees of documents, or a flat text?
  • Files should not be sub-resources under provers-- we may want to load a particular file, and then have the broker know (by magic) which prover to start to process this file. Also, we may want heterogeneous proof script loaded by more than one prover.


da: some questions/thoughts:

  • I thought that resources should not change over time in REST, so one would rather have URIs which encoded a focus position for the prover, e.g. http://localhost:9619/Foo.thy/processedline/67 which means the file where the focus has been shifted to line 67. This gives a document which lists spans processed up to that line.
  • If resources change (e.g., when the file gets edited), what actually changes? Perhaps URIs for text spans may expire, so http://localhost:9619/Foo.thy/span/a67 may become 404'd if the file is edited and span a67 is deleted? Here the objid is part of the resource address. Or perhaps we maintain a fixed numbering for spans, and then (e.g.) all spans after position 67 change.
  • A more extreme position (but simpler) is to make every edit to the file create a new revision (so, in fact, files never seem to change). Then we include a version number in the access http://localhost:9619/Foo.thy/rev/27/processedline/67. Behind the scenes the broker will not save all these revisions, of course, and may decide to expire some of them, e.g. just retaining last 50 edits or so (lots of opportunities for Haskell space leaks).
  • We need some holder for metadata: perhaps as Foo.thy/metadata/a67 for a list of all metadata elements after span a67? Or as a special kind of span.
  • It would be nice to be able to retrieve the whole document (as pgipdoc element) as well as having access to the individual spans in it, I think. The whole document could be a persistable form of the text. Also we could offer it in different formats, e.g., piped through some style sheets to beautify or to plain text the result. Of course we could just implement the core in the Broker and add additional features like this on top using an ugly scripting language. Fetching a screen full with separate requests for each text span could be tedious over a slow connection, but conversely, the individual span approach lets us just request what we want to display lazily (viewport), not the whole document.

We could also/alternatively offer services over XML-RPC which Norbert Voelker suggested a long time ago, which gives a complementary API-oriented (possibly state-ful) view.


As far as I understand the REST view, we should have a new URI for each document, and for each message from the prover as well. Text span id's do not change, so having one resource for each seems ok. With each edit, a new document is created (which contains links to the text spans contained therein). Having one URI to retrieve the whole document seems a very good idea (and not too difficult either).

As for editing, POSTing the whole document back seems preferable to editing single text spans, which is a bit like structural editing. The broker then just needs to check which text spans have really changed, and only needs to update them (it should do that anyway).

Problem here is that parts of our application are asynchronous (the messages from the prover, and changes in the document-- if we take the document-centered view serious, then edit operations should not really create a new version). Ways to address this in REST include

  • RSS
  • Xupdate
  • Http Events (not sure if this is still actively developed)

I would suggest not getting too dogmatic about this. If the REST view becomes a limitation, we should go beyond, e.g. by providing URIs which do change; we could call them channels instead of resources to make it clear. Well, maybe not. The main point about this is to get a clean definition of the interface (e.g. by sorting out precisely which parts are stateless resources, and which are not).

In that vein, an additional XML-RPC interface seems a good idea too.

-- ChristophLueth - 07 Jul 2007

PGIP Messages and Commands

Here, we give a list of all display messages (sent from broker to display) and display commands (sent from display to broker). We given them here because all these messages need to find their place in the resources listed above, corresponding to attributes of resources or change requests.

From Broker to Display

Messages from the broker to the display are given by the entities todisplaymsg and fromprovermsg in the Relax schema, which resolve to the following entities and, finally, messages.

Entity Message Resource
kitconfig usespgip Broker, Prover
usespgml Broker, Prover
pgmlconfig Prover?
proverinfo Prover
hasprefs Prover
prefval Prover
displayinfo Broker/Prover
setids Prover
addids Prover
delids Prover
idvalue Prover
menuadd Prover
menudel Prover
proveroutput ready Not seen by display
cleardisplay Not seen by display?
proofstate Prover
normalresonse Prover
errorresponse Prover
scriptinsert Not seen by display
metainforesponse Not seen by display
parseresult Not seen by display
fileinfomsg informfileloaded File
informfileretracted File
informguise Not seen by display
brokermsg brokerstatus Broker
proveravailmsg Prover
newprovermsg Prover
proverstatemsg Prover
dispmsg newfile File
filestatus File
dispobjmsg Text spans

From Display to Broker

Messages from display to broker are given by the entities fromdisplaymsg and toprovermsg, which resolve to the following entities and messages:

Entity Message Resource
dispfilecmd loadparsefile Prover
newfilewith Prover
dispopenfile Prover
savefile File
discardfile File
dispobjcmd setobjstate Text span
editobj File, Text spans
createobj File, Text spans
inputcmd Prover?
interruptcmd Prover
brokercontrol launchprover Broker,Prover
exitprover Prover
restartprover Prover
proversquery Broker
shutdownbroker Broker
brokerstatusquery Broker
pgipconfig Broker (creates Prover resources)
proverconfig askpgip Broker (for Prover not seen by display)
askpgml Broker
askconfig Prover
askprefs Prover (Preference?)
setpref Prover (Preference?)
getpref Prover (Preference?)
provercontrol Display uses brokercontrol messages
improperfilecmd Display uses dispobjfilecmd messages
improperproofcmd Not used by display (display edits text spans)
properfilecmd Not used by display
properproofcmd Not used by display
proofctxt askids File (Theory)
askrefs File, Identifier
showid File, Theory, Identifier
askguise Not used by display
parsescript Display uses dispobjmsg instead
showproofstate Not used by display
showctxt Not used by display
searchtheorems Prover
setlinewidth Not used by display, legacy
viewdoc Prover? Semantics unclear

-- ChristophLueth - 03 Jul 2007

Topic revision: r4 - 07 Jul 2007 - 11:53:04 - ChristophLueth
 
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies