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

Topic revision: r1 - 09 Mar 2007 - 14:45:07 - 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