blob: 858ed98bbcd5509b565a48d4880018e518e21320 (
plain)
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
|
Thu Jan 21 14:27:36 GMT 1999 da
Quick test for pipe communication with emacs 20.3.
Used C-c C-n and C-c C-u on example.ML file in
Isabelle successfully.
(Tested 990115 prerelease with piped communication
patch in XEmacs already, for LEGO and Isabelle).
Wed Dec 16 15:45:53 GMT 1998 da
Quick test of Coq mode.
xemacs -q -l ProofGeneral/generic/proof-site.el
(setq proof-rsh-command "ssh hope")
Assertion and retraction commands work as far as I can
tell. Using toolbar on file coq/example.v
Wed Dec 16 12:25:00 GMT 1998 tms
Clarification of entry "Mon Dec 14 15:02:52 GMT 1998 da"
The problem with LEGOVERSION "alpha" can also be reproduced with
lego 1.3.1 (and XEmacs 20.4 or FSF Emacs 20.2) and the file
lego/example2.l which accesses a module in a non-writable directory.
You need to set chmod u-w readonly yourself; CVS doesn't like
non-writable directories)
It is a LEGO specific problem. LEGO forgets about annotations
sometimes. This has been reported to lego@dcs.ed.ac.uk .
Wed Dec 16 12:25:00 GMT 1998 tms
On scar, tested Emacs 20.2.1 with lego 1.3.1 via "ssh craro",
LEGOVERSION "std"
emacs-20.2 -eval '(progn (load
"/home/tms/emacs/ProofGeneral/generic/proof-site.el")(setq
proof-rsh-command "ssh craro"))' lego/example.l
Pressing C-c C-n crashes Emacs: Fatal error (11).Segmentation fault
This must be a problem with my .emacs file. Including -q in the
options, everyting seems to work just fine. Still, this is somewhat
concerning.
Mon Dec 14 15:02:52 GMT 1998 da
Tested Emacs 20.2.1 with lego 1.3 via "ssh hope",
with lego 1.3.1 via "ssh craro", LEGOVERSION "std"
Both successfully process example.l
With lego 1.3.1 via "ssh craro", LEGOVERSION "alpha",
processing gets stuck, never reports "imports done".
Is this a bug or problem with LEGO installation?
Bugs:
Killing off process shell via proof-shell-exit.
Killing proof script buffer gives error.
|
