We want to allow flexibility but be careful in case of race conditions.

Example:

- The user requests some object B to be processed, message sent to broker.
- The user then edits object A on which object B depends.

Step 2 might happen before the broker has responded to the first message. Then - The display tries to re-parse the edited object, sending
`editobj`

- Likely confusion for all concerned.

Here the simplest fix seems to be for the display to block when it has an outstanding request to the broker and is waiting for an object status change. The broker is supposed to be speedy about providing object status changes (transitions to "parsed" can take a little bit longer than transitions to "being proved", but should still be quick).

Update July 07: not clear that this case is problematic actually. The `editobj`

in the display **must** invalidate the old object identifiers, so if the broker
sends updates for them, they will not be shown (avoiding the situation
that some ill-formed theorem appears to have been proven!). The display
can be silent about this (perhaps a diagnostic), maybe the broker is
processing some old queue of messages.

Here are MoreThoughtsAboutDisplayProtocol

Simple answer for sanity: this is **not allowed**! If another display tries to open a file for editing/take an
edit lock we give a warning/error message.

The user has in her buffer:

- Theorem A: blah QED
- Theorem C: blah QED

She now goes back and inserts

- Theorem B: blah QED

between the two. Do we allow this? The possibilities are:

- This is a valid position for the new theorem:
*B does not depend on C* - This is not a valid position:
*B depends on C*

In the second case, we really want the user (or the broker?!) to reorder the user's file to respect the order seen.

Constraint: here we require that the linear dependency realised in the file is compatible with the actual dependency that the theorems have. This is similar to Pons' requirement of intra-proof consistency between tactics in a single proof.

The user has in her buffer:

- Theorem A: blah QED
- Theorem B: blah QED
- Theorem C: blah QED

And suppose that theorem C does not depend on theorem B.

She now goes back and edits the proof of theorem B. Because the Broker uses non-linear dependency, it outdates theorem B but not theorem C.

But the new proof of theorem B now refers to theorem C!

Again, the broker should spot that the current linear order of the file now violates the dependency relation.

It should offer to make theorem B fly to somewhere after theorem C!

Topic revision: r4 - 18 Jul 2007 - 14:11:14 - DavidAspinall

Copyright © 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

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies