On prover_id and component_id

Presently, a prover is identified by an attribute prover_id in display messages, which uniquely identifies the running instance of this prover. If we start a second instance, it will get another prover_id. This is bad, because it requires displays to keep the prover_id, but the main drawback is that we can't just restart a prover and let it re-use the source files the previous instance had already parsed and processed.

Therefore, I suggest that we identify the prover_id with the component_id of the prover. A component_id uniquely identifies one component, e.g. the prover "Isabelle 2005/HOL", but not its running instance. We can keep the name of the attribute.

This means that displays refer to a prover by "type", rather than a unique instance. The drawback is that we cannot support more than one running instance of the same prover, but given that this is bound to confuse the user anyway, this may be an advantage.

This change is wholly transparent to displays. We could make the startup/broker information protocol a bit simpler (but that would break compatibility with existing displays):

Present:

brokermsg  = 
    brokerstatus      # response to brokerstatusquery:
  | proveravailmsg      # announce new prover is available
  | newprovermsg      # new prover has started 
  | proverstatemsg      # prover state has changed (busy/ready/exit)

brokerstatus  = element brokerstatus 
                       { knownprovers, runningprovers, brokerinformation }

knownprover   = element knownprover   { componentid_attr, provername }
runningprover = element runningprover { componentid_attr, proverid_attr, provername }

knownprovers   = element knownprovers { knownprover* }
runningprovers = element runningprovers { runningprover* }
brokerinformation = element brokerinformation { text }

proveravailmsg  = element proveravailable { provername_attr,
                                            componentid_attr }
newprovermsg    = element proverstarted { proverid_attr
               , componentid_attr
                              , provername_attr
                              }
proverstatemsg = element proverstate { 
                       proverid_attr, provername_attr,
                       attribute proverstate {proverstate} } 

proverstate    = ("ready" | "busy" | "exitus")

Suggested changes:

• remove knownbrokers, runningprovers message, and replace brokerstatus with the following, so the broker just reports the state of all provers it knows (the state will show wether provers are running or not):

brokerstatus  = element brokerstatus {proverstatemsg*, brokerinformation }

• remove newprovermsg (and replace it with appropriate proverstatemsg).
• Rename componentid_attr in proveravailmsg to proverid_attr to be consistent.
• Do we need a new proverstate "started" for provers having just started?

Suggestion is to first implement the new meaning of prover_id as suggested above, and keep the old brokercontrol messages for a while.

-- ChristophLueth - 26 Sep 2006

This seems fine. Probably there aren't many components using the brokercontrol messages yet so you could go ahead with simplifying that part too.

On started: generally it's good to be able to show information ("Starting Isabelle process..." "succeeded") to the user so they know what the machine is trying to do. But we don't always have to send this in the PGIP protocol, we can just make it into status messages originating from the Broker that the display will show or not. We need to think carefully which cases really need PGIP handling and which not.

-- DavidAspinall - 29 Sep 2006