SBCL + PVS on ARM

This is how to reproduce a problem building PVS with SBCL on an ARM platform.

Build Machine

I do not have access to ARM hardware, so I am building with QEMU 1.6.2 on an x86_64 host that is running Fedora 20. The emulated ARM platform has the following characteristics:

Build Environment

The virtual ARM machine is also running Fedora 20. Since SBCL for ARM is only available in Fedora Rawhide (to be released as Fedora 21 sometime in fall of 2014), I am doing the actual building in a chroot, using mock. The chroot environment has the following software installed (list pared down to what seems interesting):

Build Setup

SRI has never provided a source tarball for PVS 6.0. Also, some patches that have subsequently been applied to the PVS git repository are necessary for a successful build with SBCL. Therefore, we get to use this somewhat convoluted technique to acquire the sources to build.

  1. git clone https://github.com/samowre/PVS.git pvs-6.0
  2. cd pvs-6.0
  3. git reset --hard 42a7aae6c6d477dd2c25b846757274176092b08d
  4. patch -p1 < pvs.patch
  5. If using an installed SBCL, instead of a run-in-place, you may also need to change run-sbcl.sh to sbcl in Makefile.in.
  6. autoreconf -i
  7. export LANG=en_US.UTF-8
    (That I specified US English is irrelevant; the important part is the UTF-8. Feel free to specify a different language part.)
  8. CFLAGS="-O2 -g -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -fexceptions -grecord-gcc-switches" LDFLAGS="-Wl,-z,relro" ./configure
    (You may also wish to specify a --prefix option, but that is not important.)
  9. make SBCLISP_HOME=/usr/bin

Ulimit Notes

I wondered if the problem was lack of resources, so I added this to the build, with no change in the result:

Build Failure

The build failure manifests as follows:

Typechecking union
 Datatype union may be empty

fatal error encountered in SBCL pid 5235:
maximum interrupt nesting depth (1024) exceeded


Welcome to LDB, a low-level debugger for the Lisp runtime environment.
ldb>

See this message for more information.


Last modified: Wed Jul 9 10:33:35 MDT 2014 by Jerry James