TWiki
>
PG Web
>
PGIP
>
PGIPMunichMeetingFeb07
>
PGMeetingNotesDayTwo
(09 Mar 2007,
DavidAspinall
)
E
dit
A
ttach
Notes on
PGIP
Meeting, Day Two
Notes on PGIP Meeting, Day Two
Structure of history and synchronization
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
E
dit
|
A
ttach
|
P
rint version
|
H
istory
: r1
|
B
acklinks
|
R
aw View
|
Ra
w
edit
|
M
ore topic actions
Topic revision: r1 - 09 Mar 2007 - 14:45:07 -
DavidAspinall
PG
PG Web
PG Web Home
Changes
Index
Search
Notifications
RSS Feed
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