[pvs-sbcl] Fix building on non-Intel architectures.
Jerry James
jjames at fedoraproject.org
Tue Dec 6 17:49:12 UTC 2011
commit 9cadf5d2ebaefb9f7d96e3af01a9dd9d274fe66c
Author: Jerry James <loganjerry at gmail.com>
Date: Tue Dec 6 10:48:48 2011 -0700
Fix building on non-Intel architectures.
pvs-fedora.patch | 373 ++++++++++++++++++++++++++++--------------------------
pvs-sbcl.spec | 5 +-
2 files changed, 199 insertions(+), 179 deletions(-)
---
diff --git a/pvs-fedora.patch b/pvs-fedora.patch
index dd3f226..6f2dae5 100644
--- a/pvs-fedora.patch
+++ b/pvs-fedora.patch
@@ -1,18 +1,70 @@
---- ./src/WS1S/ws1s_table.c.orig 2010-12-18 00:07:32.000000000 -0700
-+++ ./src/WS1S/ws1s_table.c 2011-04-16 15:20:06.104545718 -0600
-@@ -182,8 +182,8 @@
- int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
-
-
--extern int mona_bdd_size (int);
--int (*ws1s___bdd_size)(int) = mona_bdd_size;
-+extern int bdd_size (int);
-+int (*ws1s___bdd_size)(int) = bdd_size;
-
+--- ./bin/pvs-platform.orig 2011-04-15 11:45:09.000000000 -0600
++++ ./bin/pvs-platform 2011-12-06 10:39:21.003660835 -0700
+@@ -33,11 +33,8 @@ case `uname -s` in
+ esac
+ os=SunOS
+ os_version=`uname -r | cut -d"." -f1`;;
+- Linux|FreeBSD) case `uname -m` in
+- x86_64) arch=ix86_64;;
+- *86*) arch=ix86;;
+- esac
+- os=Linux;;
++ Linux|FreeBSD) arch=linux
++ os=Linux;;
+ AIX) arch=powerpc-ibm
+ os=AIX
+ os_version=`uname -r`;;
+--- ./src/utils/linux/Makefile.orig 2011-12-06 10:39:20.993660845 -0700
++++ ./src/utils/linux/Makefile 2011-12-06 10:39:20.993660845 -0700
+@@ -0,0 +1,22 @@
++LDFLAGS = -shared -L./
++CC=gcc
++CFLAGS=
++SFLAGS=-fPIC -fno-strict-aliasing
++VPATH=..
++
++obj=file_utils.o
++
++.SUFFIXES:
++.SUFFIXES: .c .o
++.c.o : ; $(CC) $(XCFLAGS) $(SFLAGS) $(CFLAGS) -c $< -o $@
++
++all : file_utils.so b64
++
++file_utils.so: ${obj}
++ $(CC) $(CFLAGS) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj}
++
++b64: ../b64.c
++ $(CC) $(XCFLAGS) $(CFLAGS) -o ./b64 ../b64.c
++
++clean :
++ rm -f *.o *.a *.so b64
+--- ./src/classes-expr.lisp.orig 2011-04-15 11:45:05.000000000 -0600
++++ ./src/classes-expr.lisp 2011-12-06 10:39:20.992660846 -0700
+@@ -36,6 +36,10 @@
- extern int dfaSetup (int);
---- ./src/WS1S/linux/Makefile.orig 2011-04-16 13:51:18.431676758 -0600
-+++ ./src/WS1S/linux/Makefile 2011-04-16 13:51:18.432676644 -0600
+ ;; SBCL changed things so this no longer works - pvs.system
+ ;; simply unlocks the :common-lisp package
++#+sbcl
++(eval-when (:execute :compile-toplevel :load-toplevel)
++ (sb-ext:unlock-package :common-lisp))
++
+ #+cmu
+ (ext:without-package-locks
+ (defgeneric type (x))
+--- ./src/WS1S/ws1s-ld-table.orig 2011-04-15 11:45:04.000000000 -0600
++++ ./src/WS1S/ws1s-ld-table 2011-12-06 10:39:20.992660846 -0700
+@@ -46,7 +46,7 @@ ws1s___dfaPrintVitals = dfaPrintVitals ;
+ ws1s___dfaPrint = dfaPrint ;
+ ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
+ ws1s___dfaPrintVerbose = dfaPrintVerbose ;
+-ws1s___bdd_size = mona_bdd_size ;
++ws1s___bdd_size = bdd_size ;
+ ws1s___dfaSetup = dfaSetup ;
+ ws1s___dfaAllocExceptions = dfaAllocExceptions ;
+ ws1s___dfaStoreException = dfaStoreException ;
+--- ./src/WS1S/linux/Makefile.orig 2011-12-06 10:39:20.991660847 -0700
++++ ./src/WS1S/linux/Makefile 2011-12-06 10:39:20.991660847 -0700
@@ -0,0 +1,55 @@
+ifneq (,)
+This makefile requires GNU Make.
@@ -69,153 +121,22 @@
+
+clean :
+ rm -f *.o *.a *.so
---- ./src/WS1S/ws1s-ld-table.orig 2010-12-18 00:07:32.000000000 -0700
-+++ ./src/WS1S/ws1s-ld-table 2011-04-16 15:19:40.142543771 -0600
-@@ -46,7 +46,7 @@
- ws1s___dfaPrint = dfaPrint ;
- ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
- ws1s___dfaPrintVerbose = dfaPrintVerbose ;
--ws1s___bdd_size = mona_bdd_size ;
-+ws1s___bdd_size = bdd_size ;
- ws1s___dfaSetup = dfaSetup ;
- ws1s___dfaAllocExceptions = dfaAllocExceptions ;
- ws1s___dfaStoreException = dfaStoreException ;
---- ./src/classes-expr.lisp.orig 2011-04-05 00:26:24.000000000 -0600
-+++ ./src/classes-expr.lisp 2011-04-16 16:06:46.211939608 -0600
-@@ -36,6 +36,10 @@
-
- ;; SBCL changed things so this no longer works - pvs.system
- ;; simply unlocks the :common-lisp package
-+#+sbcl
-+(eval-when (:execute :compile-toplevel :load-toplevel)
-+ (sb-ext:unlock-package :common-lisp))
-+
- #+cmu
- (ext:without-package-locks
- (defgeneric type (x))
---- ./src/utils/linux/Makefile.orig 2011-04-16 13:51:18.432676644 -0600
-+++ ./src/utils/linux/Makefile 2011-04-16 13:51:18.432676644 -0600
-@@ -0,0 +1,22 @@
-+LDFLAGS = -shared -L./
-+CC=gcc
-+CFLAGS=
-+SFLAGS=-fPIC -fno-strict-aliasing
-+VPATH=..
-+
-+obj=file_utils.o
-+
-+.SUFFIXES:
-+.SUFFIXES: .c .o
-+.c.o : ; $(CC) $(XCFLAGS) $(SFLAGS) $(CFLAGS) -c $< -o $@
-+
-+all : file_utils.so b64
-+
-+file_utils.so: ${obj}
-+ $(CC) $(CFLAGS) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj}
-+
-+b64: ../b64.c
-+ $(CC) $(XCFLAGS) $(CFLAGS) -o ./b64 ../b64.c
-+
-+clean :
-+ rm -f *.o *.a *.so b64
---- ./BDD/linux/Makefile.orig 2011-04-16 13:51:18.432676644 -0600
-+++ ./BDD/linux/Makefile 2011-04-16 13:51:18.432676644 -0600
-@@ -0,0 +1,47 @@
-+BDD = ../bdd/src
-+MU = ../mu/src
-+UTILS = ../bdd/utils
-+INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
-+LDFLAGS = -shared -L./
-+CC = gcc
-+CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -fno-strict-aliasing
-+XCFLAGS = -O
-+SHELL = /bin/sh
-+VPATH = ..:../bdd/utils:../bdd/src:../mu/src
-+
-+muobj = bdd_interface.o bdd.o bdd_factor.o bdd_quant.o bdd_fns.o bdd_vfns.o \
-+ appl.o mu_interface.o mu.o
-+
-+utilobj = double.o list.o hash.o alloc.o
-+
-+.SUFFIXES:
-+.SUFFIXES: .c .o
-+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
-+
-+all : mu.so
-+
-+mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table
-+ $(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm
-+
-+libutils.a : ${utilobj}
-+ ar r libutils.a ${utilobj}
-+ ranlib libutils.a
-+
-+bdd_interface.o : bdd_interface.c bdd_fns.h
-+bdd_factor.o : bdd_factor.c bdd_factor.h
-+bdd.o : bdd.c bdd.h bdd_extern.h
-+bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h
-+bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h
-+bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h
-+
-+mu_interface.o : mu_interface.c mu.h
-+mu.o : mu.c mu.h
-+
-+double.o : double.c double.h
-+list.o : list.c list.h alloc.h
-+hash.o : hash.c hash.h alloc.h
-+alloc.o : alloc.c
-+
-+clean :
-+ rm -f *.o *.a *.so
-+
---- ./pvs.in.orig 2011-04-04 03:21:58.000000000 -0600
-+++ ./pvs.in 2011-04-16 14:23:51.123179054 -0600
-@@ -266,7 +266,7 @@
- *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1
- esac
+--- ./src/WS1S/ws1s_table.c.orig 2011-04-15 11:45:04.000000000 -0600
++++ ./src/WS1S/ws1s_table.c 2011-12-06 10:39:20.991660847 -0700
+@@ -182,8 +182,8 @@ extern int dfaPrintVerbose (int);
+ int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
--binpath=$PVSPATH/bin/$PVSARCH-$opsys${majvers}
-+binpath=$PVSPATH/bin/linux
- # Check if this is a 64-bit platform, but only 32-bit available
- if [ "$PVSARCH" = "ix86_64" -a ! -x "$binpath" ]
- then binpath=$PVSPATH/bin/ix86-$opsys${majvers}
-@@ -349,6 +349,7 @@
- fi
- PVSVERBOSE=${PVSVERBOSE:-0}
-+PVSIMAGE="/usr/bin/sbcl --core $pvsimagepath"
+-extern int mona_bdd_size (int);
+-int (*ws1s___bdd_size)(int) = mona_bdd_size;
++extern int bdd_size (int);
++int (*ws1s___bdd_size)(int) = bdd_size;
- export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
- export PVSARCH PVSIMAGE PVSPATH PATH PVSLISP PVSVERBOSE PVSTIMEOUT
-@@ -414,13 +415,13 @@
- then
- # Make sure there are no spaces in the eval form - otherwise it goes
- # through the pvs-cmulisp script and gets mangled.
-- echo `$pvsimagepath $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"`
-+ echo `$PVSIMAGE $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"`
- elif [ $rawmode ]
- then
- if [ -n "$emacsargs" ]
- then echo "Emacs flags '$emacsargs' will be ignored in raw mode"
- fi
-- $pvsimagepath $noinit $flags
-+ $PVSIMAGE $noinit $flags
- elif [ $batch ]
- then
- "$PVSEMACS" $batch $dotemacs $pvsemacsinit $flags 2>&1
---- ./doc/user-guide/user-guide.tex.orig 2010-12-18 00:07:48.000000000 -0700
-+++ ./doc/user-guide/user-guide.tex 2011-04-16 16:59:48.714007926 -0600
-@@ -20,6 +20,7 @@
- \else
- \usepackage[bookmarks=true,hyperindex=true]{hyperref}
- \fi
-+\usepackage{amssymb}
- \topmargin -10pt
- \textheight 8.5in
---- ./Makefile.in.orig 2011-02-14 04:19:19.000000000 -0700
-+++ ./Makefile.in 2011-04-16 13:53:25.550057201 -0600
-@@ -66,7 +66,7 @@
+ extern int dfaSetup (int);
+--- ./Makefile.in.orig 2011-04-15 11:45:09.000000000 -0600
++++ ./Makefile.in 2011-12-06 10:39:21.003660835 -0700
+@@ -66,7 +66,7 @@ endif
PLATFORM := $(shell $(PVSPATH)bin/pvs-platform)
export PLATFORM
@@ -224,7 +145,7 @@
SYSTEM ?= pvs
-@@ -94,7 +94,7 @@
+@@ -94,7 +94,7 @@ endif
ifneq ($(SBCLISP_HOME),)
# Check that the given SBCLISP_HOME works
@@ -233,7 +154,7 @@
ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
SBCLVERSION = $(shell $(SBCLISPEXE) --version)
# $(warning "$(SBCLVERSION)")
-@@ -190,10 +190,10 @@
+@@ -190,10 +190,10 @@ emacs-elc = $(filter-out %ilfsf18.elc %i
%illuc19.elc %ilxemacs.elc %ilisp-menu.elc,\
$(emacs-sub-src:.el=.elc))
@@ -248,7 +169,7 @@
ess = ess/dist-ess.lisp \
ess/init-load.lisp \
-@@ -502,12 +502,12 @@
+@@ -502,12 +502,12 @@ $(PVSPATH)TAGS : $(lisp-files) $(allegro
$(ETAGS) $(lisp-files) $(allegrolisp) $(sbcllisp) $(cmulisp) $(pvs-emacs-src)
fileutils = \
@@ -265,7 +186,7 @@
image-deps = $(fileutils) $(bddlib) $(ws1slib) $(pvs-make-files) \
$(ess) $(ff-files) $(lisp-files) \
-@@ -544,7 +544,7 @@
+@@ -544,7 +544,7 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
--eval "(let ((*load-pvs-prelude* nil)) \
(mk:operate-on-system :pvs :compile))" \
--eval '(quit)'
@@ -274,7 +195,7 @@
@echo "******* Building PVS image $@"
$(SBCLISPEXE) --eval '(require :sb-posix)' \
--eval '(require :sb-md5)' \
-@@ -552,15 +552,14 @@
+@@ -552,15 +552,14 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
--eval "(unwind-protect \
(mk:operate-on-system :pvs :compile) \
(save-lisp-and-die \"$@\" \
@@ -295,7 +216,7 @@
endif
ifneq ($(CMULISP_HOME),)
-@@ -635,12 +634,12 @@
+@@ -635,12 +634,12 @@ endif
clean distclean tar
$(fileutils) makefileutils :
@@ -311,19 +232,115 @@
make-release-notes :
$(MAKE) -C $(PVSPATH)doc/release-notes
---- ./bin/pvs-platform.orig 2011-01-28 03:52:57.000000000 -0700
-+++ ./bin/pvs-platform 2011-04-16 13:53:46.854607161 -0600
-@@ -33,11 +33,8 @@
+--- ./BDD/linux/Makefile.orig 2011-12-06 10:39:20.993660845 -0700
++++ ./BDD/linux/Makefile 2011-12-06 10:39:20.993660845 -0700
+@@ -0,0 +1,47 @@
++BDD = ../bdd/src
++MU = ../mu/src
++UTILS = ../bdd/utils
++INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
++LDFLAGS = -shared -L./
++CC = gcc
++CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -fno-strict-aliasing
++XCFLAGS = -O
++SHELL = /bin/sh
++VPATH = ..:../bdd/utils:../bdd/src:../mu/src
++
++muobj = bdd_interface.o bdd.o bdd_factor.o bdd_quant.o bdd_fns.o bdd_vfns.o \
++ appl.o mu_interface.o mu.o
++
++utilobj = double.o list.o hash.o alloc.o
++
++.SUFFIXES:
++.SUFFIXES: .c .o
++.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
++
++all : mu.so
++
++mu.so : ${muobj} libutils.a ../bdd-ld-table ../mu-ld-table
++ $(CC) ../bdd-ld-table ../mu-ld-table $(LDFLAGS) -o mu.so ${muobj} -lutils -lm
++
++libutils.a : ${utilobj}
++ ar r libutils.a ${utilobj}
++ ranlib libutils.a
++
++bdd_interface.o : bdd_interface.c bdd_fns.h
++bdd_factor.o : bdd_factor.c bdd_factor.h
++bdd.o : bdd.c bdd.h bdd_extern.h
++bdd_fns.o : bdd_fns.c bdd_fns.h bdd.h bdd_extern.h
++bdd_quant.o : bdd_quant.c bdd_fns.h bdd.h bdd_extern.h
++bdd_vfns.o : bdd_vfns.c bdd_vfns.h bdd_fns.h bdd.h bdd_extern.h
++
++mu_interface.o : mu_interface.c mu.h
++mu.o : mu.c mu.h
++
++double.o : double.c double.h
++list.o : list.c list.h alloc.h
++hash.o : hash.c hash.h alloc.h
++alloc.o : alloc.c
++
++clean :
++ rm -f *.o *.a *.so
++
+--- ./pvs.in.orig 2011-04-15 11:45:09.000000000 -0600
++++ ./pvs.in 2011-12-06 10:42:04.652502258 -0700
+@@ -229,15 +229,8 @@ case $opsys in
+ case `uname -m` in
+ x86_64) PVSARCH=ix86_64 ;;
+ *86*) PVSARCH=ix86 ;;
+- *) echo "PVS only runs on Intel under Linux"; exit 1
++ *) PVSARCH=`uname -m` ;;
esac
- os=SunOS
- os_version=`uname -r | cut -d"." -f1`;;
-- Linux|FreeBSD) case `uname -m` in
-- x86_64) arch=ix86_64;;
-- *86*) arch=ix86;;
-- esac
-- os=Linux;;
-+ Linux|FreeBSD) arch=linux
-+ os=Linux;;
- AIX) arch=powerpc-ibm
- os=AIX
- os_version=`uname -r`;;
+- # Allegro does not work with Linux's New Posix Thread Library (NPTL)
+- # used in newer Red Hat kernels and 2.6 kernels. This will force
+- # the old thread-implementation.
+- export LD_ASSUME_KERNEL=2.4.19;
+- # See if setting this leads to problems - if it does, then
+- # uname exits with an error and we unset it.
+- uname -a > /dev/null 2>&1 || unset LD_ASSUME_KERNEL
+ ;;
+ FreeBSD) opsys=Linux
+ majvers=
+@@ -266,7 +259,7 @@ case $opsys in
+ *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1
+ esac
+
+-binpath=$PVSPATH/bin/$PVSARCH-$opsys${majvers}
++binpath=$PVSPATH/bin/linux
+ # Check if this is a 64-bit platform, but only 32-bit available
+ if [ "$PVSARCH" = "ix86_64" -a ! -x "$binpath" ]
+ then binpath=$PVSPATH/bin/ix86-$opsys${majvers}
+@@ -349,6 +342,7 @@ if [ "$PVSTIMEOUT" -a ! "$batch" ]
+ fi
+
+ PVSVERBOSE=${PVSVERBOSE:-0}
++PVSIMAGE="/usr/bin/sbcl --core $pvsimagepath"
+
+ export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
+ export PVSARCH PVSIMAGE PVSPATH PATH PVSLISP PVSVERBOSE PVSTIMEOUT
+@@ -414,13 +408,13 @@ elif [ $getversion ]
+ then
+ # Make sure there are no spaces in the eval form - otherwise it goes
+ # through the pvs-cmulisp script and gets mangled.
+- echo `$pvsimagepath $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"`
++ echo `$PVSIMAGE $noinit $evalflag "(progn(pvs::pvs-version)(terpri)(bye))"`
+ elif [ $rawmode ]
+ then
+ if [ -n "$emacsargs" ]
+ then echo "Emacs flags '$emacsargs' will be ignored in raw mode"
+ fi
+- $pvsimagepath $noinit $flags
++ $PVSIMAGE $noinit $flags
+ elif [ $batch ]
+ then
+ "$PVSEMACS" $batch $dotemacs $pvsemacsinit $flags 2>&1
+--- ./doc/user-guide/user-guide.tex.orig 2011-04-15 11:45:08.000000000 -0600
++++ ./doc/user-guide/user-guide.tex 2011-12-06 10:39:20.994660844 -0700
+@@ -20,6 +20,7 @@
+ \else
+ \usepackage[bookmarks=true,hyperindex=true]{hyperref}
+ \fi
++\usepackage{amssymb}
+
+ \topmargin -10pt
+ \textheight 8.5in
diff --git a/pvs-sbcl.spec b/pvs-sbcl.spec
index 0c8ebf1..b6ed463 100644
--- a/pvs-sbcl.spec
+++ b/pvs-sbcl.spec
@@ -1,6 +1,6 @@
Name: pvs-sbcl
Version: 5.0
-Release: 4%{?dist}
+Release: 5%{?dist}
Summary: Interactive theorem prover from SRI
Group: Applications/Engineering
@@ -172,6 +172,9 @@ update-desktop-database %{_datadir}/applications &>/dev/null ||:
%{_texmf_main}/tex/latex/pvs
%changelog
+* Tue Dec 6 2011 Jerry James <loganjerry at gmail.com> - 5.0-5
+- Fix building on non-Intel architectures
+
* Mon Nov 07 2011 Rex Dieter <rdieter at fedoraproject.org> 5.0-4
- rebuild (sbcl)
More information about the scm-commits
mailing list