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
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
|
-*- mode:outline -*-
$Id$
* Priorities
============
A* (SUPERSONIC URGENT) to be fixed yesterday.
A (URGENT) to be fixed immediately for pre-release
B (High) to be fixed before release (Version 2.0)
C would be nice to fix before release of 2.0; but not crucial
D (Medium) desirable to fix at some point
X (Low) probably not worth wasting time on
* This is a list of things which need doing in the generic interface
====================================================================
B proof-find-next-terminator doesn't work properly:
first;second;third
^
Invoking proof-find-next-terminator in cursor position (^) should
move point to "t". Currently, it doesn't do anything. This is a
bug.
B Add proof-rsh-command and note in documentation about how to
use widely-advertised "remote shell" feature. (1hr)
D Add proof-quit-command: some provers may like a quit command to be
sent to the shell, not just EOF ! (see proof-stop-shell).
D Multiple files (after basic feature added): handle failures in
reading ancestors.
A* Fix Non Sequitur nonsense with Isabelle when warnings appear before
proofstate. (da, 1hr?)
A* Check & fix support for a recent version of FSFmacs. (da, 2hr).
A Add support for putting a locked region in processed files.
(tms 4h)
B Clean up proof-assert-until-point behaviour. Discussion results:
1. At the moment we get an odd error if it is run in
the locked region. This is a bug. Should behave same
as proof-assert-next-command in this case (simpler) or
give better error message.
2. At or before first character of proof command, "nothing to do"
error message. This is a bug. Should behave same
as proof-assert-next-command in this case.
[1,2 have been "fixed" by rebinding C-c RET to
proof-assert-next-command for now, eventually
this may form a new version of proof-assert-until-point]
3. Toolbar movement functions should operate just on the locked
region, and not move point. They should maintain visibility of
end of locked region, though.
4. Movement and possible insertion of spaces/newlines for
when new commands are added to the buffer needs careful
thought!
A Write function proof-retract-file. (30min tms)
Currently, the command ForgetMark (for LEGO) is hardwired in
proof-steal-process.
A Implement more generic mechanism for large undos (2h tms)
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)
A replace (current-buffer) by proof-shell-buffer/proof-script-buffer
where ever possible (30 min tms)
B Simplify icons in proof toolbar (make double triangles into single
ones). (1hr, da)
B Revise ProofGeneral.texi and publish LaTeX version as an LFCS
Technical Report (2 days; da + tms)
B Provide a sensible default frame/buffer layout (4h)
B A less drastic version of proof-restart-script would be useful:
one that doesn't involve killing off the proof assistant process
and restarting that -- it can take ages!
We want two different modes of restarting:
1. Restart all: clear all context and kill proof process.
2. Restart some: clear context, do some retraction/kill goals
in proof process.
Add kill buffer hook to script buffer which does restart some
in case it's the active buffer.
(da, 20mins)
B Improve script stealing stuff. It should display the other buffer
which was scripting. Proof there should be killed off and
locked region shrunk/deleted accordingly.
C Improve proof-goal-command and proof-save-command:
`proof-goal-command' should be more flexible and support a
placeholder for the name and the actual goal. In LEGO, we have
Goal foo : absurd;
...
Save foo;
Perhaps functions at the generic level to make suitable
values for the hook, e.g.,
(setq proof-goal-command (proof-prompt-named-goal "Goal %s :" "%s;"))
C Cleanup handling of proof-terminal-string. At the moment some
commands need to have the terminal string, some don't.
da: I suggest removing proof-terminal-string altogether and
adding back the semi-colons or fullstops at the specific level.
It's not a big deal and would support other provers which
may use a mixture of terminators, or no terminators at all.
C Investigate and improve indentation/font-locking code.
At the moment editing .ML files in Isabelle Proof General is
*very* slow. Moreover the indentation is screwy. Also
seems screwy in LEGO/Coq PG. (da, 2hr)
C Improve Linux install via spec file: hack the load line into
site-start.el. Could use emacs to determine its location,
automatically detect both XEmacs and Emacs, etc. See if
other Emacs packages do something clever.
B New buffer model:
1. Script buffers
2. Response buffer
3. (optionally part of response buffer) goals buffer
4. (hidden) process buffer
5. Minibuffer for additionally sending information to the process
B proof-toolbar: Fixup movement of point (choice of
up and down functions). Add toolbar to response mode too.
B Split code; particularly proof.el
C toolbar icons: Automatically generate reduced and
pressed/greyed-out versions from gimp xcf files. Keep the
xcf files under CVS rather than xpm files. (2h, da)
C Better support for adding a new prover: give error messages which
hint at what variable to set (see proof-issue-goal for example).
C Functions for next,previous input a la shell mode, but in proof
script buffer (3h, da).
X Read-only mode of extents sometimes gets in the way: for example,
if file changes on disk, can't reload it via usual functions.
Can this be improved? Always have to retract first, and that
always leaves stuff around.
C User-level functions:
1. add new version of undo-until-point which behaves analogously to
proof-assert-next-command.
2. make version of proof-restart-script which will start or
restart the proof assistant as appropriate. (It's handy to have
a direct function to start the proof assistant).
(1hr, da)
C Write test schedule for things to try out with a new instantiation
of Proof General.
B Add skeleton instantiation files for a dummy prover "myassistant" to
make it easier to add support for new assistants -- looking at
any of the existing modes is confusing because of the
prover-specific stuff. Ideally it should work for one of
the default provers as an impoverished example mode.
(2h, da will do for Isabelle)
D Code in proof.el assumes all characters with top bit set are special
instructions to Emacs. This is rather arrogant, and precludes proof
systems which utilize 8-bit character sets! Needs repair. (3h)
D Prune dead code. (1h)
D 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
(da, 1.5hrs)
D Outsource script management features from proof.el to
proof-script.el (1h)
D Improve documentation in proof.el to help porting/understanding
Also add notes into proof.texinfo.
(ongoing, da).
C Fixup sources to follow Elisp conventions better.
1. The first line of documentation of functions and
variables should be a whole sentence. Subsequent lines should
*not* be indented. See output of hyper-apropos and
poor formatting of current comments. (1hr)
2. Replace defvar's by defconst's where appropriate.
Introduce new defconsts.
3. Check on use of "*" in docstrings. Should be used for
variables which are user-level options, only.
4. Upper case in docstrings is reserved for the name
of a function's arguments, usually.
D Implement proof-find-previous-terminator and bind it to C-c C-a
(45min)
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). This could be
achieved with a hook which is not set by default. [Remember to add
user documentation] (30min tms)
B Reengineer *-count-undos and *-find-and-forget at generic level
(3h)
D Allow bib-cite style clicking on Load/Import commands to go to file.
D support font-lock in goal buffer
C Unify toolbar and menu functions.
D Remove duplication of variables e.g., proof-prog-name and
lego-prog-name for Coq and Lego. (1h)
D Fixup implementation of "spans": Add documentation!
(30 mins)
C Make completion more generic. For Isabelle and Lego, we can build a
completion table by querying the process, which is better than
messing with tags.
X Support for x-symbols package.
Provers with sophisticated/configurable syntax should tell Emacs
about their syntax somehow, rather than trying to duplicate
specifications inside Emacs.
X Comment support is not very generic: we don't support end-of-line
terminated comments. Is there any case where this might be
worthwhile? (2h to add it).
X Splash screen: Add fancy text logo to it. Centre the display
prettily.
X Write a Makefile for the distribution. It can do things like
install the info file properly. The work is at the moment done
in the RPM spec file instead.
X Make process handling smarter: because Emacs is single-threaded,
no process output can be dealt with when we are running some
command. This means that it would be safe to extend the
red region, by putting more commands on the queue. Also it would
be safe to implement a clever undo command which worked on the
red region: if there are commands waiting to be processed, we
could remove them from the queue. If there are no commands waiting,
we have to wait until something becomes blue to undo it by sending
a command to the process.
X Ideas for efficiency improvements. Rather than repeatedly
re-parsing the buffer, we could parse the whole buffer *once*
and make adjustments after edits, like font-lock. We could
make an extent for every command, and set it to "blue", "red"
or "clear" as appropriate. (This would allow proofs to be
sent out-of-order to the proof process too, although perhaps
that's not so nice).
The function proof-segment-up-to could be made to cache its
result.
X 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. Document this problem so that it can be
tested for future versions. [Currently the problem is documented in
Email messages sent to lego]
* Proof-by-Pointing
===================
B Change proof by pointing (pbp) stuff into proofstate buffer stuff.
C Fixing up errors caused by pbp-generated commands; currently, script
management unwisely assumes that pbp commands cannot fail (2h)
B Rename pbp-mode to response-mode or goals-mode (which doesn't
support any actual proof-by-pointing) (30min)
B Outsource actual pbp/goals functionality (30min)
(separate pbp annotations from other annotations).
Make a file proof-goals.el.
X 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
=========================================
C fix Pbp implementation (10h)
A release new version of the LEGO proof engine (4h tms)
C 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)
C LEGO should not issue warning messages triggered by the interactive
use of the Module command when invoked by the interface e.g.,
Lego> Module nstderror Import stderror;
Including module nstderror
Warning: module name "nstderror" does not equal filename ""!
(15min)
X Mechanism to save object file
C Improve legotags. I cannot handle lists e.g., with
[x,y:nat];
it only tags x but not y. [The same problem exists for coqtags]
* Here are things to be done to Coq mode
========================================
D set proof-commands-regexp to support indentation for commands
(10min hhg)
D Add Patrick Loiseleur's commands to search for vernac or ml files.
X Sections and files are handled incorrectly.
B 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 ]
D Proof-by-Pointing (10h hhg)
B Add coq-add-tactic with a tactic name, which adds that tactic to the
undoable tactics and to the font-lock. (2h hhg)
C Improve coqtags. I cannot handle lists e.g., with
Parameter x,y:nat
it only tags x but not y. [The same problem exists for legotags]
* Here are things to be done to Isabelle Mode
=============================================
B Get basic features working:
proof state extraction -- okay.
undo -- needs work (undoes to much).
error detection -- seems okay.
what else?
Check these things:
abort-goal-regexp
Still get non-sequitur errors, why?
BUG: undo after last step undoes till top of proof in
process buffer, not in script!
B CRUCIAL: Do something to manage .thy and .ML files coherently.
At the moment loading one into Isabelle will force the
processing of the other. We could ask that users develop
proof scripts in another kind of file entirely, or a file
with a different name. But that's an ugly hack.
But what else can we do??
(Probably answer: Isabelle needs to support non-automatic
reading of ML file: a function "use_thy_only" ).
B (part of above): Handle proof-retract-file by querying Isabelle
about the decendants of a file. Then all the descendents can
also be unlocked.
X Write perl scripts to generate TAGS file for ML and thy files.
(6h, I've completely forgotten perl), or better:
D Implement completion for Isabelle using tables generated by
the running process.
D 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)
D 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)
X New features ideas:
1. Manage multiple proofs (markers in possibly different buffers)
* Emacs19
=========
D 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
=========
B validate/fix web pages.
|