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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
-*- 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
====================================================================
B Prune dead code. (1h)
B Add support to proof.el for *not* setting variables for
commands which aren't supported by a prover. For example,
in Isabelle there is no such thing as killing a goal.
For the minimum set of variables to cover, see FIXME's in isa.el
(1.5hrs)
B Outsource script management features from proof.el to
proof-script.el (1h)
A Write function proof-retract-file. (30min tms)
Currently, the command ForgetMark (for LEGO) is hardwired in
proof-steal-process.
B Improve documentation in proof.el to help porting/understanding
Also add notes into script-management.texinfo.
(ongoing, da).
B Fixup sources to follow Elisp conventions better.
The first line of documentation of functions and
variables should be a whole sentence. See output of
hyper-apropos for why. (1hr)
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?
A Multiple files are sometimes handled incorrectly, because the
function `proof-steal-process' cannot figure out that some files have
already been processed. This is most likely caused by the ad-hoc
equality test on file names. Instead, one could employ
the built-in `file-truename' to trigger *canonical* file names.
(1h tms)
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)
B Support for x-symbols package
C XEmacs sessions seem to grow excessively in terms of memory
allocation. Perhaps some of the spans aren't removed properly?
Setting a limit on the size of the process buffer doesn't seem to
help.
A 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)
A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
where ever possible (30 min tms)
A Replace "You are not authorised for this information." by a proper
documentation (2h)
A Reengineer *-count-undos and *-find-and-forget at generic level
(3h)
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)
B support font-lock in response buffer
B Response buffer: after an error message has been displayed; ensure
that the error message is visible
B Introduce keybinding to save the proof e.g., in LEGO, this should
insert "Save id" or "$Save id" depending on the name of the theorem.
B use proof buffer instead of response buffer and leave non-proof
state output in the process buffer (1h)
B Remove duplication of variables e.g., proof-prog-name and
lego-prog-name . (1h)
B As well as duplicated variables, we also have duplicated modes,
which could be removed. We never use proof-shell-mode, proof-mode,
pbp-mode, only the derived instances.
Shouldn't the generic interface directly *define* the derived
version required? (1h to fix)
B Fixup implementation of "spans". Add documentation!
(2h)
* Proof-by-Pointing
===================
A Fixing up errors caused by pbp-generated commands; currently, script
management unwisely assumes that pbp commands cannot fail (2h tms)
A Rename pbp-mode to response-mode (which doesn't support any actual
proof-by-pointing) (30min)
A Outsource actual pbp functionality (30min)
(separate pbp annotations from other annotations)
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.
* Here are things to be done to Lego mode
=========================================
A fix Pbp implementation (10h; 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
B 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 set proof-commands-regexp to support indentation for commands
(10min hhg)
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)
* Here are things to be done to Isabelle Mode
=============================================
A Get basic features working:
proof state extraction -- okay.
undo -- needs work.
Check these things:
abort-goal-regexp
B Write perl scripts to generate TAGS file for ML and thy files.
(6h, I've completely forgotten perl)
B Add useful specific commands for Isabelle. Many could
be added. Would be better to merge in Isamode's menus.
(probably a week's work to bring together Isamode and proof.el,
making some of Isamode generic)
B Add ability to choose logic. Maybe not necessary: can use default
set in Isabelle settings nowadays, in the premise that most people
stick to a particular logic? But then no support for loading
user-saved databases.
(ponder this)
* 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)
* Release
=========
A remove CVS history in all files
A extend Copyright to 1998
A fix INSTALL file, add COPYING note
A write Makefile targets to build documentation formats
and generate distributable tar.gz file, tag sources,
compile .elc, web page (?), with release version.
Perhaps add subdirectories doc/ generic/ coq/ lego/ isabelle/
(3h, da moderately willing to do the dirty work)
|
