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))))