[pvs-sbcl] New upstream release. Drop unnecessary emacs patch. Define LANG while building and add -unicode patc
Jerry James
jjames at fedoraproject.org
Fri Feb 22 19:26:44 UTC 2013
commit 7ef32fa77a49fdc0a52b72a892699fe5e7ba5760
Author: Jerry James <jamesjer at betterlinux.com>
Date: Fri Feb 22 12:26:19 2013 -0700
New upstream release.
Drop unnecessary emacs patch.
Define LANG while building and add -unicode patch to get Unicode support.
.gitignore | 10 +-
pvs-chmod.patch | 6 +-
pvs-emacs.patch | 31 ----
pvs-fedora.patch | 432 ++++++++++++++++++++++++++--------------------------
pvs-sbcl.spec | 59 +++++---
pvs-unicode.patch | 147 ++++++++++++++++++
sources | 2 +-
7 files changed, 411 insertions(+), 276 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index 65f70b8..4674bb7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
-csl-93-9.ps.gz
-csl-97-2.ps.gz
-interpretations.pdf
-pvs-prelude.pdf
-pvs-5.0-source.tgz
+/csl-93-9.ps.gz
+/csl-97-2.ps.gz
+/interpretations.pdf
+/pvs-prelude.pdf
+/pvs-6.0.tar.xz
diff --git a/pvs-chmod.patch b/pvs-chmod.patch
index a7576ba..fdc720c 100644
--- a/pvs-chmod.patch
+++ b/pvs-chmod.patch
@@ -1,6 +1,6 @@
---- src/utils.lisp.orig 2011-04-15 11:45:05.000000000 -0600
-+++ src/utils.lisp 2012-01-20 12:12:15.770232801 -0700
-@@ -398,7 +398,7 @@
+--- ./src/utils.lisp.orig 2013-02-21 08:19:17.033451582 -0700
++++ ./src/utils.lisp 2013-02-21 08:36:17.004144822 -0700
+@@ -413,7 +413,7 @@
#+sbcl
(defun chmod (prot file)
(sb-ext:run-program
diff --git a/pvs-fedora.patch b/pvs-fedora.patch
index 6f2dae5..3e98260 100644
--- a/pvs-fedora.patch
+++ b/pvs-fedora.patch
@@ -1,141 +1,107 @@
---- ./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
+--- ./pvs.in.orig 2013-02-21 08:19:16.955451682 -0700
++++ ./pvs.in 2013-02-21 08:35:32.107201978 -0700
+@@ -225,15 +225,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`;;
---- ./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 @@
+- # 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=
+@@ -262,7 +255,7 @@ case $opsys in
+ *) echo "PVS only runs under Solaris, Linux, FreeBSD (linux-enabled), or MacOSX"; exit 1
+ esac
- ;; 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.
-+endif
-+
-+BDD = ../mona/BDD
-+DFA = ../mona/DFA
-+UTILS = ../mona/Mem
-+INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS)
+-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}
+@@ -345,6 +338,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
+@@ -410,13 +404,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
+--- ./BDD/linux/Makefile.orig 2013-02-21 08:35:32.107201978 -0700
++++ ./BDD/linux/Makefile 2013-02-21 08:35:32.107201978 -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 += -fPIC -fno-strict-aliasing -D_POSIX_SOURCE -DSYSV $(INCLUDES)
++CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -fno-strict-aliasing
+XCFLAGS = -O
+SHELL = /bin/sh
-+VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
++VPATH = ..:../bdd/utils:../bdd/src:../mu/src
+
-+obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
++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 : ws1s.so
++all : mu.so
+
-+ws1s_extended_interface.o : ../ws1s_extended_interface.c
-+ $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
++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
+
-+ws1s.so : ${obj}
-+ $(CC) -shared $(XCFLAGS) $(CFLAGS) $(LDFLAGS) -o ws1s.so ${obj}
++libutils.a : ${utilobj}
++ ar r libutils.a ${utilobj}
++ ranlib libutils.a
+
-+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
++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
+
-+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
++mu_interface.o : mu_interface.c mu.h
++mu.o : mu.c mu.h
+
-+dlmalloc.o: dlmalloc.c dlmalloc.h
-+mem.o: mem.c dlmalloc.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
---- ./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;
-
-
--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;
-
-
- 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
++
+--- ./Makefile.in.orig 2013-02-21 08:19:16.837451834 -0700
++++ ./Makefile.in 2013-02-21 08:35:32.107201978 -0700
@@ -66,7 +66,7 @@ endif
PLATFORM := $(shell $(PVSPATH)bin/pvs-platform)
export PLATFORM
@@ -154,7 +120,7 @@
ifeq ($(shell if [ -x "$(SBCLISPEXE)" ]; then echo OK; fi),OK)
SBCLVERSION = $(shell $(SBCLISPEXE) --version)
# $(warning "$(SBCLVERSION)")
-@@ -190,10 +190,10 @@ emacs-elc = $(filter-out %ilfsf18.elc %i
+@@ -162,10 +162,10 @@ emacs-elc = $(filter-out %ilfsf18.elc %i
%illuc19.elc %ilxemacs.elc %ilisp-menu.elc,\
$(emacs-sub-src:.el=.elc))
@@ -169,7 +135,7 @@
ess = ess/dist-ess.lisp \
ess/init-load.lisp \
-@@ -502,12 +502,12 @@ $(PVSPATH)TAGS : $(lisp-files) $(allegro
+@@ -481,12 +481,12 @@ $(PVSPATH)TAGS : $(lisp-files) $(allegro
$(ETAGS) $(lisp-files) $(allegrolisp) $(sbcllisp) $(cmulisp) $(pvs-emacs-src)
fileutils = \
@@ -186,7 +152,7 @@
image-deps = $(fileutils) $(bddlib) $(ws1slib) $(pvs-make-files) \
$(ess) $(ff-files) $(lisp-files) \
-@@ -544,7 +544,7 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
+@@ -523,7 +523,7 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
--eval "(let ((*load-pvs-prelude* nil)) \
(mk:operate-on-system :pvs :compile))" \
--eval '(quit)'
@@ -195,7 +161,7 @@
@echo "******* Building PVS image $@"
$(SBCLISPEXE) --eval '(require :sb-posix)' \
--eval '(require :sb-md5)' \
-@@ -552,15 +552,14 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
+@@ -531,15 +531,14 @@ $(sbcl-rt) : $(image-deps) $(sbcllisp)
--eval "(unwind-protect \
(mk:operate-on-system :pvs :compile) \
(save-lisp-and-die \"$@\" \
@@ -216,7 +182,7 @@
endif
ifneq ($(CMULISP_HOME),)
-@@ -635,12 +634,12 @@ endif
+@@ -614,12 +613,12 @@ endif
clean distclean tar
$(fileutils) makefileutils :
@@ -232,115 +198,149 @@
make-release-notes :
$(MAKE) -C $(PVSPATH)doc/release-notes
---- ./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)
+--- ./doc/user-guide/user-guide.tex.orig 2013-02-21 08:19:16.876451784 -0700
++++ ./doc/user-guide/user-guide.tex 2013-02-21 08:35:32.107201978 -0700
+@@ -20,6 +20,7 @@
+ \else
+ \usepackage[bookmarks=true,hyperindex=true]{hyperref}
+ \fi
++\usepackage{amssymb}
+
+ \topmargin -10pt
+ \textheight 8.5in
+--- ./bin/pvs-platform.orig 2013-02-21 08:19:16.838451832 -0700
++++ ./bin/pvs-platform 2013-02-21 08:35:32.105201980 -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 2013-02-21 08:35:32.106201979 -0700
++++ ./src/utils/linux/Makefile 2013-02-21 08:35:32.106201979 -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/WS1S/ws1s_table.c.orig 2013-02-21 08:19:16.983451646 -0700
++++ ./src/WS1S/ws1s_table.c 2013-02-21 08:35:32.106201979 -0700
+@@ -182,8 +182,8 @@ extern int dfaPrintVerbose (int);
+ 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;
+
+
+ extern int dfaSetup (int);
+--- ./src/WS1S/linux/Makefile.orig 2013-02-21 08:35:32.106201979 -0700
++++ ./src/WS1S/linux/Makefile 2013-02-21 08:35:32.106201979 -0700
+@@ -0,0 +1,55 @@
++ifneq (,)
++This makefile requires GNU Make.
++endif
++
++BDD = ../mona/BDD
++DFA = ../mona/DFA
++UTILS = ../mona/Mem
++INCLUDES = -I$(BDD) -I$(DFA) -I$(UTILS)
+LDFLAGS = -shared -L./
+CC = gcc
-+CFLAGS = -D_POSIX_SOURCE -DSYSV $(INCLUDES) -DLINUX -DLINUX_REDHAT5 -DSIGNALS_LINUX -fPIC -fno-strict-aliasing
++CFLAGS += -fPIC -fno-strict-aliasing -D_POSIX_SOURCE -DSYSV $(INCLUDES)
+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
++VPATH = ..:../mona/BDD:../mona/DFA:../mona/Mem
+
-+utilobj = double.o list.o hash.o alloc.o
++obj = ws1s_table.o ws1s_extended_interface.o -lmonadfa
+
+.SUFFIXES:
+.SUFFIXES: .c .o
+.c.o : ; $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
+
-+all : mu.so
++all : ws1s.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
++ws1s_extended_interface.o : ../ws1s_extended_interface.c
++ $(CC) $(XCFLAGS) ${CFLAGS} -c $< -o $@
+
-+libutils.a : ${utilobj}
-+ ar r libutils.a ${utilobj}
-+ ranlib libutils.a
++ws1s.so : ${obj}
++ $(CC) -shared $(XCFLAGS) $(CFLAGS) $(LDFLAGS) -o ws1s.so ${obj}
+
-+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
++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
+
-+mu_interface.o : mu_interface.c mu.h
-+mu.o : mu.c mu.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
+
-+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
++dlmalloc.o: dlmalloc.c dlmalloc.h
++mem.o: mem.c dlmalloc.h
+
+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
-- # 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}
+--- ./src/WS1S/ws1s-ld-table.orig 2013-02-21 08:19:16.983451646 -0700
++++ ./src/WS1S/ws1s-ld-table 2013-02-21 08:35:32.106201979 -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/classes-expr.lisp.orig 2013-02-21 08:19:16.989451638 -0700
++++ ./src/classes-expr.lisp 2013-02-21 08:35:32.106201979 -0700
+@@ -36,6 +36,10 @@
- \topmargin -10pt
- \textheight 8.5in
+ ;; 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))
diff --git a/pvs-sbcl.spec b/pvs-sbcl.spec
index 6491c25..f31be5e 100644
--- a/pvs-sbcl.spec
+++ b/pvs-sbcl.spec
@@ -1,15 +1,20 @@
-# workaround http://bugzilla.redhat.com/885762
-%{?!_texmf_main:%global _texmf_main %{_datadir}/texmf}
-
Name: pvs-sbcl
-Version: 5.0
-Release: 20%{?dist}
+Version: 6.0
+Release: 1%{?dist}
Summary: Interactive theorem prover from SRI
Group: Applications/Engineering
License: GPLv2+ and BSD and Public Domain
URL: http://pvs.csl.sri.com/
-Source0: http://pvs.csl.sri.com/download-open/pvs-%{version}-source.tgz
+# SRI no longer provides source tarballs. Generate one from git as follows:
+# git clone https://github.com/samowre/PVS.git pvs-6.0
+# cd pvs-6.0
+# git reset --hard 42a7aae6c6d477dd2c25b846757274176092b08d
+# rm -fr .git*
+# find . -name .cvsignore | xargs rm -f
+# cd ..
+# tar cvJf pvs-6.0.tar.xz pvs-6.0
+Source0: pvs-%{version}.tar.xz
Source1: http://pvs.csl.sri.com/doc/pvs-prelude.pdf
Source2: http://pvs.csl.sri.com/doc/interpretations.pdf
Source3: http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps.gz
@@ -27,10 +32,11 @@ Patch1: pvs-hashfn.patch
# path is passed to a function that expects an absolute path, thereby breaking
# the chmod function
Patch2: pvs-chmod.patch
-# This patch was sent upstream 20 Jan 2012. It adapts to Emacs 24.
-Patch3: pvs-emacs.patch
# Workaround http://bugzilla.redhat.com/886158
-Patch4: pvs-makeindex.patch
+Patch3: pvs-makeindex.patch
+# This patch was sent upstream 22 Feb 2013. It fixes processing of Unicode
+# symbols in the language documentation.
+Patch4: pvs-unicode.patch
BuildRequires: automake
BuildRequires: desktop-file-utils
@@ -42,6 +48,7 @@ BuildRequires: texinfo-tex
BuildRequires: tex(latex)
BuildRequires: tex(boxedminipage.sty)
BuildRequires: tex(relsize.sty)
+BuildRequires: tex(stmaryrd.sty)
BuildRequires: tex(tocbibind.sty)
BuildRequires: emacs
BuildRequires: xemacs
@@ -62,17 +69,17 @@ Requires: sbcl
%endif
%description
-PVS is a verification system: that is, a specification language integrated
-with support tools and a theorem prover. It is intended to capture the
-state-of-the-art in mechanized formal methods and to be sufficiently rugged
-that it can be used for significant applications.
+PVS is a verification system: that is, a specification language
+integrated with support tools and a theorem prover. It is intended to
+capture the state-of-the-art in mechanized formal methods and to be
+sufficiently rugged that it can be used for significant applications.
-This build of PVS must be invoked as "pvs-sbcl", both to distinguish it from
-builds with other Common Lisp engines, and to distinguish it from /sbin/pvs in
-the lvm2 package.
+This build of PVS must be invoked as "pvs-sbcl", both to distinguish it
+from builds with other Common Lisp engines, and to distinguish it from
+/usr/sbin/pvs in the lvm2 package.
%prep
-%setup -q -c
+%setup -q -n pvs-%{version}
%patch0
%patch1
%patch2
@@ -85,7 +92,14 @@ autoreconf -i
# Fix a permission problem
chmod a-x emacs/emacs-src/pvs-prover-manip.el
+# Fix building the language documentation
+ln -s ../makebnf.sty doc/language
+
%build
+# SBCL defaults to an external format of ASCII in mock builds, which breaks
+# the build when PVS tries to read Unicode-encoded files.
+export LANG=en_US.UTF-8
+
%configure
make SBCLISP_HOME=%{_bindir}
make SBCLISP_HOME=%{_bindir} make-release-notes
@@ -179,16 +193,21 @@ fi
update-desktop-database %{_datadir}/applications &>/dev/null ||:
%files
-%doc *.ps.gz *.pdf LICENSE NOTICES README Examples
-%doc doc/PVSio-2.d.pdf doc/api/pvs-api.pdf
-%doc doc/language/language.pdf doc/user-guide/user-guide.pdf
+%doc *.ps.gz *.pdf LICENSE NOTICES README Examples doc/*.pdf
+%doc doc/api/pvs-api.pdf doc/language/language.pdf
%doc doc/prover/prover.pdf doc/release-notes/pvs-release-notes.pdf
+%doc doc/user-guide/user-guide.pdf
%{_bindir}/*
%{_libdir}/pvs
%{_datadir}/applications/*.desktop
%{_texmf_main}/tex/latex/pvs
%changelog
+* Thu Feb 21 2013 Jerry James <loganjerry at gmail.com> - 6.0-1
+- New upstream release
+- Drop unnecessary emacs patch
+- Define LANG while building and add -unicode patch to get Unicode support
+
* Wed Feb 20 2013 Rex Dieter <rdieter at fedoraproject.org> 5.0-20
- rebuild (sbcl)
diff --git a/pvs-unicode.patch b/pvs-unicode.patch
new file mode 100644
index 0000000..2b1ed36
--- /dev/null
+++ b/pvs-unicode.patch
@@ -0,0 +1,147 @@
+--- ./doc/language/language.tex.orig 2013-02-21 08:19:16.000000000 -0700
++++ ./doc/language/language.tex 2013-02-22 11:54:34.856890763 -0700
+@@ -13,6 +13,9 @@
+ \usepackage{latexsym}
+ %\usepackage{showidx} % shows index entries in the margin
+ \usepackage[chapter]{tocbibind}
++\usepackage{amsmath}
++\usepackage{amssymb}
++\usepackage{stmaryrd}
+ \usepackage{ifpdf}
+ \ifpdf
+ \usepackage[pdftex,dvipsnames,usenames]{color}
+--- ./doc/language/pvs-doc.el.in.orig 2013-02-21 08:19:16.000000000 -0700
++++ ./doc/language/pvs-doc.el.in 2013-02-22 11:54:19.800914545 -0700
+@@ -43,15 +43,128 @@
+ "Return a list of which elements are characters in the STRING."
+ (mapcar #'identity string))
+
++(defun unicode-to-latex (cp)
++ (case cp
++ (955 "$\\lambda$")
++ (8226 "$\\bullet$")
++ (8592 "$\\leftarrow$")
++ (8593 "$\\uparrow$")
++ (8594 "$\\rightarrow$")
++ (8595 "$\\downarrow$")
++ (8605 "$\\rightsquigarrow$")
++ (8614 "$\\mapsto$")
++ (8656 "$\\Leftarrow$")
++ (8657 "$\\Uparrow$")
++ (8658 "$\\Rightarrow$")
++ (8659 "$\\Downarrow$")
++ (8660 "$\\Leftrightarrow$")
++ (8704 "$\\forall$")
++ (8707 "$\\exists$")
++ (8711 "$\\nabla$")
++ (8712 "$\\in$")
++ (8713 "$\\notin$")
++ (8715 "$\\ni$")
++ (8723 "$\\mp$")
++ (8724 "$\\dotplus$")
++ (8728 "$\\circ$")
++ (8730 "$\\sqrt{}$")
++ (8739 "$\\mid$")
++ (8741 "$\\parallel$")
++ (8743 "$\\wedge$")
++ (8744 "$\\vee$")
++ (8745 "$\\cap$")
++ (8746 "$\\cup$")
++ (8769 "$\\nsim$")
++ (8771 "$\\eqsim$")
++ (8773 "$\\cong$")
++ (8775 "$\\ncong$")
++ (8776 "$\\approx$")
++ (8777 "$\\not\\approx$")
++ (8781 "$\\asymp$")
++ (8782 "$\\Bumpeq$")
++ (8783 "$\\bumpeq$")
++ (8784 "$\\doteq$")
++ (8791 "$\\circeq$")
++ (8793 "$\\triangleq$")
++ (8800 "$\\neq$")
++ (8801 "$\\equiv$")
++ (8804 "$\\leq$")
++ (8805 "$\\geq$")
++ (8806 "$\\leqq$")
++ (8807 "$\\geqq$")
++ (8808 "$\\lneqq$")
++ (8809 "$\\gneqq$")
++ (8810 "$\\ll$")
++ (8811 "$\\gg$")
++ (8814 "$\\nless$")
++ (8815 "$\\ngtr$")
++ (8816 "$\\nleq$")
++ (8817 "$\\ngeq$")
++ (8826 "$\\prec$")
++ (8827 "$\\succ$")
++ (8834 "$\\subset$")
++ (8835 "$\\supset$")
++ (8836 "$\\not\\subset$")
++ (8837 "$\\not\\supset$")
++ (8838 "$\\subseteq$")
++ (8839 "$\\supseteq$")
++ (8846 "$\\uplus$")
++ (8847 "$\\sqsubset$")
++ (8848 "$\\sqsupset$")
++ (8851 "$\\sqcap$")
++ (8852 "$\\sqcup$")
++ (8853 "$\\oplus$")
++ (8854 "$\\ominus$")
++ (8855 "$\\otimes$")
++ (8856 "$\\oslash$")
++ (8857 "$\\odot$")
++ (8859 "$\\circledast$")
++ (8862 "$\\boxplus$")
++ (8863 "$\\boxminus$")
++ (8864 "$\\boxtimes$")
++ (8866 "$\\boxdot$")
++ (8867 "$\\dashv$")
++ (8869 "$\\bot$")
++ (8872 "$\\vDash$")
++ (8873 "$\\vdash$")
++ (8896 "$\\bigwedge$")
++ (8897 "$\\bigvee$")
++ (8898 "$\\bigcap$")
++ (8899 "$\\bigcup$")
++ (8904 "$\\bowtie$")
++ (8968 "$\\lceil$")
++ (8969 "$\\rceil$")
++ (8970 "$\\lfloor$")
++ (8971 "$\\rfloor$")
++ (8988 "$\\ulcorner$")
++ (8989 "$\\urcorner$")
++ (8990 "$\\llcorner$")
++ (8991 "$\\lrcorner$")
++ (9001 "$\\langle$")
++ (9002 "$\\rangle$")
++ (9633 "$\\square$")
++ (9655 "$\\rhd$")
++ (9665 "$\\lhd$")
++ (9671 "$\\Diamond$")
++ (9711 "$\\bigcirc$")
++ (9733 "$\\bigstar$")
++ (10016 "$\\maltese$")
++ (10752 "$\\bigodot$")
++ (10753 "$\\bigoplus$")
++ (10754 "$\\bigotimes$")
++ (12298 "$\\ll$")
++ (12299 "$\\gg$")
++ (12314 "$\\llbracket$")
++ (12315 "$\\rrbracket$")
++ (t (concat "\\char" (format "%d" cp)))))
++
+ (defun escape-tex-operator-chars (string)
+ (let ((pos (- (length string) 1))
+ (chars nil))
+ (while (>= pos 0)
+ (setq chars
+- (nconc
+- (string-to-char-list (concat "\\char"
+- (format "%d" (aref string pos))))
+- chars))
++ (nconc (string-to-char-list (unicode-to-latex (aref string pos)))
++ chars))
+ (decf pos))
+ (concat chars)))
+
diff --git a/sources b/sources
index f2f6d20..3ae29fb 100644
--- a/sources
+++ b/sources
@@ -1,5 +1,5 @@
9646a3fa12ae6112c4ddd17e4a14c846 csl-93-9.ps.gz
6fd7d301fb569cacb8aa9fb6278498a8 csl-97-2.ps.gz
3c763226529517d39dfb962628492ec2 interpretations.pdf
-f287eefa58162b36e3c43c854e0108b0 pvs-5.0-source.tgz
+6b5c07eaf761157a5b23fbfd733c8d80 pvs-6.0.tar.xz
432c4e35d4b172b227c2c3dbe0afb6a6 pvs-prelude.pdf
More information about the scm-commits
mailing list