diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-16 14:35:47 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-16 14:35:47 +0000 |
| commit | 258294f034ddf00d19a6225c090e78329da69f23 (patch) | |
| tree | 1c92d0b409e4812128d773b4a2536ecf58e2032a | |
| parent | b6233745cb6a55f03a9d2194a0617798796ea86d (diff) | |
documented LEGO specific bug
| -rw-r--r-- | BUGS | 5 | ||||
| -rw-r--r-- | etc/testing-log.txt | 27 | ||||
| -rw-r--r-- | lego/example2.l | 1 |
3 files changed, 31 insertions, 2 deletions
@@ -67,6 +67,11 @@ FSF Emacs specific bugs LEGO Proof General Bugs ======================= +* If LEGO attempts to write a (object) file in a non-writable + directory, it forgets the protocol mechanism on how to interact with + Proof General and gets stuck. Workaround: directly enter "Configure + AnnotateOn" in the Proof Shell to recover. + * After a `Discharge', retraction ought to only be possible back to the first declaration/definition which is discharged. However, LEGO Proof General does not know that Discharge has such a non-local effect. diff --git a/etc/testing-log.txt b/etc/testing-log.txt index ccd65ec3..6f6307ca 100644 --- a/etc/testing-log.txt +++ b/etc/testing-log.txt @@ -14,7 +14,30 @@ Mon Dec 14 15:02:52 GMT 1998 da Killing proof script buffer gives error. - - +Mon 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 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 .
\ No newline at end of file diff --git a/lego/example2.l b/lego/example2.l new file mode 100644 index 00000000..37d1e563 --- /dev/null +++ b/lego/example2.l @@ -0,0 +1 @@ +Module example2 Import "readonly/readonly";
\ No newline at end of file |