[Gcl-devel] apparent GCL 2.5.0 bug on Redhat 7.3

[Matt Kaufmann]

Hi --

I just ran across an apparent GCL 2.5.0 bug on Redhat 7.3.  I performed
essentially the same action on a Debian Gnu Linux platform (GCL 2.5.0) as well
as many others (including Solaris GCL 2.3.8 and many other Lisps) without
running into this problem.  The relevant part of the log is as follows.

  [SGC for 94 STRING pages..(5707 writable)..(T=24).GC finished]
  Loading 
/home/kaufmann/apps/acl2/acl2-sources/books/data-structures/structures.o
  [SGC for 0 CONTIGUOUS-BLOCKS pages..(5722 writable)..(T=25).GC finished]
  [SGC off][GC for 500 RELOCATABLE-BLOCKS pages..(T=50).GC finished]
  [SGC on]
  Error: Cannot get relocated section contents

  Fast links are on: do (si::use-fast-links nil) for debugging
  Error signalled by INCLUDE-BOOK-FN.
  Broken at COND.  Type :H for Help.
  ACL2>>

Here is how you can re-create this bug (at least, on Redhat 7.3; at least on
*my* laptop).  First download
ftp://ftp.cs.utexas.edu:/pub/moore/acl2/v2-7/acl2.tar.gz.  Then (where you can
replace "gcl" below with a path to your GCL):

  gunzip acl2.tar.gz
  tar xvf acl2.tar
  cd acl2-sources
  make LISP=gcl
  make certify-books

The error will appear in books/misc/mult.out.  It will take a little while
(about 15 min. on my 850 MH Duron laptop) to get to the problem after make
certify-books is started.  The above mult.out file is the result of ACL2's
processing ("certification") of file mult.lisp; none of the other several dozen
such certifications completed so far have caused an error in the above make
certify-books.

By the way, the above acl2.tar.gz may not be our final release of ACL2 Version
2.7, though it's close.  So please do not redistribute it, but feel free to use
it in your testing.  In fact, we plan to finalize the release next Wednesday
(11/13), so if you find any issues before then, we'd be very interested!

Thanks --
-- Matt