Notes on PGIP Meeting, Day Two

Structure of history and synchronization

• Free navigation, with unlimited/unrestricted undo
  • Supported in Matita
  • May be supportable in Isabelle/Isar: top level supports purely functional view
  • ``We should support this in PGIP as a prover configuration option``
  • This influences the undo model, which becomes simpler
  • Question: should the prover implement this?
  • Answer: if it does, it needs a reply to undo request to say how much was undone

• Support for completely parsed and processed documents
  • Some systems (e.g., Agda, maybe Mizar), maintain view of document as completely processed
  • Can we support this in PGIP?
  • Seems to be another configuration option:
    • either classic mode: three regions, locked processed and queued regions
    • or ``complete`` mode: parse and quick-prove whole document, support replacement

-- DavidAspinall - 09 Mar 2007