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
|
Some test cases for Proof General.
==================================
See testing-log.txt for log of tests conducted.
Please add to that file!
22.3.00 FILENAME ESCAPES PROBLEM [All provers, probably]
========================================================
Filename substitution %s in settings including proof-shell-cd-cmd,
proof-shell-inform-file-{retracted,processed}-cmd, may need
to add escape characters peculiar to the proof assistant syntax.
Test cases:
ln -s ProofGeneral \\backslash
ln -s ProofGeneral \"quote
Then try scripting with example files for each prover,
i.e. \"quote/coq/example.v, etc.
1.2.99 FILE RECOGNITION PROBLEM [Isabelle]
===========================================
Bug in regexp caused ML files to be recognized as
theory files when "thy" appeared in path.
Test case in etc/isa/thy/test.ML.
15.1.99 LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS
===================================================
Test that etc/isa/long-line-backslash.ML can be processed
successfully.
16.12.98 KILLING THE PROOF PROCESS
==================================
Process some proof script buffer. Invoke
M-x proof-shell-exit
Process should exit cleanly.
11.12.98 RUDELY KILLING THE ACTIVE SCRIPTING BUFFER
====================================================
Start scripting with some buffer, after
having processed another buffer.
Kill it when scripting is only partly finished.
Scripting should be cleanly turned off and it
should be possible to resume retraction in the
first buffer.
Moreover, this ensures that if the file is on the included
files list, yet has been only partly processed (e.g. because
Undo steps were taken), then it will be retracted and
removed from the included files list.
FIXME: Using C-x C-v to revert to saved version doesn't
seem to work because it renames the buffer or something.
8.12.98 INHIBIT VARIABLES
==========================
Test with proof-splash-inhibit=t
Test with proof-toolbar-inhibit=t
8.12.98 SCRIPTING FOR BUFFERS WITHOUT FILES.
=============================================
Switch to a fresh buffer FOO which doesn't visit a file.
Do M-x isa-mode RET.
Should succeed.
Try asserting commands, e.g. Goal "P-->P";
Switch to another fresh buffer BAR, turn on isa-mode.
Should succeed again.
Try asserting commands here, e.g. Goal "Q&Q --> Q";
Should give error "Cannot have more than one active scripting buffer".
Exit emacs. Should query whether we want to save these
scripting buffers (maybe XEmacs only).
|
