Use cases for editing

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

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


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

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 display?!) 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.

Edit | Attach | Print version | History: r4 < r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 10 Oct 2006 - 23:46:42 - 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