Use cases for editing

Various race conditions in display<->broker<->prover

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

Example:

  1. The user requests some object B to be processed, message sent to broker.
  2. 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
  3. The display tries to re-parse the edited object, sending editobj
  4. 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

More than one display edits a file

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.

Insertion in non-linear dependency model

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:

  1. This is a valid position for the new theorem: B does not depend on C
  2. 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.

Introducing dependency in non-linear model

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