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