aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/testing-log.txt
blob: 324284d49d215ec834f0da671a8004d6bf269bf6 (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
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
Fri Mar 24 15:40:10 GMT 2000 da

 Tested Proof General on win32 (NT4sp6) with Isabelle, Coq and
 XEmacs 21.1.9.

 Problems:  Isabelle bombs on paths containing chars like \ : $
            XEmacs barfs on reading some files in PG, why??
	    e.g. coq/coq.el 

	 Can fix this by reloading coq stuff again.

	 A few probs remain, e.g. toolbar enablers for undo are
	 flaky.
	

Wed Mar 22 13:45:34 GMT 2000 da 

 Tested file name quoting problem with Coq, Isabelle, LEGO.
  
   \ quoting triggers bug in Isabelle (complaint about pathname)
   " quoting not allowed in LEGO, \ quoting not needed.
   Coq works well with either.
   
	

--------
	
Wed Nov 17 13:43:11 GMT 1999

 Tested compiled version.  Seems to work well for XEmacs!
 Also for FSF Emacs!  So long as using their own elc's.

Tue Nov 16 15:28:51 GMT 1999

 Tested automatic multiple file handling: see etc/demoisa

 Tested FSF Emacs, after fixing several things.

 Tested proof by pointing in LEGO.  Fixes for bugs,
 empty pbp response, and added a useful click
 (C-button 3) for undoing and deleting the last 
 pbp command.  Can now prove example.l by PBP.
 Proof-by-pointing lives!

Thu Nov 11 19:05:39 GMT 1999

 Tested response buffer display: see isa/message-test.ML
 Made output more regular by removing spurious space/newline 
 after every prompt, and padding response buffer with 
 newlines when messages aren't newline terminated.

 Testing window management for multiple frames.  Could find no
 evidence of old bug message in code about with
 special-display-regexps, script buffer gets made into
 dedicated buffer.  Removed the comment.

Mon Aug 23 19:00:26 BST 1999 da

  Summary of tests today:

  Proof General 2.0:  sanity check.
    Okay with XEmacs 20.4, lego 1.3.1 and Isabelle 98p1.
    Strange overlay disappearing problem with FSF Emacs 20.2,
    so must be X Server or architecture anomaly that causes
    different display order.

  Today's Proof General.

    1. With Isabelle 98p1, no go.
    2. Same show-stopper as above with Emacs 20.2 and 20.3.  
       Argh!  I'm really fed up of FSF Emacs, it goes wrong
       even when "nothing" has changed.
    3. With current Isabelle (or, at least, 99pre180899).
    4. Using x-symbol.  No success, and a big mess (rebinds M-x !!?)

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.