This is how to reproduce a problem building PVS with SBCL on an ARM platform.
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:
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):
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.
I wondered if the problem was lack of resources, so I added this to the build, with no change in the result:
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.