Upgrade to 3.0 (previous version was actually 3.0-beta.) -> bump

PKGREVISION.
Also use buildlink2 and emacs.mk for simplicity.

4 files changed, 83 insertions, 319 deletions

diff --git a/devel/pvs/Makefile b/devel/pvs/Makefile
index 18a22db89bb..863bf62c487 100644
--- a/devel/pvs/Makefile
+++ b/devel/pvs/Makefile
@@ -1,7 +1,8 @@
-# $NetBSD: Makefile,v 1.1.1.1 2002/09/24 17:57:24 jschauma Exp $
+# $NetBSD: Makefile,v 1.2 2002/12/20 21:37:37 jschauma Exp $
 #
 
 DISTNAME=		pvs-${VERSION}
+PKGREVISION=		1
 CATEGORIES=		devel lang
 MASTER_SITES=		ftp://pvs.csl.sri.com/pub/pvs/pvs${VERSION}/ \
 			ftp://ftp.informatik.uni-ulm.de/pub/KI/pvs/pvs${VERSION}/
@@ -15,13 +16,12 @@ MAINTAINER=		jschauma@netbsd.org
 HOMEPAGE=		http://pvs.csl.sri.com/
 COMMENT=		The PVS Specification and Verification System
 
-DEPENDS=		emacs>=19.0:../../editors/emacs
-DEPENDS+=		tk>=8.3:../../x11/tk
 DEPENDS+=		teTeX>=1.0.7:../../print/teTeX
 
 VERSION=		3.0
 WRKSRC=			${WRKDIR}
 NO_BUILD=		# defined
+USE_BUILDLINK2=		yes
 
 LICENSE=        	pvs-license
 # not quite sure about this, but to be on the safe side:
@@ -57,4 +57,7 @@ do-install:
 	cd ${WRKSRC} && ${PAX} -s ,^./[.].*,, -rw . ${PREFIX}/pvs
 	${CHMOD} 755 ${PREFIX}/pvs/pvs
 
+.include "../../x11/tk/buildlink2.mk"
+.include "../../mk/emacs.mk"
+.include "../../mk/texinfo.mk"
 .include "../../mk/bsd.pkg.mk"
diff --git a/devel/pvs/PLIST b/devel/pvs/PLIST
index e8244fc1efa..f9b787d137c 100644
--- a/devel/pvs/PLIST
+++ b/devel/pvs/PLIST
@@ -1,18 +1,35 @@
-@comment $NetBSD: PLIST,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+@comment $NetBSD: PLIST,v 1.2 2002/12/20 21:37:38 jschauma Exp $
 bin/pvs
+pvs/Examples/README
+pvs/Examples/ackerman.pvs
+pvs/Examples/f91.pvs
+pvs/Examples/groups.pvs
+pvs/Examples/stack.pvs
+pvs/Examples/stacks.pvs
+pvs/Examples/sum.pvs
+pvs/Examples/sum2.pvs
+pvs/Examples/ustacks.pvs
 pvs/README
 pvs/bin/ix86-redhat5/runtime/file_utils.so
 pvs/bin/ix86-redhat5/runtime/files.bu
-pvs/bin/ix86-redhat5/runtime/ics_lisp_error.so
-pvs/bin/ix86-redhat5/runtime/libacli601.so
-pvs/bin/ix86-redhat5/runtime/libics.so
+pvs/bin/ix86-redhat5/runtime/ics_lisp.so
+pvs/bin/ix86-redhat5/runtime/libacl623.so
 pvs/bin/ix86-redhat5/runtime/mu.so
-pvs/bin/ix86-redhat5/runtime/pvs-allegro6.0
+pvs/bin/ix86-redhat5/runtime/pvs-allegro6.2
 pvs/bin/ix86-redhat5/runtime/pvs-allegro6.dxl
 pvs/bin/ix86-redhat5/runtime/pvs-allegro6.lic
 pvs/bin/ix86-redhat5/runtime/ws1s.so
 pvs/bin/pvs-platform
 pvs/bin/relocate
+pvs/bin/tarmail
+pvs/bin/untarmail
+pvs/doc/release-notes/pvs3.0-release-notes.html
+@unexec ${INSTALL_INFO} --delete --info-dir=%D/info %D/pvs/doc/release-notes/pvs3.0-release-notes.info
+pvs/doc/release-notes/pvs3.0-release-notes.info
+@exec ${INSTALL_INFO} --info-dir=%D/info %D/pvs/doc/release-notes/pvs3.0-release-notes.info
+pvs/doc/release-notes/pvs3.0-release-notes.pdf
+pvs/doc/release-notes/pvs3.0-release-notes.ps
+pvs/doc/release-notes/pvs3.0-release-notes.texi
 pvs/emacs/README
 pvs/emacs/emacs-src/ilisp/comint-ipc.el
 pvs/emacs/emacs-src/ilisp/completer.el
@@ -70,12 +87,15 @@ pvs/emacs/emacs-src/pvs-load.el
 pvs/emacs/emacs-src/pvs-macros.el
 pvs/emacs/emacs-src/pvs-menu.el
 pvs/emacs/emacs-src/pvs-mode.el
+pvs/emacs/emacs-src/pvs-prelude-files-and-regions.el
 pvs/emacs/emacs-src/pvs-print.el
 pvs/emacs/emacs-src/pvs-prover-helps.el
 pvs/emacs/emacs-src/pvs-prover.el
+pvs/emacs/emacs-src/pvs-set-prelude-info.el
 pvs/emacs/emacs-src/pvs-tcl.el
 pvs/emacs/emacs-src/pvs-utils.el
 pvs/emacs/emacs-src/pvs-view.el
+pvs/emacs/emacs-src/pvs.xpm
 pvs/emacs/emacs-src/tcl.el
 pvs/emacs/emacs19/Makefile
 pvs/emacs/emacs19/comint-ipc.el
@@ -173,12 +193,14 @@ pvs/emacs/emacs19/pvs-menu.el
 pvs/emacs/emacs19/pvs-menu.elc
 pvs/emacs/emacs19/pvs-mode.el
 pvs/emacs/emacs19/pvs-mode.elc
+pvs/emacs/emacs19/pvs-prelude-files-and-regions.el
 pvs/emacs/emacs19/pvs-print.el
 pvs/emacs/emacs19/pvs-print.elc
 pvs/emacs/emacs19/pvs-prover-helps.el
 pvs/emacs/emacs19/pvs-prover-helps.elc
 pvs/emacs/emacs19/pvs-prover.el
 pvs/emacs/emacs19/pvs-prover.elc
+pvs/emacs/emacs19/pvs-set-prelude-info.el
 pvs/emacs/emacs19/pvs-tcl.el
 pvs/emacs/emacs19/pvs-tcl.elc
 pvs/emacs/emacs19/pvs-utils.el
@@ -282,12 +304,14 @@ pvs/emacs/emacs20/pvs-menu.el
 pvs/emacs/emacs20/pvs-menu.elc
 pvs/emacs/emacs20/pvs-mode.el
 pvs/emacs/emacs20/pvs-mode.elc
+pvs/emacs/emacs20/pvs-prelude-files-and-regions.el
 pvs/emacs/emacs20/pvs-print.el
 pvs/emacs/emacs20/pvs-print.elc
 pvs/emacs/emacs20/pvs-prover-helps.el
 pvs/emacs/emacs20/pvs-prover-helps.elc
 pvs/emacs/emacs20/pvs-prover.el
 pvs/emacs/emacs20/pvs-prover.elc
+pvs/emacs/emacs20/pvs-set-prelude-info.el
 pvs/emacs/emacs20/pvs-tcl.el
 pvs/emacs/emacs20/pvs-tcl.elc
 pvs/emacs/emacs20/pvs-utils.el
@@ -297,115 +321,6 @@ pvs/emacs/emacs20/pvs-view.elc
 pvs/emacs/emacs20/tcl.el
 pvs/emacs/emacs20/tcl.elc
 pvs/emacs/go-pvs.el
-pvs/emacs/xemacs20/comint-ipc.el
-pvs/emacs/xemacs20/comint-ipc.elc
-pvs/emacs/xemacs20/completer.el
-pvs/emacs/xemacs20/completer.elc
-pvs/emacs/xemacs20/completer.new.el
-pvs/emacs/xemacs20/completer.no-fun.el
-pvs/emacs/xemacs20/ilcompat.el
-pvs/emacs/xemacs20/ilfsf18.el
-pvs/emacs/xemacs20/ilfsf19.el
-pvs/emacs/xemacs20/ilfsf20.el
-pvs/emacs/xemacs20/ilisp-acl.el
-pvs/emacs/xemacs20/ilisp-acl.elc
-pvs/emacs/xemacs20/ilisp-aut.el
-pvs/emacs/xemacs20/ilisp-aut.elc
-pvs/emacs/xemacs20/ilisp-bat.el
-pvs/emacs/xemacs20/ilisp-chs.el
-pvs/emacs/xemacs20/ilisp-cl.el
-pvs/emacs/xemacs20/ilisp-cl.elc
-pvs/emacs/xemacs20/ilisp-cmp.el
-pvs/emacs/xemacs20/ilisp-cmp.elc
-pvs/emacs/xemacs20/ilisp-cmt.el
-pvs/emacs/xemacs20/ilisp-cmt.elc
-pvs/emacs/xemacs20/ilisp-def.el
-pvs/emacs/xemacs20/ilisp-def.elc
-pvs/emacs/xemacs20/ilisp-dia.el
-pvs/emacs/xemacs20/ilisp-dia.elc
-pvs/emacs/xemacs20/ilisp-doc.el
-pvs/emacs/xemacs20/ilisp-doc.elc
-pvs/emacs/xemacs20/ilisp-el.el
-pvs/emacs/xemacs20/ilisp-el.elc
-pvs/emacs/xemacs20/ilisp-ext.el
-pvs/emacs/xemacs20/ilisp-ext.elc
-pvs/emacs/xemacs20/ilisp-hi.el
-pvs/emacs/xemacs20/ilisp-hi.elc
-pvs/emacs/xemacs20/ilisp-hnd.el
-pvs/emacs/xemacs20/ilisp-hnd.elc
-pvs/emacs/xemacs20/ilisp-ind.el
-pvs/emacs/xemacs20/ilisp-ind.elc
-pvs/emacs/xemacs20/ilisp-inp.el
-pvs/emacs/xemacs20/ilisp-inp.elc
-pvs/emacs/xemacs20/ilisp-key.el
-pvs/emacs/xemacs20/ilisp-key.elc
-pvs/emacs/xemacs20/ilisp-kil.el
-pvs/emacs/xemacs20/ilisp-kil.elc
-pvs/emacs/xemacs20/ilisp-low.el
-pvs/emacs/xemacs20/ilisp-low.elc
-pvs/emacs/xemacs20/ilisp-menu.el
-pvs/emacs/xemacs20/ilisp-mnb.el
-pvs/emacs/xemacs20/ilisp-mod.el
-pvs/emacs/xemacs20/ilisp-mod.elc
-pvs/emacs/xemacs20/ilisp-mov.el
-pvs/emacs/xemacs20/ilisp-mov.elc
-pvs/emacs/xemacs20/ilisp-out.el
-pvs/emacs/xemacs20/ilisp-out.elc
-pvs/emacs/xemacs20/ilisp-prc.el
-pvs/emacs/xemacs20/ilisp-prc.elc
-pvs/emacs/xemacs20/ilisp-prn.el
-pvs/emacs/xemacs20/ilisp-prn.elc
-pvs/emacs/xemacs20/ilisp-rng.el
-pvs/emacs/xemacs20/ilisp-rng.elc
-pvs/emacs/xemacs20/ilisp-snd.el
-pvs/emacs/xemacs20/ilisp-snd.elc
-pvs/emacs/xemacs20/ilisp-src.el
-pvs/emacs/xemacs20/ilisp-sym.el
-pvs/emacs/xemacs20/ilisp-sym.elc
-pvs/emacs/xemacs20/ilisp-utl.el
-pvs/emacs/xemacs20/ilisp-utl.elc
-pvs/emacs/xemacs20/ilisp-val.el
-pvs/emacs/xemacs20/ilisp-val.elc
-pvs/emacs/xemacs20/ilisp-xfr.el
-pvs/emacs/xemacs20/ilisp-xfr.elc
-pvs/emacs/xemacs20/ilisp-xls.el
-pvs/emacs/xemacs20/ilisp.el
-pvs/emacs/xemacs20/illuc19.el
-pvs/emacs/xemacs20/ilxemacs.el
-pvs/emacs/xemacs20/pvs-abbreviations.el
-pvs/emacs/xemacs20/pvs-abbreviations.elc
-pvs/emacs/xemacs20/pvs-browser.el
-pvs/emacs/xemacs20/pvs-browser.elc
-pvs/emacs/xemacs20/pvs-byte-compile.el
-pvs/emacs/xemacs20/pvs-cmds.el
-pvs/emacs/xemacs20/pvs-cmds.elc
-pvs/emacs/xemacs20/pvs-eval.el
-pvs/emacs/xemacs20/pvs-eval.elc
-pvs/emacs/xemacs20/pvs-file-list.el
-pvs/emacs/xemacs20/pvs-file-list.elc
-pvs/emacs/xemacs20/pvs-ilisp.el
-pvs/emacs/xemacs20/pvs-load.el
-pvs/emacs/xemacs20/pvs-load.elc
-pvs/emacs/xemacs20/pvs-macros.el
-pvs/emacs/xemacs20/pvs-macros.elc
-pvs/emacs/xemacs20/pvs-menu.el
-pvs/emacs/xemacs20/pvs-menu.elc
-pvs/emacs/xemacs20/pvs-mode.el
-pvs/emacs/xemacs20/pvs-mode.elc
-pvs/emacs/xemacs20/pvs-print.el
-pvs/emacs/xemacs20/pvs-print.elc
-pvs/emacs/xemacs20/pvs-prover-helps.el
-pvs/emacs/xemacs20/pvs-prover-helps.elc
-pvs/emacs/xemacs20/pvs-prover.el
-pvs/emacs/xemacs20/pvs-prover.elc
-pvs/emacs/xemacs20/pvs-tcl.el
-pvs/emacs/xemacs20/pvs-tcl.elc
-pvs/emacs/xemacs20/pvs-utils.el
-pvs/emacs/xemacs20/pvs-utils.elc
-pvs/emacs/xemacs20/pvs-view.el
-pvs/emacs/xemacs20/pvs-view.elc
-pvs/emacs/xemacs20/tcl.el
-pvs/emacs/xemacs20/tcl.elc
 pvs/emacs/xemacs21/comint-ipc.el
 pvs/emacs/xemacs21/comint-ipc.elc
 pvs/emacs/xemacs21/completer.el
@@ -501,12 +416,14 @@ pvs/emacs/xemacs21/pvs-menu.el
 pvs/emacs/xemacs21/pvs-menu.elc
 pvs/emacs/xemacs21/pvs-mode.el
 pvs/emacs/xemacs21/pvs-mode.elc
+pvs/emacs/xemacs21/pvs-prelude-files-and-regions.el
 pvs/emacs/xemacs21/pvs-print.el
 pvs/emacs/xemacs21/pvs-print.elc
 pvs/emacs/xemacs21/pvs-prover-helps.el
 pvs/emacs/xemacs21/pvs-prover-helps.elc
 pvs/emacs/xemacs21/pvs-prover.el
 pvs/emacs/xemacs21/pvs-prover.elc
+pvs/emacs/xemacs21/pvs-set-prelude-info.el
 pvs/emacs/xemacs21/pvs-tcl.el
 pvs/emacs/xemacs21/pvs-tcl.elc
 pvs/emacs/xemacs21/pvs-utils.el
@@ -515,114 +432,28 @@ pvs/emacs/xemacs21/pvs-view.el
 pvs/emacs/xemacs21/pvs-view.elc
 pvs/emacs/xemacs21/tcl.el
 pvs/emacs/xemacs21/tcl.elc
-pvs/lib/bitvectors/.cvsignore
 pvs/lib/bitvectors/.pvscontext
-pvs/lib/bitvectors/CVS/.cvsignore,t
-pvs/lib/bitvectors/CVS/Entries
-pvs/lib/bitvectors/CVS/Repository
-pvs/lib/bitvectors/CVS/Root
-pvs/lib/bitvectors/CVS/Tag
-pvs/lib/bitvectors/CVS/bit.prf,t
-pvs/lib/bitvectors/CVS/bit.pvs,t
-pvs/lib/bitvectors/CVS/bitvectors-doc.ps,t
-pvs/lib/bitvectors/CVS/bv.prf,t
-pvs/lib/bitvectors/CVS/bv.pvs,t
-pvs/lib/bitvectors/CVS/bv_adder.prf,t
-pvs/lib/bitvectors/CVS/bv_adder.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_caret.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_caret.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_caret_concat_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_caret_concat_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_caret_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_caret_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_concat.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_concat.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_extend.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_extend.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_int_caret.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_int_caret.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_int_concat.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_int_concat.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_int_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_int_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_minus_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_minus_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_nat.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_nat.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_nat_caret_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_nat_caret_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_nat_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_nat_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arith_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_arith_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_arithmetic.prf,t
-pvs/lib/bitvectors/CVS/bv_arithmetic.pvs,t
-pvs/lib/bitvectors/CVS/bv_bitwise.prf,t
-pvs/lib/bitvectors/CVS/bv_bitwise.pvs,t
-pvs/lib/bitvectors/CVS/bv_bitwise_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_bitwise_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret.prf,t
-pvs/lib/bitvectors/CVS/bv_caret.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret_bitwise.prf,t
-pvs/lib/bitvectors/CVS/bv_caret_bitwise.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret_bitwise_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_caret_bitwise_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret_concat.prf,t
-pvs/lib/bitvectors/CVS/bv_caret_concat.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret_concat_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_caret_concat_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_caret_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_caret_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_cnv.pvs,t
-pvs/lib/bitvectors/CVS/bv_concat.prf,t
-pvs/lib/bitvectors/CVS/bv_concat.pvs,t
-pvs/lib/bitvectors/CVS/bv_concat_def.prf,t
-pvs/lib/bitvectors/CVS/bv_concat_def.pvs,t
-pvs/lib/bitvectors/CVS/bv_concat_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_concat_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_constants.prf,t
-pvs/lib/bitvectors/CVS/bv_constants.pvs,t
-pvs/lib/bitvectors/CVS/bv_core.pvs,t
-pvs/lib/bitvectors/CVS/bv_extend.prf,t
-pvs/lib/bitvectors/CVS/bv_extend.pvs,t
-pvs/lib/bitvectors/CVS/bv_fract.prf,t
-pvs/lib/bitvectors/CVS/bv_fract.pvs,t
-pvs/lib/bitvectors/CVS/bv_int.prf,t
-pvs/lib/bitvectors/CVS/bv_int.pvs,t
-pvs/lib/bitvectors/CVS/bv_nat.prf,t
-pvs/lib/bitvectors/CVS/bv_nat.pvs,t
-pvs/lib/bitvectors/CVS/bv_nat_rules.prf,t
-pvs/lib/bitvectors/CVS/bv_nat_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_notes.pvs,t
-pvs/lib/bitvectors/CVS/bv_overflow.prf,t
-pvs/lib/bitvectors/CVS/bv_overflow.pvs,t
-pvs/lib/bitvectors/CVS/bv_rotate.prf,t
-pvs/lib/bitvectors/CVS/bv_rotate.pvs,t
-pvs/lib/bitvectors/CVS/bv_rules.pvs,t
-pvs/lib/bitvectors/CVS/bv_shift.prf,t
-pvs/lib/bitvectors/CVS/bv_shift.pvs,t
-pvs/lib/bitvectors/CVS/bv_sum.prf,t
-pvs/lib/bitvectors/CVS/bv_sum.pvs,t
-pvs/lib/bitvectors/CVS/div.prf,t
-pvs/lib/bitvectors/CVS/div.pvs,t
-pvs/lib/bitvectors/CVS/empty_bv.pvs,t
-pvs/lib/bitvectors/CVS/exp2.prf,t
-pvs/lib/bitvectors/CVS/exp2.pvs,t
-pvs/lib/bitvectors/CVS/floor_div_props.prf,t
-pvs/lib/bitvectors/CVS/floor_div_props.pvs,t
-pvs/lib/bitvectors/CVS/mod.prf,t
-pvs/lib/bitvectors/CVS/mod.pvs,t
-pvs/lib/bitvectors/CVS/mod_rules.prf,t
-pvs/lib/bitvectors/CVS/mod_rules.pvs,t
-pvs/lib/bitvectors/CVS/orphaned-proofs.prf,t
-pvs/lib/bitvectors/CVS/sums.prf,t
-pvs/lib/bitvectors/CVS/sums.pvs,t
-pvs/lib/bitvectors/CVS/top.pvs,t
-pvs/lib/bitvectors/bit.prf
-pvs/lib/bitvectors/bit.pvs
-pvs/lib/bitvectors/bitvectors-doc.ps
-pvs/lib/bitvectors/bv.prf
-pvs/lib/bitvectors/bv.pvs
+pvs/lib/bitvectors/BitvectorMultiplication.bin
+pvs/lib/bitvectors/BitvectorMultiplication.prf
+pvs/lib/bitvectors/BitvectorMultiplication.pvs
+pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.bin
+pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.prf
+pvs/lib/bitvectors/BitvectorMultiplicationWidenNarrow.pvs
+pvs/lib/bitvectors/BitvectorOneComplementDivision.bin
+pvs/lib/bitvectors/BitvectorOneComplementDivision.prf
+pvs/lib/bitvectors/BitvectorOneComplementDivision.pvs
+pvs/lib/bitvectors/BitvectorTwoComplementDivision.bin
+pvs/lib/bitvectors/BitvectorTwoComplementDivision.prf
+pvs/lib/bitvectors/BitvectorTwoComplementDivision.pvs
+pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.bin
+pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.prf
+pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.pvs
+pvs/lib/bitvectors/BitvectorUtil.bin
+pvs/lib/bitvectors/BitvectorUtil.prf
+pvs/lib/bitvectors/BitvectorUtil.pvs
+pvs/lib/bitvectors/DivisionUtil.bin
+pvs/lib/bitvectors/DivisionUtil.prf
+pvs/lib/bitvectors/DivisionUtil.pvs
 pvs/lib/bitvectors/bv_adder.bin
 pvs/lib/bitvectors/bv_adder.prf
 pvs/lib/bitvectors/bv_adder.pvs
@@ -668,13 +499,9 @@ pvs/lib/bitvectors/bv_arith_rules.pvs
 pvs/lib/bitvectors/bv_arithmetic.bin
 pvs/lib/bitvectors/bv_arithmetic.prf
 pvs/lib/bitvectors/bv_arithmetic.pvs
-pvs/lib/bitvectors/bv_bitwise.prf
-pvs/lib/bitvectors/bv_bitwise.pvs
 pvs/lib/bitvectors/bv_bitwise_rules.bin
 pvs/lib/bitvectors/bv_bitwise_rules.prf
 pvs/lib/bitvectors/bv_bitwise_rules.pvs
-pvs/lib/bitvectors/bv_caret.prf
-pvs/lib/bitvectors/bv_caret.pvs
 pvs/lib/bitvectors/bv_caret_bitwise.bin
 pvs/lib/bitvectors/bv_caret_bitwise.prf
 pvs/lib/bitvectors/bv_caret_bitwise.pvs
@@ -689,14 +516,10 @@ pvs/lib/bitvectors/bv_caret_concat_rules.prf
 pvs/lib/bitvectors/bv_caret_concat_rules.pvs
 pvs/lib/bitvectors/bv_caret_rules.bin
 pvs/lib/bitvectors/bv_caret_rules.prf
-pvs/lib/bitvectors/bv_caret_rules.prf~
 pvs/lib/bitvectors/bv_caret_rules.pvs
-pvs/lib/bitvectors/bv_cnv.pvs
 pvs/lib/bitvectors/bv_concat.bin
 pvs/lib/bitvectors/bv_concat.prf
 pvs/lib/bitvectors/bv_concat.pvs
-pvs/lib/bitvectors/bv_concat_def.prf
-pvs/lib/bitvectors/bv_concat_def.pvs
 pvs/lib/bitvectors/bv_concat_rules.bin
 pvs/lib/bitvectors/bv_concat_rules.prf
 pvs/lib/bitvectors/bv_concat_rules.pvs
@@ -714,8 +537,9 @@ pvs/lib/bitvectors/bv_fract.pvs
 pvs/lib/bitvectors/bv_int.bin
 pvs/lib/bitvectors/bv_int.prf
 pvs/lib/bitvectors/bv_int.pvs
-pvs/lib/bitvectors/bv_nat.prf
-pvs/lib/bitvectors/bv_nat.pvs
+pvs/lib/bitvectors/bv_mult_div_rem.bin
+pvs/lib/bitvectors/bv_mult_div_rem.prf
+pvs/lib/bitvectors/bv_mult_div_rem.pvs
 pvs/lib/bitvectors/bv_nat_rules.bin
 pvs/lib/bitvectors/bv_nat_rules.prf
 pvs/lib/bitvectors/bv_nat_rules.pvs
@@ -738,9 +562,6 @@ pvs/lib/bitvectors/bv_sum.pvs
 pvs/lib/bitvectors/div.bin
 pvs/lib/bitvectors/div.prf
 pvs/lib/bitvectors/div.pvs
-pvs/lib/bitvectors/empty_bv.pvs
-pvs/lib/bitvectors/exp2.prf
-pvs/lib/bitvectors/exp2.pvs
 pvs/lib/bitvectors/floor_div_props.bin
 pvs/lib/bitvectors/floor_div_props.prf
 pvs/lib/bitvectors/floor_div_props.pvs
@@ -750,64 +571,13 @@ pvs/lib/bitvectors/mod.pvs
 pvs/lib/bitvectors/mod_rules.bin
 pvs/lib/bitvectors/mod_rules.prf
 pvs/lib/bitvectors/mod_rules.pvs
-pvs/lib/bitvectors/orphaned-proofs.prf
 pvs/lib/bitvectors/sums.bin
 pvs/lib/bitvectors/sums.prf
 pvs/lib/bitvectors/sums.pvs
 pvs/lib/bitvectors/top.bin
 pvs/lib/bitvectors/top.pvs
 pvs/lib/character_adt.pvs
-pvs/lib/finite_sets/.cvsignore
 pvs/lib/finite_sets/.pvscontext
-pvs/lib/finite_sets/CVS/.cvsignore,t
-pvs/lib/finite_sets/CVS/Baserev
-pvs/lib/finite_sets/CVS/Entries
-pvs/lib/finite_sets/CVS/Repository
-pvs/lib/finite_sets/CVS/Root
-pvs/lib/finite_sets/CVS/Tag
-pvs/lib/finite_sets/CVS/card_def.prf,t
-pvs/lib/finite_sets/CVS/card_def.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets.prf,t
-pvs/lib/finite_sets/CVS/finite_sets.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_below.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_below.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_card_eq.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_card_eq.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_eq.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_eq.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_inductions.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_inductions.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_int.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_int.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_minmax.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_minmax.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_nat.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_nat.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_pred.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_pred.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_sum.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_sum.pvs,t
-pvs/lib/finite_sets/CVS/finite_sets_sum_real.prf,t
-pvs/lib/finite_sets/CVS/finite_sets_sum_real.pvs,t
-pvs/lib/finite_sets/CVS/func_composition.prf,t
-pvs/lib/finite_sets/CVS/func_composition.pvs,t
-pvs/lib/finite_sets/CVS/min_nat.prf,t
-pvs/lib/finite_sets/CVS/min_nat.pvs,t
-pvs/lib/finite_sets/CVS/nat_fun_props.prf,t
-pvs/lib/finite_sets/CVS/nat_fun_props.pvs,t
-pvs/lib/finite_sets/CVS/orphaned-proofs.prf,t
-pvs/lib/finite_sets/CVS/prelude_aux.prf,t
-pvs/lib/finite_sets/CVS/prelude_aux.pvs,t
-pvs/lib/finite_sets/CVS/top.prf,t
-pvs/lib/finite_sets/CVS/top.pvs,t
-pvs/lib/finite_sets/card_def.bin
-pvs/lib/finite_sets/card_def.prf
-pvs/lib/finite_sets/card_def.prf~
-pvs/lib/finite_sets/card_def.pvs
-pvs/lib/finite_sets/card_def.pvs.~1.1.2.2~
-pvs/lib/finite_sets/finite_sets.bin
-pvs/lib/finite_sets/finite_sets.prf
-pvs/lib/finite_sets/finite_sets.pvs
 pvs/lib/finite_sets/finite_sets_below.bin
 pvs/lib/finite_sets/finite_sets_below.prf
 pvs/lib/finite_sets/finite_sets_below.pvs
@@ -828,8 +598,6 @@ pvs/lib/finite_sets/finite_sets_minmax.prf
 pvs/lib/finite_sets/finite_sets_minmax.pvs
 pvs/lib/finite_sets/finite_sets_nat.bin
 pvs/lib/finite_sets/finite_sets_nat.prf
-pvs/lib/finite_sets/finite_sets_nat.prf.~1.1.2.1~
-pvs/lib/finite_sets/finite_sets_nat.prf~
 pvs/lib/finite_sets/finite_sets_nat.pvs
 pvs/lib/finite_sets/finite_sets_pred.bin
 pvs/lib/finite_sets/finite_sets_pred.prf
@@ -843,9 +611,6 @@ pvs/lib/finite_sets/finite_sets_sum_real.pvs
 pvs/lib/finite_sets/func_composition.bin
 pvs/lib/finite_sets/func_composition.prf
 pvs/lib/finite_sets/func_composition.pvs
-pvs/lib/finite_sets/nat_fun_props.bin
-pvs/lib/finite_sets/nat_fun_props.prf
-pvs/lib/finite_sets/nat_fun_props.pvs
 pvs/lib/finite_sets/orphaned-proofs.prf
 pvs/lib/finite_sets/prelude_aux.bin
 pvs/lib/finite_sets/prelude_aux.prf
@@ -862,6 +627,7 @@ pvs/lib/pvs-prover.help
 pvs/lib/pvs.bnf
 pvs/lib/pvs.grammar
 pvs/lib/pvs.help
+pvs/lib/strategies.lisp
 pvs/pvs
 pvs/pvs-tex.sub
 pvs/pvs.sty
@@ -869,25 +635,19 @@ pvs/wish/gray.xbm
 pvs/wish/pvs-support.tcl
 pvs/wish/sequent.xbm
 @dirrm pvs/wish
-@exec ${MKDIR} %D/pvs/lib/finite_sets/CVS/Base
-@dirrm pvs/lib/finite_sets/CVS/Base
-@dirrm pvs/lib/finite_sets/CVS
 @dirrm pvs/lib/finite_sets
-@dirrm pvs/lib/bitvectors/CVS
 @dirrm pvs/lib/bitvectors
 @dirrm pvs/lib
 @dirrm pvs/emacs/xemacs21
-@dirrm pvs/emacs/xemacs20
-@exec ${MKDIR} %D/pvs/emacs/xemacs19
-@dirrm pvs/emacs/xemacs19
 @dirrm pvs/emacs/emacs20
 @dirrm pvs/emacs/emacs19
 @dirrm pvs/emacs/emacs-src/ilisp
 @dirrm pvs/emacs/emacs-src
 @dirrm pvs/emacs
+@dirrm pvs/doc/release-notes
+@dirrm pvs/doc
 @dirrm pvs/bin/ix86-redhat5/runtime
 @dirrm pvs/bin/ix86-redhat5
 @dirrm pvs/bin
-@exec ${MKDIR} %D/pvs/Examples
 @dirrm pvs/Examples
 @dirrm pvs
diff --git a/devel/pvs/distinfo b/devel/pvs/distinfo
index 31a8d6c92fb..6a10dfaf34a 100644
--- a/devel/pvs/distinfo
+++ b/devel/pvs/distinfo
@@ -1,11 +1,11 @@
-$NetBSD: distinfo,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+$NetBSD: distinfo,v 1.2 2002/12/20 21:37:38 jschauma Exp $
 
-SHA1 (pvs-3.0-redhat5.tgz) = 62996ae43bf8c61a99d324bf92598dbcf7c9e527
-Size (pvs-3.0-redhat5.tgz) = 12252501 bytes
-SHA1 (pvs-3.0-system.tgz) = d019ab1c52c6f53d6fb14088dba9eae8550159d4
-Size (pvs-3.0-system.tgz) = 1343169 bytes
-SHA1 (pvs-3.0-emacs19.tgz) = 191a63c304fa4244cc885fad39826eaa2106744b
-Size (pvs-3.0-emacs19.tgz) = 352394 bytes
-SHA1 (pvs-3.0-libraries.tgz) = cf67df788384be6c94593a3b4f3aa901e20cba9c
-Size (pvs-3.0-libraries.tgz) = 1104488 bytes
-SHA1 (patch-aa) = c2da82352e0adc0f4d27ff895136baf1b1430437
+SHA1 (pvs-3.0-redhat5.tgz) = d075d99f566cb638d5ca981a0160b27b8c7008f5
+Size (pvs-3.0-redhat5.tgz) = 12626606 bytes
+SHA1 (pvs-3.0-system.tgz) = ac2502f0aace86f0c44110bee5123fee875a2bee
+Size (pvs-3.0-system.tgz) = 1291673 bytes
+SHA1 (pvs-3.0-emacs19.tgz) = d4aeb58a995257e96e16350fc6ad52c963dc7308
+Size (pvs-3.0-emacs19.tgz) = 360087 bytes
+SHA1 (pvs-3.0-libraries.tgz) = f5989c0c0b92a24fb0740c45b70f0961d026c679
+Size (pvs-3.0-libraries.tgz) = 1459536 bytes
+SHA1 (patch-aa) = dc2e51855dae92e6b5e8fb1c97fe34186893e1f2
diff --git a/devel/pvs/patches/patch-aa b/devel/pvs/patches/patch-aa
index 78489eabebc..ceff428c0f9 100644
--- a/devel/pvs/patches/patch-aa
+++ b/devel/pvs/patches/patch-aa
@@ -1,13 +1,13 @@
-$NetBSD: patch-aa,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+$NetBSD: patch-aa,v 1.2 2002/12/20 21:37:40 jschauma Exp $
 
---- pvs.orig	Fri Jul 19 05:57:05 2002
-+++ pvs	Tue Sep 24 12:43:19 2002
+--- pvs.orig	Thu Dec 19 22:38:25 2002
++++ pvs	Thu Dec 19 22:42:32 2002
 @@ -46,7 +46,7 @@
  
  # PVSPATH should be set after installation by <PVS>/bin/relocate or by hand
  # to the location of the PVS installation
--PVSPATH=/homes/owre/pvs3.0
-+PVSPATH=@PREFIX@/pvs
+-PVSPATH=/project/pvs/pvs3.0
++PVSPATH=@PREFIX@/pvs/
  
  #-------------------------------------------------
  # Nothing below this line should need modification
@@ -16,27 +16,28 @@ $NetBSD: patch-aa,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
  	 fi
  	 PVSARCH=sun4;;
 +  NetBSD) # pretend to be a redhat linux system
-+  	opsys=redhat
++	opsys=redhat
 +	majvers=5
 +	othervers=4
 +	PVSARCH=ix86;;
    Linux) # If Linux, we need to determine the Redhat version to use.
  	 opsys=redhat
  	 if [ ! $majvers ]; then
-@@ -228,8 +233,14 @@
+@@ -228,8 +233,15 @@
  PVSIMAGE="$PVSLISP"
  
  export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
 -export PVSARCH PVSIMAGE PVSPATH PATH PVSLISP PVSVERBOSE PVSTIMEOUT
 -export PVSPATCHLEVEL PVSMINUSQ PVSFORCEDP PVSDEFAULTDP
 +export PVSARCH PVSIMAGE PVSPATH PATH PVSLISP PVSVERBOSE
-+export PVSPATCHLEVEL PVSMINUSQ PVSFORCEDP 
++export PVSPATCHLEVEL PVSMINUSQ PVSFORCEDP
 +if [ "$PVSTIMEOUT" ]; then
 +	export PVSTIMEOUT
 +fi
 +if [ "$PVSDEFAULTDP" ]; then
 +	export PVSDEFAULTDP;
 +fi
++
  
  pvsemacsinit="-load $PVSPATH/emacs/go-pvs.el $loadafter"