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
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
|
-*- mode:outline -*-
Proof General Low-level List of Things to Do
============================================
$Id$
* Contents
==========
* Priorities
* Things to do in the generic interface
* Things to do for Proof-by-Pointing
* Things to do for Lego
* Things to do for Coq
* Things to do for Isabelle
* FSF Emacs issues
* Stable version release checklist
* Things to do for Proof General Project
* Priorities
============
A (URGENT) to be fixed immediately for next pre-release
B to be fixed before next release (Version 2.1)
C would be nice to fix before release of 2.1; but not crucial
D (Medium) desirable to fix at some point
X (Low) probably not worth spending time on
* Things to in the generic interface
====================================
A Usability enhancement:
Movement of point after assert/retract commands
- configure by default for one command/line.
- Add option for many commands per line.
- Maybe shell like behaviour with pressing return?
A Usability enhancement:
Optional argument to delete region should be removed
from C-c C-u, pressing quickly in succession can delete
from buffer
A Usability enhancement:
Rationalize next and undo. Make same as toolbar
commands and have different commands for power users
to assert/retract until point.
A Usability enhancement:
Have toolbar button/command to goto a point.
Proof General itself should work out whether it's a
retraction or advancement!
A Usability enhancement:
Add toolbar button for interrupting.
B New feature:
Add command and button for searching for a theorem
(possibly matching a given constant, or the proof state).
B Finish design of new icons.
D bug: outline mode when proof-strict-read-only is nil ought to
work, but there may be problems.
D bug: mentioned by Martin H. with Lego: "don't know what I should
be doing..." error when it shouldn't happen.
C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting
ELISP_DIRS somehow.
D Update logo to include new "???" prover badge (maybe it should be
"...") from graphics file elsewhere (da)
D Add etc/announce to web pages somewhere.
B Improve relocatability of RPM package, and produce package for XEmacs
which installs directly under ~/.xemacs/packages.
C Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General
info file into a good place.
C Check compilation okay, check on use of eval-and-compile.
C Support for proof-guess-command-line, new generic setting added
by Patrick.
D Key binding and interface issues
- Consider change for prefix argument for C-c C-u and C-c u,
it's quite easy to accidently delete by pressing C-c C-u
repeatedly.
D CVS repository issues.
Where are obsolete 'fileattr' files generated from/maintained?
Should junk these (which appear to say that tms is watching everything).
B QUESTION: why do we have proof-shell-proof-completed-regexp's
perhaps objectionable behaviour of forcing the response buffer?
Would it be safe just to set the proof-shell-proof-completed flag
and output as usual? (The effect would be to allow Isabelle's
completed proof message to appear in the goals buffer since it's
marked up as a proof state output)
C proof-shell-exit has a time delay of 10 secs built-in,
before which the process is killed off.
This should be configurable to allow for proof assistants
which really want to do some work before exiting, for
example writing persistent databases out or the like.
Also this fact should be documented.
C Add support for XEmacs 21 packaging. Make suitable updates available
on web page, and make RPM put things in the right place so no .emacs
file may need editing(?). [4 hours]
B Fixup display problems.
The window dedicated stuff is a real pain and I've
spent ages inserting workarounds. Why do we want it??
The latest problem is that with
(setq special-display-regexps
(cons "\\*Inferior .*-\\(goals\\|response\\)\\*"
special-display-regexps))
I get the script buffer made into a dedicated buffer,
presumably because the wrong window is selected in
proof-display-and-keep-buffer?
B 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.
B outline configuration should be generic (or else documented for
each prover separately, since not guaranteed to work for all).
B Improve behaviour when switching active scripting buffer.
Now kill buffer function retracts partially-processed files
and removes them from proof-included-files-list, we could
allow switching between scripting buffers automatically,
(perhaps with an option akin to the old "steal scripting?" idea).
B Check matching code carefully, in view of bug reported (now fixed)
for Isabelle.
Examine syntax tables for all instances, and whether
word matching is based on whitespace constituents or non-word
constituents. [6 hrs]
C Reorganize menus in a better way. Have generic scripting commands
for keyboard or menu/toolbar use. (2hrs)
C Implement proof-auto-retract idea. (4hrs)
C Make and test generic versions of <..>-goal-command-p,
<...>-count-undos, to simplify prover-specific code.
C Improve handling of process exiting early (see note at
end of proof-shell-mode). (30mins)
C da: Suggested improvement to interface for included files:
Currently have two cases: processing a single file, and
retracting which updates the included file list arbitrarily
(but assumes that only removals are made). A simpler and
more general interface would be to just have the second
case, and automatically find removed files and added files
between two versions of proof-included-files-list and
unlock or lock buffers appropriately. We could provide
a useful default function based on three regexps:
retract-file-regexp, add-file-regexp, clear-filelist-regexp.
Master regexp process-file-regexp would match all of
these cases. Could be multiple matches of the three above
within a single process-file-regexp to avoid processing
lots of urgent messages. (3h)
C da: goal-hyp: this should be more generic. At the moment, there are
generic variables which are only used in the specific code:
proof-shell-goal-regexp and proof-shell-assumption-regexp.
This is confusing. I suggest making lego-goal-hyp the
default behaviour for proof-goal-hyp-fn a hook function.
That will work for Isabelle too. (15 mins)
C Process handling output.
Handling mixtures of urgent and non-urgent messages:
at the moment any non-urgent output *before* an urgent
message will not be displayed in the response buffer.
Accept this as a feature for now.
C proof-goal-command-regexp: the syntax of Coq spoils the
uniform use of a regexp to match a goal (since it allows
goals to begin Definition ...). Nonetheless, it would be
for this not to mean that everyone else needs to set
proof-goal-command-p. Perhaps some crucial regexps can
be used via proof-string-match-p which would allow a
function to be invoked instead? (Cf font lock).
C Improve indentation code and see why it's so slow (at
least for Isabelle). Enable it for particular provers if
it works okay (but must test in on large files).
C Regions in script buffer have nice "name" property and configurers
have to set regexps carefully so that it works, but is it actually
used anywhere? What's it good for?
C ROBUSTness: deal gracefully with possibility that goals buffer is
killed during session. (2h)
D Add support to filter out unwanted noise from the prover by setting
up a regular expression proof-shell-noise-regexp (1h)
C support for templates e.g., in LEGO it would be nice if, by default,
fresh buffers corrsponding to file foo.l would automatically insert
"Module foo;" (1h)
C Remove "FIXME notes" which are just notes I've put in about old
code in case something breaks (da, 10mins).
C Check on all FIXME notes.
C automise testing procedures in etc/
C Write proof-define-derived-mode which automatically adds a
call back hook somehow. Propose this to maintainer of derived.el.
(1.5hrs)
C Toolbar icon for `proof-execute-minibuffer-cmd' (1.5hrs)
C Improve web pages after suggestions in doc/notes.txt
(da, 1.5hrs)
C proof-issue-goal should refuse to work when a proof is in progress.
Similarly proof-issue-save should refuse to work when a proof
hasn't been completed! Algorithm: Search the last goal and check
length of span. (45min)
C Bug in proof-retract-until-point when called twice in succession:
calls backward-char at beginning of buffer. (Should say no
locked region, or "nothing to retract"). Problems is that
there is a proof-locked-end, but it's at (point-min). (30min)
C 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. Movement and possible insertion of spaces/newlines for
when new commands are added to the buffer needs careful
thought! (1h)
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 Functions for next,previous input a la shell mode, but in proof
script buffer (3h, da).
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.
C 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)
C 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)
C Reengineer *-count-undos and *-find-and-forget at generic level
(3h)
C Unify toolbar and menu functions. (1h)
C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's.
Generic problem, really: maybe CRs should be stripped, and just first
line of multiline urgent message displayed in minibuffer.
D Perhaps goal..save sequences should be closed also by the appearance
of a new goal, even though this may be a "broken" proof. At the
moment, undoing past the new goal causes errors:
<goal>
...
<new goal>
..
Will ACS idea handle this?
D Better support for adding a new prover: give error messages which
hint at what variable to set (see proof-issue-goal for example).
D Multiple files: handle failures in reading ancestors.
D Provide a sensible default frame/buffer layout (4h)
D Implement mouse drag-and-drop support for selecting subterms in the
goals buffer and copying them in a script buffer. This could be
implemented by defining button2 in the response buffer and setting
button2up in script buffers. (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.
D proof-find-next-terminator is too slow when it needs to parse
a long buffer. Generally a performance problem with
proof-segment-up-to.
D Implement proof-find-previous-terminator and bind it to C-c C-a
(45min)
D Implement a function to undo to the previous goal.
D Remove duplication of variables e.g., proof-prog-name and
lego-prog-name for Coq and Lego. (1h)
D Display management is much better than it was, but perhaps
not quite as good as it could be. It might be nice to
display both the goals and response buffer occasionally
(even with window-dedicated disabled).
e.g. when proof-shell-erase-response-flag is non-nil
and the goals buffer is updated: might like to still
see what was in the response buffer.
Oddities:
Response buffer doesn't get cleared after completion
of a proof followed by retraction of whole file.
On other cases of retraction, it does.
Perhaps retraction should set the flag to ensure
it's cleared.
D Fixup display of urgent messages in minibuffer: split at
newlines so we don't get ^J's in FSF Emacs.
D Make wellclean target remove images in html/images which are
generated from the image directory. Consider putting all the
image sources in images/
X Web pages:
- Check appearance in V3 browsers.
- Make front page logo be an image map.
- Reduce text size and front page image, for 1024x768 screens.
- Validate pages.
Current failures for HTML 4.0 to do with CGI-style arguments with "&",
this is a problem with PHP3 really.
- Restructure so that page titles are different to help
browsing. (Move links_arr from header.phtml somewhere new,
and set $pg_title appropriately before head.phtml is included).
- Add pdf documentation as soon as DCS upgrades its ancient
TeX installation, or as soon as making release from elsewhere
works. Also need to fix inclusion of image in pdf.
- Add status bar messages to navigation bar
- Get rid of footer() function.
- Convert to SSI only plus a meta-generation phase?
X Is it possible to let C-c C-c (SIGINT) issue additional process input?
Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or
rather, to fail gracefully.
[ This item reduced to X since Poly/ML is now obsolete. This may
still be useful for future proof assistants, though. ]
X splash screen: report XEmacs problem of not displaying transparent
gif properly.
X Consider filtering out special annotations from shell buffer
rather than merely making them invisible.
X Allow bib-cite style clicking on Load/Import commands to go
to file.
X w3 manages to do toolbar enablers that work. How?
X Images for splash screen: could add xpm files for logos
so that XEmacs displays transparent parts properly.
(Probably not worth effort of distributing more files).
X Customization mechanism: is there a way to make saved settings
not be overwritten by setq's in the code? Need to think how
to do this, something like customize-set-variable-if-unchanged
Otherwise no so useful for people to use customize for
prover config settings (we'd need to shadow them all again for
each assistant for this to work smoothly).
Sure sign saving will fail is when you see "this option has
been changed outside customization buffer"
At the moment even setting config variables in a hook is tricky,
because proof-config-done is called before the hook variables for the
new mode are. Our new version of define-derived-mode needs
to address this.
X Proofs in Isabelle scripts can be non-interactive. Non-interactive
proofs have only one command, effectively. It might be useful
to find a way to integrate these into Proof General nicely.
X 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)
X Span convenience functions for special 'type property.
Could put these in proof.el or somewhere.
(defsubst set-span-type-property (span val)
"Set type property of SPAN to VAL"
(set-span-property span 'type val))
(defsubst span-type-property (span)
"Get type property of SPAN"
(span-property span 'type))
etc. (1hr)
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
leaves stuff around.
X 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)
X Remove .gif, .jpg, .xpm, .xbm files from the CVS repository. Add
.cvsignore's for them instead. Disadvantage: developers will need
to have the Gimp installed to build them via 'make images'
(or copy them from the latest download). (da, 1hr)
X proof-site (da): I think it would be nice to change the architecture
to make customization for new provers much easier.
The standard use of 'define-derived-mode' could be invoked
automatically in proof-site, and we could easily get away from the
kludge of proof-config-done and friends.
(Compare this to the way font-lock works automatically for XEmacs
when the right variable name is set, but for FSF Emacs you have
to write something special).
The objection to doing this is based on the idea that we should use
an object-like inheritance mechanism to define the new modes.
But if this is forgone, it might even be possible to add
support for new assistants entirely via the customize mechanism,
without any knowledge of elisp apart from regular expressions!
X Support a history of proof commands, with a "redo" command to
redo undo-to-point or sequences of toolbar undo's.
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 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 proof-mark-buffer-atomic marks the buffer as only containing
comments if the first ACS is a goal-save span. This is however not a
problem for LEGO and Isabelle. (30 min)
X Idea for future re-engineering:
Indirect Buffers seem to be a cunning way
to implement the response buffer and goals buffer, since they're
basically variants on displaying fragments of the shell buffer
output. Unfortunately seems to be implemented only in FSFmacs at the
moment.
* Things to do for Proof-by-Pointing
====================================
B Change proof by pointing (pbp) stuff into proofstate buffer stuff.
(1h tms)
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 tmd)
(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.
* Things to do for Lego
=======================
C In LEGO, apart from Goal...Save pairs, we have
declaration...discharge pairs. See the section "Granularity of
Atomic Commands" for a proposal on how to generalise the current
implementation so that it can also deal with "Discharge".
[See also the Coq problem with Sections] (6h)
C Inoking an "Expand" command produces a new proof state. But this is
incorrectly displayed in the response buffer and not the goals
buffer because special annotations are missing. Presumably, one
ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)
C fix Pbp implementation (10h)
D Improve legotags. It cannot handle lists e.g., with
[x,y:nat];
it only tags x but not y. [The same problem exists for coqtags]
X Add support for changing directory when scripting buffer changes
(see proof-activate-scripting-hook). This would alleviate users
from some messing with LEGOPATH. (Possibly contentious).
X Mechanism to save object file. Specifically, after having processed
a script (interactively), it would be nice if one could now save the
buffer in object format. At the moment, it only gets converted
(automatically) when it is read in indirectly at a later stage.
However, there is currently no LEGO command to do this. [4h]
* Things to do for Coq
======================
A C-c C-c breaks the coherence with prover state
C Retraction in a Section should retract to the beginning of the whole
section. See the section "Granularity of
Atomic Commands" for a proposal on how to generalise the current
implementation so that it can also deal with sections.
[See also the LEGO problem with Discharge] (6h)
D Add Patrick Loiseleur's commands to search for vernac or ml files.
(they are in a separate file that is part of Coq distrib.
should I really integrate that in PG ? Patrick)
D Proof-by-Pointing (10h)
D Add coq-add-tactic with a tactic name, which adds that tactic to the
undoable tactics and to the font-lock. (2h)
D Improve coqtags. It cannot handle lists e.g., with
Parameter x,y:nat
it only tags x but not y. [The same problem exists for legotags]
* Things to do for Isabelle
===========================
A Multiple files needs careful testing. There are cases when
retracting asks for files to be removed which were never loaded.
This might be harmless, but might be better cleaned up.
B auto-adjust Pretty.setmargin when window is resized
C Unify display of proof output for final level "No subgoals"
case with other levels (i.e. remove spurious newlines).
NB: spurious newlines may be liked by other provers.
C derive an isa-response-mode from proof-response-mode;
see lego.el (10min)
D Implement completion for Isabelle using tables generated by
the running process. Would be a nice addition. (4 hours)
D Add useful specific commands for Isabelle. Many could
be added. Would be better to merge in Isamode's menus.
(however, probably two week's work to bring together Isamode
and proof.el, making some of Isamode generic)
D Switching to other file with C-c C-o could be more savy
with file names and extensions (use some standard function?)
X 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 Write perl scripts to generate TAGS file for ML and thy files.
(6h, I've completely forgotten perl). Does anyone
actually want this?
X Manage multiple proofs (markers in possibly different buffers)
* FSF Emacs issues
==================
A bug: FSF Emacs problem (showstopper): highlighting of locked region
and queue region seems faulty nowadays for me (da).
Only tested on Linux.
Going back to 2.0 does not fix problem, on 20.2 or 20.3
C `proof-zap-commas-region' does not work for Emacs 20.2 on
lego/example.l . On *initially* fontifying the buffer,
commas are not zapped. However, when entering text, commata are
zapped correctly. (2h)
C proof-shell-dont-show-annotations doesn't seem to work.
X possible bug: Thomas had a bizarre .emacs file which causes
Seg Faults with Proof General and FSF Emacs. Doesn't happen
with "emacs -q". Investigate which package/setting he adds is to blame.
* Bugs in other packages beyond our control
===========================================
. Odd behaviour of font-lock in elisp buffers when long strings
contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)"
. oddity: startup delay when running XEmacs remotely and local display
is 8 bit. Suspect an XEmacs issue to do with face allocations.
Also huge delay in buffers for Isabelle mode which try to highlight
binders (removed because they appear inside strings anyway)
* New Stable Version Release checklist
======================================
0. Make all files have same CVS branch with cvs commit -f
(only seems to work locally, not via cvs server).
Innessential convention. Could increment head number.
1. Test multiple file test suite for LEGO, Isabelle. Coq example.
2. Check case with FSF Emacs
3. Check case with compiled code, for XEmacs only.
(Wait for error reports for FSF Emacs)
4. Dates and versions updated in:
README, doc/ProofGeneral.texi, html/download.html
5. ProofGeneral.texi docstring magic is up-to-date:
cd doc; make magic
6. Update Emacs and prover versions in texi, html/
7. Check web page references from other places.
8. Validate web pages if they're changed much.
* Things to do for Proof General Project
========================================
A Try to get small project grant from LFCS to help with
development of Proof General
A Find new person to help maintain Coq Proof General
A Polish ProofGeneral.texi and publish LaTeX as an LFCS
Technical Report.
* Fix page rearrangement to insert a blank page
* Fix typos/other stuff found by Dave.
* Suggestions, typos, contributions by Healf.
(Dave has email)
* Improve trivial and uniformative docstrings.
* Fixup markup mistakes by editing docstrings.
* Update menus in texi
[6 hours]
A Write paper for system demonstration of Proof General
for some conference. Write paper on design and
development of Proof General.
|