[Gcl-devel] still a problem with interrupts in 64-bit GCL

[Matt Kaufmann]

Hi --

I really appreciate the work you've done (Camm and Dave), but
unfortunately we seem to be back where we started.  I've included my
email with the original issue below, so that you can re-create the
problem.  (I've redone the steps listed below, in the locations
specified.)

By the way, I'm still not seeing the problem with 32-bit GCL; just
64-bit.

Thanks --
-- Matt
   Date: 20 Feb 2009 08:23:17 -0600
   From: Matt Kaufmann <address@hidden>
   CC: address@hidden, gripe

   Hi --

   The sysadmins here at UT CS have built GCL 2.6.8pre from CVS as you
   suggested.  It's working great on 32-bit linux, but I've run into an
   issue for 64-bit linux.

   You can re-create the issue on a UT CS 64-bit linux machine as
   follows.

   Start up ACL2 built on GCL, as follows:

   /projects/acl2/v3-4-linux/fast-linux-gcl-saved_acl2

   Then issue these commands:

     ; Just to slow down the output from the next form:
     (trace$ rewrite)

     ; ACL2 disables the debugger by default; this restores it:
     (set-debugger-enable t)

     ; This goes pretty fast but you'll have time to interrupt it:
     (thm (equal (append (append x x) x) (append x x x)))

     [Now quickly interrupt with control-c, and then :q from the break.
      If the form above completes, just try it again.  Eventually I think
      you'll see a Lisp "fatal error" or even a "Segmentation fault".]

   By the way, I built /projects/acl2/v3-4-linux/fast-linux-gcl as
   follows, on lhug-0 (a 64-bit linux machine):

   rm -f TAGS ; mv make-fast-gcl.log make-fast-gcl.old.log ; (time nice make 
PREFIX=fast-linux-gcl- LISP=my-fast-gcl) >& make-fast-gcl.log&

   where "my-fast-gcl" is a script containing:

   #!/bin/sh
   /lusr/opt/gcl-2.6.8pre/bin/gcl -eval "(defparameter 
user::*fast-acl2-gcl-build* t)" $*

   Also by the way, if you instead run the following on a 32-bit UT CS
   linux machine

   /projects/acl2/v3-4-linux/gcl-saved_acl2

   then you won't see the interrupt problem described above (or at least,
   I didn't, and I tried).

   Thanks --
   -- Matt