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
|
-*- 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 Write function proof-retract-file. (hhg? 30min)
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 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 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)
* 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)
B Replace running-(xemacs|emacs19) in proof.el by fboundp. (20min tms)
A Replace recursion with while-loop in span-overlay. (2h hhg)
|
