GCL Tips (for ACL2 Version 2.9 News)

Table of Contents:

Installing ACL2 on top of GCL 2.6.5 in an X86 running Fedora Core 3

Thanks to Sandip Ray for supplying the following instructions. 

[Note: Thanks to Camm Maguire for providing detailed instructions and help in the process.]

1. Download the gcl-2.6.5 sources, and unzip and untar them to some
    directory gcldir.

2. Append the following code to gcldir/h/386-linux.h:

#ifdef IN_SFASL 
#include <sys/mman.h> 
#define CLEAR_CACHE {\
    void *p,*pe; \
    p=(void *)((unsigned long)memory->cfd.cfd_start & ~(PAGESIZE-1)); \
    pe=(void *)((unsigned long)(memory->cfd.cfd_start+memory->cfd.cfd_size) & ~(PAGESIZE-1)) + PAGESIZE-1; \
    if (mprotect(p,pe-p,PROT_READ|PROT_WRITE|PROT_EXEC)) {\
      fprintf(stderr,"%p %p\n",p,pe);\
      perror("");\
      FEerror("Cannot mprotect", 0);\
    }\ 
} 
#endif

  Note:

  The above code is required since FC3 have made brk() pages
  non-executable by default. If you do not apply the patch above you will be able
  to compile gcl but when you then go onto compiling ACL2 you will probably see
  an error like "Memory may be damaged."

3. Now compile gcl with the following commands:

   cd gcldir
   ./configure --disable-statsysbfd --enable-locbfd
   make
   make install

  Notes:

  (i) The options to configure are required since binutils have changed on FC3
      since the release of gcl. Thus gcl probably would not compile otherwise.

  (ii) "make install" is not necessary but otherwise you must give the entire
       pathname for the gcl executable while compiling ACL2 (step 4).


4. Now follow the directions for "Building an Executable Image on a Unix or
    Linux System" from the ACL2 home page.

Building on GCL 2.6.0 and earlier

We have learned that the build process for ACL2 2.9 is broken for GCL 2.6.0 (and perhaps some earlier versions of GCL). Thanks to Jose Luis Ruiz-Reyna for bringing this problem to our attention and for testing the fix, which is to replace the definition of function gcl-version->, in ACL2 source file acl2-init.lisp, with the definition shown below.

We recommend that instead of applying the fix, simply download GCL 2.6.5 from http://ftp.gnu.org/gnu/gcl/ and build ACL2 Version 2.9 on this GCL, for which the fix is not necessary. The ACL2 regression suite has consistently run about 30% faster with ACL2 built on this version of GCL than with ACL2 built on GCL 2.6.1.

However, in case you have a version of GCL preceding 2.6.1 and prefer not to replace it, here is the patch promised above. 

(defun gcl-version-> (major minor extra)

; When true, this guarantees that the current GCL version is greater than
; major.minor.extra.  The converse holds for versions of GCL past perhaps 2.0.

  (and (boundp 'si::*gcl-major-version*)
       (integerp si::*gcl-major-version*)
       (if (= si::*gcl-major-version* major)
           (and (boundp 'si::*gcl-minor-version*)
                (integerp si::*gcl-minor-version*)
                (if (= si::*gcl-minor-version* minor)
                    (and (boundp 'si::*gcl-extra-version*)
                         (integerp si::*gcl-extra-version*)
                         (> si::*gcl-extra-version* extra))
                  (> si::*gcl-minor-version* minor)))
         (> si::*gcl-major-version* major))))

Possible GCL/Windows Issue

Note 1: This issue has only arisen when building GCL from scratch. So you may want to fetch a binary GCL/Windows distribution and then ignore this issue.

Note 2: The issue discussed below has already been dealt with in Jared Davis's Windows installer for ACL2 built on GCL, which you can download.

We have seen hard lisp errors in events with case-match, for ACL2 built on GCL Version 2.6.5, built on Windows. The errors might not occur if you build ACL2 on a GCL Windows binary downloaded from http://ftp.gnu.org/gnu/gcl/binaries/stable/. If you do get such a hard a lisp error, a workaround is to download the following files and put them in the directory with your ACL2 image (presumably the ACL2 source directory).

  • gazonk520.o
  • windows_saved_acl2
    • The file windows_saved_acl2 (which you are welcome to rename) will be your ACL2 executable. Open it in an editor and edit pathnames as indicated in the comment in that file.

    Optionally, instead of downloading gazonk520.o, you can download gazonk520.lsp and compile it yourself to create gazonk520.o.