1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
-*- mode:outline -*-
* Priorities
============
A (High) to be fixed before release (Version 2.0)
B (Medium) desirable to fix at some point
C (Low) probably not worth wasting time on
* This is a list of things which need doing in the generic interface
====================================================================
A Structured review of complete system. Is there redundant code?
Can some of the LEGO/Coq specific code made generic? Re-engineering.
(2h hhg & tms)
A Update source documentation and manual, in particular document bugs
and workarounds
(4h hhg & tms)
A Implement more generic mechanism for large undos (2h)
COQ: C-c u inside a Section should reset the whole section, then
redo defns
LEGO: consider Discharge; perhaps unrol to the beginning of the
module?
B Implement proof-find-previous-terminator and bind it to C-c C-a
(45min tms)
B Technical documentation to record expertise and allow users of other
proof systems to adopt generic package (40h hhg & tms)
A Fixing up errors caused by pbp-generated commands; currently, script
management unwisely assumes that pbp commands cannot fail (2h tms)
C pbp code doesn't quite accord with the tech report; in particular it
decodes annotations eagerly. Lazily would be faster, and it's what
the tech report claims
--- djs: probably not much faster, actually.
B file handling could be more robust; perhaps one should always cd to
the directory corresponding to the script buffer (currently only
done for the buffer which starts up the proof system) (30min tms)
B replace (current-buffer) by proof-shell-buffer/proof-script-buffer
where ever possible (30 min tms)
B Allow bib-cite style clicking on Load/Import commands to go to file.
C LEGO and Coq modes overwrite each other.
C We need to go over to piped communication rather than ptys to fix
the (Solaris) ^G bug. In this circumstance there's a bug in the
eager annotation code
C Outline-mode does not work due to read-only restrictions of
protected region
B Remove LEGO-specific code in proof.el: for example,
proof-shell-eager-annotation-end, proof-included-files-list.
(added by hhg)
* Here are things to be done to Lego mode
=========================================
A set up regular definitions to support definitions of the form
id == term (10min; tms)
A fix Pbp implementation (10h; tms)
A LEGO mode might incorporate changes to Coq mode menu, in particular
making help refer to the info file (30min tms)
A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
annotations are recorded in the object file. This needs to be
changed in the SML code. (initially 2h tms)
C Mechanism to save object file
A Equiv, Next,... aren't handled properly, because LEGO does not
refresh the proof state. Perhaps it would be easiest to get LEGO to
output more information in proof script mode (2h tms)
A Error messages need to be revised e.g., if an import fails, LEGO
outputs
Error in file: search: undefined or out of context: should
(* closing file ./blah.l; time= 0.010000 gc= 0.0 sys= 0.0 *)
Error: Unwinding to top-level
but script management only prints the last line. (5h tms)
* Here are things to be done to Coq mode
========================================
B Add Patrick Loiseleur's commands to search for vernac or ml files.
C Sections and files are handled incorrectly.
A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
correct command if I undo up to the lower lemma, but the buffer
undoes to the upper lemma. I.e., if I start Lemma x, then prove
Lemma y, then finish x, and undo lemma x, then lemma y gets undone
in the buffer as well. (45min hhg)
[ This seems to have corrected itself... hhg ]
B Proof-by-Pointing (10h hhg)
A Add coq-add-tactic with a tactic name, which adds that tactic to the
undoable tactics and to the font-lock. (2h hhg)
* Emacs19
=========
B The proof-locked-span isn't set to read-only, because overlays don't
have that capability. This needs to be done with text-regions.
(2hr hhg)
|
