The package rpms/pvs-sbcl.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/pvs-sbcl.git/commit/?id=70835bfbb....
Change:
+%ifarch x86_64
Thanks.
Full change:
============
commit 70835bfbbc1696bce1aa3fc717c94fb1569314f7
Author: Jerry James <loganjerry(a)gmail.com>
Date: Fri Feb 28 14:55:24 2020 -0700
Rebuild for sbcl 2.0.1 (bz 1807476).
Update to latest git snapshot for bug fixes.
diff --git a/pvs-fedora.patch b/pvs-fedora.patch
index 8c57923..8c0fdc9 100644
--- a/pvs-fedora.patch
+++ b/pvs-fedora.patch
@@ -1,19 +1,5 @@
---- a/bin/pvs-platform.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/bin/pvs-platform 2020-01-27 11:10:12.334492312 -0700
-@@ -33,10 +33,7 @@ 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
-+ Linux|FreeBSD) arch=linux
- os=Linux;;
- AIX) arch=powerpc-ibm
- os=AIX
---- a/Makefile.in.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/Makefile.in 2020-01-27 11:10:12.374491828 -0700
+--- a/Makefile.in
++++ b/Makefile.in
@@ -169,7 +169,7 @@ endif
ifneq ($(SBCLISP_HOME),)
@@ -23,8 +9,8 @@
ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
SBCLVERSION = $(shell $(SBCLISPEXE) --version)
# $(warning "$(SBCLVERSION)")
---- a/pvs-config.lisp.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/pvs-config.lisp 2020-01-27 11:19:14.701917754 -0700
+--- a/pvs-config.lisp
++++ b/pvs-config.lisp
@@ -46,6 +46,7 @@
(or #+allegro (sys:getenv "PVSPATH")
#+gcl (si:getenv "PVSPATH")
@@ -33,25 +19,11 @@
;; Assume this is loaded while cd'd to the PVS directory
(namestring (truename *default-pathname-defaults*))))
-@@ -85,8 +86,8 @@
- #+(and cmu linux) "x86f"
- #+(and cmu darwin) "ppcf"
- #+(and cmu solaris) "sparcf"
-- #+(and sbcl x86-64 linux) "fasl"
-- #+(and sbcl (not x86-64) linux) "x86s"
-+ #+(and sbcl linux x86 (not x86-64)) "x86s"
-+ #+(and sbcl linux (or (not x86) x86-64)) "fasl"
- #+(and sbcl darwin) "ppcs"
- #+(and sbcl sparc) "sparcs"
- #+(and clisp pc386) "clfasl"
---- a/pvs.in.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/pvs.in 2020-01-27 11:10:12.374491828 -0700
-@@ -233,15 +233,8 @@ case $opsys in
- case `uname -m` in
- x86_64) PVSARCH=ix86_64 ;;
+--- a/pvs.in
++++ b/pvs.in
+@@ -235,13 +235,6 @@ case $opsys in
*86*) PVSARCH=ix86 ;;
-- *) echo "PVS only runs on Intel under Linux"; exit 1
-+ *) PVSARCH=$(uname -m) ;;
+ *) echo "PVS only runs on Intel under Linux"; exit 1
esac
- # 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
@@ -63,183 +35,20 @@
;;
FreeBSD) opsys=Linux
majvers=
-@@ -276,11 +269,7 @@ case $opsys in
- *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or
MacOSX"; exit 1
- esac
-
--PVSBINPATH=$PVSPATH/bin/$PVSARCH-$opsys${majvers}
--# Check if this is a 64-bit platform, but only 32-bit available
--if [ "$PVSARCH" = "ix86_64" -a ! -x "$PVSBINPATH" ]
-- then PVSBINPATH=$PVSPATH/bin/ix86-$opsys${majvers}
--fi
-+PVSBINPATH=$PVSPATH/bin/linux-Linux
+--- a/pvs.system
++++ b/pvs.system
+@@ -160,7 +160,8 @@
- if [ -n "$PVSLISP" -a "$PVSLISP" != "allegro" -a
"$PVSLISP" != "cmulisp" -a "$PVSLISP" != "sbclisp"
]
- then echo "ERROR: PVSLISP must be unset, or set to 'allegro',
'cmulisp', or 'sbclisp'"
---- a/src/BDD/linux-Linux/Makefile.orig 2020-01-27 11:10:12.375491816 -0700
-+++ b/src/BDD/linux-Linux/Makefile 2020-01-27 11:10:12.375491816 -0700
-@@ -0,0 +1,49 @@
-+BDD = ../bdd/src
-+MU = ../mu/src
-+UTILS = ../bdd/utils
-+INCLUDES = -I/usr/include -I$(BDD) -I$(UTILS) -I$(MU)
-+#LD = gcc
-+#LDFLAGS = -shared -L./
-+LD = gcc
-+LDFLAGS = -Xlinker -Bsymbolic -shared -L./ @LDFLAGS@
-+CC = gcc
-+CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX
-fPIC @CFLAGS@
-+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
---- a/src/classes-expr.lisp.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/src/classes-expr.lisp 2020-01-27 11:10:12.375491816 -0700
-@@ -34,8 +34,9 @@
- equation iff iff-or-boolean-equation implication index negation
- propositional-application))
+ #+sbcl
+ (eval-when (:execute :compile-toplevel :load-toplevel)
+- (sb-ext:unlock-package :common-lisp))
++ (sb-ext:unlock-package :common-lisp)
++ (sb-ext:unlock-package :sb-impl))
--;; 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))
---- a/src/utils/linux-Linux/Makefile.orig 2020-01-27 11:10:12.376491804 -0700
-+++ b/src/utils/linux-Linux/Makefile 2020-01-27 11:10:12.376491804 -0700
-@@ -0,0 +1,23 @@
-+LD = gcc
-+LDFLAGS = -shared -L./ @LDFLAGS@
-+CC=gcc
-+CFLAGS=-fPIC @CFLAGS@
-+WFLAGS=-Wall
-+VPATH=..
-+
-+obj=file_utils.o
-+
-+.SUFFIXES:
-+.SUFFIXES: .c .o
-+.c.o : ; $(CC) $(XCFLAGS) ${WFLAGS} ${CFLAGS} -c $< -o $@
-+
-+all : file_utils.so b64
-+
-+file_utils.so: ${obj}
-+ $(LD) ../utils-ld-table $(LDFLAGS) -o file_utils.so ${obj} -lc
-+
-+b64: ../b64.c
-+ $(CC) -o ./b64 ../b64.c
-+
-+clean :
-+ rm -f *.o *.a *.so b64
---- a/src/WS1S/linux-Linux/Makefile.orig 2020-01-27 11:10:12.379491768 -0700
-+++ b/src/WS1S/linux-Linux/Makefile 2020-01-27 11:10:12.379491768 -0700
-@@ -0,0 +1,67 @@
-+ifneq (,)
-+This makefile requires GNU Make.
-+endif
-+
-+BDD = ../mona/BDD
-+DFA = ../mona/DFA
-+UTILS = ../mona/Mem
-+INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS)
-+LD = gcc
-+LDFLAGS = -shared -L./ @LDFLAGS@
-+CC = gcc
-+CFLAGS += -fPIC -D_POSIX_SOURCE -DSYSV -D_BSD_SOURCE $(INCLUDES) @CFLAGS@
-+XCFLAGS = -O
-+SHELL = /bin/sh
-+VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
-+
-+#obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
-+
-+obj = analyze.o prefix.o product.o \
-+ quotient.o basic.o external.o \
-+ makebasic.o minimize.o printdfa.o \
-+ project.o dfa.o \
-+ bdd.o bdd_double.o bdd_external.o \
-+ bdd_manager.o hash.o bdd_dump.o \
-+ bdd_trace.o bdd_cache.o \
-+ dlmalloc.o mem.o \
-+ ws1s_table.o \
-+ ws1s_extended_interface.o
-+
-+.SUFFIXES:
-+.SUFFIXES: .c .o
-+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
-+
-+all : ws1s.so
-+
-+ws1s_extended_interface.o : ../ws1s_extended_interface.c
-+ $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
-+
-+ws1s.so : ${obj}
-+ $(CC) -shared $(CFLAGS) -o ws1s.so ${obj} $(LDFLAGS) -lmonabdd
-+
-+bdd.o: bdd.c bdd.h bdd_internal.h
-+bdd_double.o: bdd_double.c bdd.h bdd_internal.h
-+bdd_external.o: bdd_external.c bdd_external.h mem.h
-+bdd_manager.o: bdd_manager.c bdd.h bdd_internal.h
-+hash.o: hash.c mem.h hash.h
-+bdd_dump.o: bdd_dump.c bdd_dump.h
-+bdd_trace.o: bdd_trace.c bdd.h bdd_internal.h
-+bdd_cache.o: bdd_cache.c bdd.h bdd_internal.h
-+
-+analyze.o: analyze.c dfa.h mem.h
-+prefix.o: prefix.c dfa.h mem.h
-+product.o: product.c dfa.h bdd.h hash.h mem.h
-+quotient.o: quotient.c dfa.h hash.h mem.h
-+basic.o: basic.c dfa.h mem.h
-+external.o: external.c dfa.h bdd_external.h mem.h
-+makebasic.o: makebasic.c dfa.h bdd_internal.h
-+minimize.o: minimize.c dfa.h hash.h mem.h
-+printdfa.o: printdfa.c dfa.h mem.h
-+project.o: project.c dfa.h hash.h mem.h
-+dfa.o: dfa.c dfa.h bdd.h hash.h mem.h
-+
-+dlmalloc.o: dlmalloc.c dlmalloc.h
-+mem.o: mem.c dlmalloc.h
-+
-+clean :
-+ rm -f *.o *.a *.so
---- a/src/WS1S/ws1s-ld-table.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/src/WS1S/ws1s-ld-table 2020-01-27 11:10:12.379491768 -0700
+ (eval-when (:execute :compile-toplevel :load-toplevel)
+--- a/src/WS1S/ws1s-ld-table
++++ b/src/WS1S/ws1s-ld-table
@@ -46,7 +46,7 @@ ws1s___dfaPrintVitals = dfaPrintVitals ;
ws1s___dfaPrint = dfaPrint ;
ws1s___dfaPrintGraphviz = dfaPrintGraphviz ;
@@ -249,8 +58,8 @@
ws1s___dfaSetup = dfaSetup ;
ws1s___dfaAllocExceptions = dfaAllocExceptions ;
ws1s___dfaStoreException = dfaStoreException ;
---- a/src/WS1S/ws1s_table.c.orig 2020-01-23 00:17:15.000000000 -0700
-+++ b/src/WS1S/ws1s_table.c 2020-01-27 11:10:12.379491768 -0700
+--- a/src/WS1S/ws1s_table.c
++++ b/src/WS1S/ws1s_table.c
@@ -182,8 +182,8 @@ extern int dfaPrintVerbose (int);
int (*ws1s___dfaPrintVerbose)(int) = dfaPrintVerbose;
diff --git a/pvs-sbcl.spec b/pvs-sbcl.spec
index 4bb0b6b..765ff89 100644
--- a/pvs-sbcl.spec
+++ b/pvs-sbcl.spec
@@ -1,8 +1,18 @@
# Upstream stopped making release tarballs in 2015. Pull from git until
# upstream starts making them again.
-%global gittag b517ae299f6c25651631ec895be29f43a203de93
+%global gittag a1f7148bdd3343e3faf60b5ad4ae62c2e513512a
%global shorttag %(cut -b -7 <<< %{gittag})
-%global gitdate 20200129
+%global gitdate 20200218
+
+%ifarch %{ix86}
+%global pvsarch ix86
+%else
+%ifarch x86_64
+%global pvsarch ix86_64
+%else
+%global pvsarch %{_arch}
+%endif
+%endif
Name: pvs-sbcl
Version: 7.0
@@ -115,14 +125,15 @@ sed -i 's/\$(TEXI2HTML).*-nav/texi2any --html
--no-number-sections/' \
doc/release-notes/Makefile
# Insert our build flags
-sed -i "s|@CFLAGS@|%{optflags}|;s|@LDFLAGS@|$RPM_LD_FLAGS|" \
- src/BDD/linux-Linux/Makefile \
- src/utils/linux-Linux/Makefile \
- src/WS1S/linux-Linux/Makefile
+sed -i "/XCFLAGS/s|-O|%{optflags}|" src/{BDD,WS1S}/%{pvsarch}-Linux/Makefile
+sed -i "/WFLAGS/s|-Wall|%{optflags}|" src/utils/%{pvsarch}-Linux/Makefile
+sed -i "s|^LDFLAGS =.*|& $RPM_LD_FLAGS|" \
+ src/{BDD,utils,WS1S}/%{pvsarch}-Linux/Makefile
+sed -i "s|-o ws1s.so.*|& -lmonabdd|" src/WS1S/%{pvsarch}-Linux/Makefile
# Make yices available where the build system expects it
-mkdir -p yices/linux-Linux/yices-2.6/bin
-cp -p %{_bindir}/yices yices/linux-Linux/yices-2.6/bin/yices
+mkdir -p yices/%{pvsarch}-Linux/yices-2.6/bin
+cp -p %{_bindir}/yices yices/%{pvsarch}-Linux/yices-2.6/bin/yices
# Remove obsolete version control files
find . -name .cvsignore -delete
@@ -217,9 +228,9 @@ desktop-file-install --mode=644
--dir=%{buildroot}%{_datadir}/applications \
%{SOURCE5}
# Adjust the sbcl and yices symlinks
-rm %{buildroot}%{_libdir}/pvs/bin/linux-Linux/{runtime/sbcl,yices2}
-ln -s %{_bindir}/yices %{buildroot}%{_libdir}/pvs/bin/linux-Linux/yices2
-ln -s %{_bindir}/sbcl %{buildroot}%{_libdir}/pvs/bin/linux-Linux/runtime/sbcl
+rm %{buildroot}%{_libdir}/pvs/bin/%{pvsarch}-Linux/{runtime/sbcl,yices2}
+ln -s %{_bindir}/yices %{buildroot}%{_libdir}/pvs/bin/%{pvsarch}-Linux/yices2
+ln -s %{_bindir}/sbcl %{buildroot}%{_libdir}/pvs/bin/%{pvsarch}-Linux/runtime/sbcl
# Remove a hidden make marker
rm %{buildroot}%{_libdir}/pvs/emacs/.readme
@@ -239,6 +250,10 @@ rm %{buildroot}%{_libdir}/pvs/emacs/.readme
%{_texmf}/tex/latex/pvs/
%changelog
+* Fri Feb 28 2020 Jerry James <loganjerry(a)gmail.com> - 7.0-1.20200218.a1f7148
+- Rebuild for sbcl 2.0.1 (bz 1807476)
+- Update to latest git snapshot for bug fixes
+
* Tue Feb 4 2020 Jerry James <loganjerry(a)gmail.com> - 7.0-1.20200129.b517ae2
- Update to latest git snapshot
- Drop upstream patches: -chmod, -emacs26, -hashfn, -makeindex,
diff --git a/sources b/sources
index 435220b..6a58e35 100644
--- a/sources
+++ b/sources
@@ -2,4 +2,4 @@ SHA512 (csl-93-9.ps.gz) =
a742b236ba4cc6ba647be00f5c3174d058d1ab98e30582c77d8511
SHA512 (csl-97-2.ps.gz) =
c2a151989e485e26ed4e227d689dde879bf9c73519b9be62c849bb1c30a310682023b1f4666c5f51ba6a283e17be3c43be27530dc723ee3b9f4686210f0f62d1
SHA512 (interpretations.pdf) =
e06fdca6ebf5c701f749caec735ae9fa49c4740bf69133446c7deee78729f83ecf42b5571488864c1de5a0e81c4a900c8bb93f6189dc2009c0ab57d92e18d6a0
SHA512 (pvs-prelude.pdf) =
cee5b938ec9684e2fb205abce08d9c56c9a7f00dab626f24c3431da5b66ea58b616915a5a6678c3056e31454d5197b5bb052b67ec6c7cbabbfe4061ded305d9c
-SHA512 (PVS-7.0-b517ae2.tar.xz) =
334ff68e6e0b9dd58072b8ed6705307da52f90a77b541d14975163102ccbdc14b8ab10cf8ff7c323e57f1d6972fa786025d0894d58a190b38891d44f3a116d9e
+SHA512 (PVS-7.0-a1f7148.tar.xz) =
ad618028fdc53b845cc0d3dd6a16bc8a8f3825778819befcc9883b0b279d0558ade5db553e7f36b03745ef494ee02378b4df6ace079b88aaa9364740694cc801