Initial import of devel/pvs into pkgsrc:

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.
For more details, please see http://pvs.csl.sri.com/ and
http://pvs.csl.sri.com/overview.html

This package was tested on NetBSD-1.6-i386 and Linux-i386, it might work
(but might need some modification) on NetBSD-1.6-sparc and SunOS as well.

For i386, NetBSD 1.6 is required -- on 1.5.x versions, it will (seemingly)
install fine but not work correctly in various instances.

6 files changed, 1017 insertions, 0 deletions

diff --git a/devel/pvs/DESCR b/devel/pvs/DESCR
new file mode 100644
index 00000000000..9c9b26656f3
--- /dev/null
+++ b/devel/pvs/DESCR
@@ -0,0 +1,4 @@
+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.
diff --git a/devel/pvs/Makefile b/devel/pvs/Makefile
new file mode 100644
index 00000000000..18a22db89bb
--- /dev/null
+++ b/devel/pvs/Makefile
@@ -0,0 +1,60 @@
+# $NetBSD: Makefile,v 1.1.1.1 2002/09/24 17:57:24 jschauma Exp $
+#
+
+DISTNAME=		pvs-${VERSION}
+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}/
+EXTRACT_SUFX=		.tgz
+DISTFILES=		${DISTNAME}-${MAINFILEEXT}${EXTRACT_SUFX} \
+			pvs-3.0-system${EXTRACT_SUFX} \
+			pvs-3.0-emacs19${EXTRACT_SUFX} \
+			pvs-3.0-libraries${EXTRACT_SUFX}
+
+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
+
+LICENSE=        	pvs-license
+# not quite sure about this, but to be on the safe side:
+RESTRICTED=     	"Redistribution not permitted - see ${HOMEPAGE}license.html"
+NO_SRC_ON_CDROM=	${RESTRICTED}
+NO_SRC_ON_FTP=  	${RESTRICTED}
+NO_BIN_ON_CDROM=	${RESTRICTED}
+NO_BIN_ON_FTP=  	${RESTRICTED}
+
+ONLY_FOR_PLATFORM=	NetBSD-1.[6-9]*-* Linux-*-* SunOS-*-*
+
+.include "../../mk/bsd.prefs.mk"
+
+.if (${OPSYS} == "NetBSD" && ${MACHINE_ARCH} == "sparc") || ${OPSYS} != "SunOS"
+MAINFILEEXT=		redhat5
+.else
+MAINFILEEXT=		solaris
+.endif
+
+.if ${OPSYS} == "NetBSD"
+MESSAGE_SRC=		${FILESDIR}/MESSAGE
+.endif
+
+post-patch:
+	${SED} -e "s|@PREFIX@|${PREFIX}|" ${WRKSRC}/pvs > \
+		${WRKSRC}/pvs.tmp
+	${MV} ${WRKSRC}/pvs.tmp ${WRKSRC}/pvs
+	${RM} ${WRKSRC}/pvs.orig
+
+do-install:
+	${INSTALL_SCRIPT} ${WRKSRC}/pvs ${PREFIX}/bin/pvs
+	${INSTALL_PROGRAM_DIR} ${PREFIX}/pvs
+	cd ${WRKSRC} && ${PAX} -s ,^./[.].*,, -rw . ${PREFIX}/pvs
+	${CHMOD} 755 ${PREFIX}/pvs/pvs
+
+.include "../../mk/bsd.pkg.mk"
diff --git a/devel/pvs/PLIST b/devel/pvs/PLIST
new file mode 100644
index 00000000000..e8244fc1efa
--- /dev/null
+++ b/devel/pvs/PLIST
@@ -0,0 +1,893 @@
+@comment $NetBSD: PLIST,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+bin/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/mu.so
+pvs/bin/ix86-redhat5/runtime/pvs-allegro6.0
+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/emacs/README
+pvs/emacs/emacs-src/ilisp/comint-ipc.el
+pvs/emacs/emacs-src/ilisp/completer.el
+pvs/emacs/emacs-src/ilisp/completer.new.el
+pvs/emacs/emacs-src/ilisp/completer.no-fun.el
+pvs/emacs/emacs-src/ilisp/ilcompat.el
+pvs/emacs/emacs-src/ilisp/ilfsf18.el
+pvs/emacs/emacs-src/ilisp/ilfsf19.el
+pvs/emacs/emacs-src/ilisp/ilfsf20.el
+pvs/emacs/emacs-src/ilisp/ilisp-acl.el
+pvs/emacs/emacs-src/ilisp/ilisp-aut.el
+pvs/emacs/emacs-src/ilisp/ilisp-bat.el
+pvs/emacs/emacs-src/ilisp/ilisp-chs.el
+pvs/emacs/emacs-src/ilisp/ilisp-cl.el
+pvs/emacs/emacs-src/ilisp/ilisp-cmp.el
+pvs/emacs/emacs-src/ilisp/ilisp-cmt.el
+pvs/emacs/emacs-src/ilisp/ilisp-def.el
+pvs/emacs/emacs-src/ilisp/ilisp-dia.el
+pvs/emacs/emacs-src/ilisp/ilisp-doc.el
+pvs/emacs/emacs-src/ilisp/ilisp-el.el
+pvs/emacs/emacs-src/ilisp/ilisp-ext.el
+pvs/emacs/emacs-src/ilisp/ilisp-hi.el
+pvs/emacs/emacs-src/ilisp/ilisp-hnd.el
+pvs/emacs/emacs-src/ilisp/ilisp-ind.el
+pvs/emacs/emacs-src/ilisp/ilisp-inp.el
+pvs/emacs/emacs-src/ilisp/ilisp-key.el
+pvs/emacs/emacs-src/ilisp/ilisp-kil.el
+pvs/emacs/emacs-src/ilisp/ilisp-low.el
+pvs/emacs/emacs-src/ilisp/ilisp-menu.el
+pvs/emacs/emacs-src/ilisp/ilisp-mnb.el
+pvs/emacs/emacs-src/ilisp/ilisp-mod.el
+pvs/emacs/emacs-src/ilisp/ilisp-mov.el
+pvs/emacs/emacs-src/ilisp/ilisp-out.el
+pvs/emacs/emacs-src/ilisp/ilisp-prc.el
+pvs/emacs/emacs-src/ilisp/ilisp-prn.el
+pvs/emacs/emacs-src/ilisp/ilisp-rng.el
+pvs/emacs/emacs-src/ilisp/ilisp-snd.el
+pvs/emacs/emacs-src/ilisp/ilisp-src.el
+pvs/emacs/emacs-src/ilisp/ilisp-sym.el
+pvs/emacs/emacs-src/ilisp/ilisp-utl.el
+pvs/emacs/emacs-src/ilisp/ilisp-val.el
+pvs/emacs/emacs-src/ilisp/ilisp-xfr.el
+pvs/emacs/emacs-src/ilisp/ilisp-xls.el
+pvs/emacs/emacs-src/ilisp/ilisp.el
+pvs/emacs/emacs-src/ilisp/illuc19.el
+pvs/emacs/emacs-src/ilisp/ilxemacs.el
+pvs/emacs/emacs-src/pvs-abbreviations.el
+pvs/emacs/emacs-src/pvs-browser.el
+pvs/emacs/emacs-src/pvs-byte-compile.el
+pvs/emacs/emacs-src/pvs-cmds.el
+pvs/emacs/emacs-src/pvs-eval.el
+pvs/emacs/emacs-src/pvs-file-list.el
+pvs/emacs/emacs-src/pvs-ilisp.el
+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-print.el
+pvs/emacs/emacs-src/pvs-prover-helps.el
+pvs/emacs/emacs-src/pvs-prover.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/tcl.el
+pvs/emacs/emacs19/Makefile
+pvs/emacs/emacs19/comint-ipc.el
+pvs/emacs/emacs19/comint-ipc.elc
+pvs/emacs/emacs19/completer.el
+pvs/emacs/emacs19/completer.elc
+pvs/emacs/emacs19/completer.new.el
+pvs/emacs/emacs19/completer.no-fun.el
+pvs/emacs/emacs19/ilcompat.el
+pvs/emacs/emacs19/ilfsf18.el
+pvs/emacs/emacs19/ilfsf19.el
+pvs/emacs/emacs19/ilfsf20.el
+pvs/emacs/emacs19/ilisp-acl.el
+pvs/emacs/emacs19/ilisp-acl.elc
+pvs/emacs/emacs19/ilisp-aut.el
+pvs/emacs/emacs19/ilisp-aut.elc
+pvs/emacs/emacs19/ilisp-bat.el
+pvs/emacs/emacs19/ilisp-chs.el
+pvs/emacs/emacs19/ilisp-cl.el
+pvs/emacs/emacs19/ilisp-cl.elc
+pvs/emacs/emacs19/ilisp-cmp.el
+pvs/emacs/emacs19/ilisp-cmp.elc
+pvs/emacs/emacs19/ilisp-cmt.el
+pvs/emacs/emacs19/ilisp-cmt.elc
+pvs/emacs/emacs19/ilisp-def.el
+pvs/emacs/emacs19/ilisp-def.elc
+pvs/emacs/emacs19/ilisp-dia.el
+pvs/emacs/emacs19/ilisp-dia.elc
+pvs/emacs/emacs19/ilisp-doc.el
+pvs/emacs/emacs19/ilisp-doc.elc
+pvs/emacs/emacs19/ilisp-el.el
+pvs/emacs/emacs19/ilisp-el.elc
+pvs/emacs/emacs19/ilisp-ext.el
+pvs/emacs/emacs19/ilisp-ext.elc
+pvs/emacs/emacs19/ilisp-hi.el
+pvs/emacs/emacs19/ilisp-hi.elc
+pvs/emacs/emacs19/ilisp-hnd.el
+pvs/emacs/emacs19/ilisp-hnd.elc
+pvs/emacs/emacs19/ilisp-ind.el
+pvs/emacs/emacs19/ilisp-ind.elc
+pvs/emacs/emacs19/ilisp-inp.el
+pvs/emacs/emacs19/ilisp-inp.elc
+pvs/emacs/emacs19/ilisp-key.el
+pvs/emacs/emacs19/ilisp-key.elc
+pvs/emacs/emacs19/ilisp-kil.el
+pvs/emacs/emacs19/ilisp-kil.elc
+pvs/emacs/emacs19/ilisp-low.el
+pvs/emacs/emacs19/ilisp-low.elc
+pvs/emacs/emacs19/ilisp-menu.el
+pvs/emacs/emacs19/ilisp-mnb.el
+pvs/emacs/emacs19/ilisp-mod.el
+pvs/emacs/emacs19/ilisp-mod.elc
+pvs/emacs/emacs19/ilisp-mov.el
+pvs/emacs/emacs19/ilisp-mov.elc
+pvs/emacs/emacs19/ilisp-out.el
+pvs/emacs/emacs19/ilisp-out.elc
+pvs/emacs/emacs19/ilisp-prc.el
+pvs/emacs/emacs19/ilisp-prc.elc
+pvs/emacs/emacs19/ilisp-prn.el
+pvs/emacs/emacs19/ilisp-prn.elc
+pvs/emacs/emacs19/ilisp-rng.el
+pvs/emacs/emacs19/ilisp-rng.elc
+pvs/emacs/emacs19/ilisp-snd.el
+pvs/emacs/emacs19/ilisp-snd.elc
+pvs/emacs/emacs19/ilisp-src.el
+pvs/emacs/emacs19/ilisp-sym.el
+pvs/emacs/emacs19/ilisp-sym.elc
+pvs/emacs/emacs19/ilisp-utl.el
+pvs/emacs/emacs19/ilisp-utl.elc
+pvs/emacs/emacs19/ilisp-val.el
+pvs/emacs/emacs19/ilisp-val.elc
+pvs/emacs/emacs19/ilisp-xfr.el
+pvs/emacs/emacs19/ilisp-xfr.elc
+pvs/emacs/emacs19/ilisp-xls.el
+pvs/emacs/emacs19/ilisp.el
+pvs/emacs/emacs19/illuc19.el
+pvs/emacs/emacs19/ilxemacs.el
+pvs/emacs/emacs19/pvs-abbreviations.el
+pvs/emacs/emacs19/pvs-abbreviations.elc
+pvs/emacs/emacs19/pvs-browser.el
+pvs/emacs/emacs19/pvs-browser.elc
+pvs/emacs/emacs19/pvs-byte-compile.el
+pvs/emacs/emacs19/pvs-cmds.el
+pvs/emacs/emacs19/pvs-cmds.elc
+pvs/emacs/emacs19/pvs-eval.el
+pvs/emacs/emacs19/pvs-eval.elc
+pvs/emacs/emacs19/pvs-file-list.el
+pvs/emacs/emacs19/pvs-file-list.elc
+pvs/emacs/emacs19/pvs-ilisp.el
+pvs/emacs/emacs19/pvs-load.el
+pvs/emacs/emacs19/pvs-load.elc
+pvs/emacs/emacs19/pvs-macros.el
+pvs/emacs/emacs19/pvs-macros.elc
+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-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-tcl.el
+pvs/emacs/emacs19/pvs-tcl.elc
+pvs/emacs/emacs19/pvs-utils.el
+pvs/emacs/emacs19/pvs-utils.elc
+pvs/emacs/emacs19/pvs-view.el
+pvs/emacs/emacs19/pvs-view.elc
+pvs/emacs/emacs19/tcl.el
+pvs/emacs/emacs19/tcl.elc
+pvs/emacs/emacs20/comint-ipc.el
+pvs/emacs/emacs20/comint-ipc.elc
+pvs/emacs/emacs20/completer.el
+pvs/emacs/emacs20/completer.elc
+pvs/emacs/emacs20/completer.new.el
+pvs/emacs/emacs20/completer.no-fun.el
+pvs/emacs/emacs20/ilcompat.el
+pvs/emacs/emacs20/ilfsf18.el
+pvs/emacs/emacs20/ilfsf19.el
+pvs/emacs/emacs20/ilfsf20.el
+pvs/emacs/emacs20/ilisp-acl.el
+pvs/emacs/emacs20/ilisp-acl.elc
+pvs/emacs/emacs20/ilisp-aut.el
+pvs/emacs/emacs20/ilisp-aut.elc
+pvs/emacs/emacs20/ilisp-bat.el
+pvs/emacs/emacs20/ilisp-chs.el
+pvs/emacs/emacs20/ilisp-cl.el
+pvs/emacs/emacs20/ilisp-cl.elc
+pvs/emacs/emacs20/ilisp-cmp.el
+pvs/emacs/emacs20/ilisp-cmp.elc
+pvs/emacs/emacs20/ilisp-cmt.el
+pvs/emacs/emacs20/ilisp-cmt.elc
+pvs/emacs/emacs20/ilisp-def.el
+pvs/emacs/emacs20/ilisp-def.elc
+pvs/emacs/emacs20/ilisp-dia.el
+pvs/emacs/emacs20/ilisp-dia.elc
+pvs/emacs/emacs20/ilisp-doc.el
+pvs/emacs/emacs20/ilisp-doc.elc
+pvs/emacs/emacs20/ilisp-el.el
+pvs/emacs/emacs20/ilisp-el.elc
+pvs/emacs/emacs20/ilisp-ext.el
+pvs/emacs/emacs20/ilisp-ext.elc
+pvs/emacs/emacs20/ilisp-hi.el
+pvs/emacs/emacs20/ilisp-hi.elc
+pvs/emacs/emacs20/ilisp-hnd.el
+pvs/emacs/emacs20/ilisp-hnd.elc
+pvs/emacs/emacs20/ilisp-ind.el
+pvs/emacs/emacs20/ilisp-ind.elc
+pvs/emacs/emacs20/ilisp-inp.el
+pvs/emacs/emacs20/ilisp-inp.elc
+pvs/emacs/emacs20/ilisp-key.el
+pvs/emacs/emacs20/ilisp-key.elc
+pvs/emacs/emacs20/ilisp-kil.el
+pvs/emacs/emacs20/ilisp-kil.elc
+pvs/emacs/emacs20/ilisp-low.el
+pvs/emacs/emacs20/ilisp-low.elc
+pvs/emacs/emacs20/ilisp-menu.el
+pvs/emacs/emacs20/ilisp-mnb.el
+pvs/emacs/emacs20/ilisp-mod.el
+pvs/emacs/emacs20/ilisp-mod.elc
+pvs/emacs/emacs20/ilisp-mov.el
+pvs/emacs/emacs20/ilisp-mov.elc
+pvs/emacs/emacs20/ilisp-out.el
+pvs/emacs/emacs20/ilisp-out.elc
+pvs/emacs/emacs20/ilisp-prc.el
+pvs/emacs/emacs20/ilisp-prc.elc
+pvs/emacs/emacs20/ilisp-prn.el
+pvs/emacs/emacs20/ilisp-prn.elc
+pvs/emacs/emacs20/ilisp-rng.el
+pvs/emacs/emacs20/ilisp-rng.elc
+pvs/emacs/emacs20/ilisp-snd.el
+pvs/emacs/emacs20/ilisp-snd.elc
+pvs/emacs/emacs20/ilisp-src.el
+pvs/emacs/emacs20/ilisp-sym.el
+pvs/emacs/emacs20/ilisp-sym.elc
+pvs/emacs/emacs20/ilisp-utl.el
+pvs/emacs/emacs20/ilisp-utl.elc
+pvs/emacs/emacs20/ilisp-val.el
+pvs/emacs/emacs20/ilisp-val.elc
+pvs/emacs/emacs20/ilisp-xfr.el
+pvs/emacs/emacs20/ilisp-xfr.elc
+pvs/emacs/emacs20/ilisp-xls.el
+pvs/emacs/emacs20/ilisp.el
+pvs/emacs/emacs20/illuc19.el
+pvs/emacs/emacs20/ilxemacs.el
+pvs/emacs/emacs20/pvs-abbreviations.el
+pvs/emacs/emacs20/pvs-abbreviations.elc
+pvs/emacs/emacs20/pvs-browser.el
+pvs/emacs/emacs20/pvs-browser.elc
+pvs/emacs/emacs20/pvs-byte-compile.el
+pvs/emacs/emacs20/pvs-cmds.el
+pvs/emacs/emacs20/pvs-cmds.elc
+pvs/emacs/emacs20/pvs-eval.el
+pvs/emacs/emacs20/pvs-eval.elc
+pvs/emacs/emacs20/pvs-file-list.el
+pvs/emacs/emacs20/pvs-file-list.elc
+pvs/emacs/emacs20/pvs-ilisp.el
+pvs/emacs/emacs20/pvs-load.el
+pvs/emacs/emacs20/pvs-load.elc
+pvs/emacs/emacs20/pvs-macros.el
+pvs/emacs/emacs20/pvs-macros.elc
+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-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-tcl.el
+pvs/emacs/emacs20/pvs-tcl.elc
+pvs/emacs/emacs20/pvs-utils.el
+pvs/emacs/emacs20/pvs-utils.elc
+pvs/emacs/emacs20/pvs-view.el
+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
+pvs/emacs/xemacs21/completer.elc
+pvs/emacs/xemacs21/completer.new.el
+pvs/emacs/xemacs21/completer.no-fun.el
+pvs/emacs/xemacs21/ilcompat.el
+pvs/emacs/xemacs21/ilfsf18.el
+pvs/emacs/xemacs21/ilfsf19.el
+pvs/emacs/xemacs21/ilfsf20.el
+pvs/emacs/xemacs21/ilisp-acl.el
+pvs/emacs/xemacs21/ilisp-acl.elc
+pvs/emacs/xemacs21/ilisp-aut.el
+pvs/emacs/xemacs21/ilisp-aut.elc
+pvs/emacs/xemacs21/ilisp-bat.el
+pvs/emacs/xemacs21/ilisp-chs.el
+pvs/emacs/xemacs21/ilisp-cl.el
+pvs/emacs/xemacs21/ilisp-cl.elc
+pvs/emacs/xemacs21/ilisp-cmp.el
+pvs/emacs/xemacs21/ilisp-cmp.elc
+pvs/emacs/xemacs21/ilisp-cmt.el
+pvs/emacs/xemacs21/ilisp-cmt.elc
+pvs/emacs/xemacs21/ilisp-def.el
+pvs/emacs/xemacs21/ilisp-def.elc
+pvs/emacs/xemacs21/ilisp-dia.el
+pvs/emacs/xemacs21/ilisp-dia.elc
+pvs/emacs/xemacs21/ilisp-doc.el
+pvs/emacs/xemacs21/ilisp-doc.elc
+pvs/emacs/xemacs21/ilisp-el.el
+pvs/emacs/xemacs21/ilisp-el.elc
+pvs/emacs/xemacs21/ilisp-ext.el
+pvs/emacs/xemacs21/ilisp-ext.elc
+pvs/emacs/xemacs21/ilisp-hi.el
+pvs/emacs/xemacs21/ilisp-hi.elc
+pvs/emacs/xemacs21/ilisp-hnd.el
+pvs/emacs/xemacs21/ilisp-hnd.elc
+pvs/emacs/xemacs21/ilisp-ind.el
+pvs/emacs/xemacs21/ilisp-ind.elc
+pvs/emacs/xemacs21/ilisp-inp.el
+pvs/emacs/xemacs21/ilisp-inp.elc
+pvs/emacs/xemacs21/ilisp-key.el
+pvs/emacs/xemacs21/ilisp-key.elc
+pvs/emacs/xemacs21/ilisp-kil.el
+pvs/emacs/xemacs21/ilisp-kil.elc
+pvs/emacs/xemacs21/ilisp-low.el
+pvs/emacs/xemacs21/ilisp-low.elc
+pvs/emacs/xemacs21/ilisp-menu.el
+pvs/emacs/xemacs21/ilisp-mnb.el
+pvs/emacs/xemacs21/ilisp-mod.el
+pvs/emacs/xemacs21/ilisp-mod.elc
+pvs/emacs/xemacs21/ilisp-mov.el
+pvs/emacs/xemacs21/ilisp-mov.elc
+pvs/emacs/xemacs21/ilisp-out.el
+pvs/emacs/xemacs21/ilisp-out.elc
+pvs/emacs/xemacs21/ilisp-prc.el
+pvs/emacs/xemacs21/ilisp-prc.elc
+pvs/emacs/xemacs21/ilisp-prn.el
+pvs/emacs/xemacs21/ilisp-prn.elc
+pvs/emacs/xemacs21/ilisp-rng.el
+pvs/emacs/xemacs21/ilisp-rng.elc
+pvs/emacs/xemacs21/ilisp-snd.el
+pvs/emacs/xemacs21/ilisp-snd.elc
+pvs/emacs/xemacs21/ilisp-src.el
+pvs/emacs/xemacs21/ilisp-sym.el
+pvs/emacs/xemacs21/ilisp-sym.elc
+pvs/emacs/xemacs21/ilisp-utl.el
+pvs/emacs/xemacs21/ilisp-utl.elc
+pvs/emacs/xemacs21/ilisp-val.el
+pvs/emacs/xemacs21/ilisp-val.elc
+pvs/emacs/xemacs21/ilisp-xfr.el
+pvs/emacs/xemacs21/ilisp-xfr.elc
+pvs/emacs/xemacs21/ilisp-xls.el
+pvs/emacs/xemacs21/ilisp.el
+pvs/emacs/xemacs21/illuc19.el
+pvs/emacs/xemacs21/ilxemacs.el
+pvs/emacs/xemacs21/pvs-abbreviations.el
+pvs/emacs/xemacs21/pvs-abbreviations.elc
+pvs/emacs/xemacs21/pvs-browser.el
+pvs/emacs/xemacs21/pvs-browser.elc
+pvs/emacs/xemacs21/pvs-byte-compile.el
+pvs/emacs/xemacs21/pvs-cmds.el
+pvs/emacs/xemacs21/pvs-cmds.elc
+pvs/emacs/xemacs21/pvs-eval.el
+pvs/emacs/xemacs21/pvs-eval.elc
+pvs/emacs/xemacs21/pvs-file-list.el
+pvs/emacs/xemacs21/pvs-file-list.elc
+pvs/emacs/xemacs21/pvs-ilisp.el
+pvs/emacs/xemacs21/pvs-load.el
+pvs/emacs/xemacs21/pvs-load.elc
+pvs/emacs/xemacs21/pvs-macros.el
+pvs/emacs/xemacs21/pvs-macros.elc
+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-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-tcl.el
+pvs/emacs/xemacs21/pvs-tcl.elc
+pvs/emacs/xemacs21/pvs-utils.el
+pvs/emacs/xemacs21/pvs-utils.elc
+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/bv_adder.bin
+pvs/lib/bitvectors/bv_adder.prf
+pvs/lib/bitvectors/bv_adder.pvs
+pvs/lib/bitvectors/bv_arith_caret.bin
+pvs/lib/bitvectors/bv_arith_caret.prf
+pvs/lib/bitvectors/bv_arith_caret.pvs
+pvs/lib/bitvectors/bv_arith_caret_concat_rules.bin
+pvs/lib/bitvectors/bv_arith_caret_concat_rules.prf
+pvs/lib/bitvectors/bv_arith_caret_concat_rules.pvs
+pvs/lib/bitvectors/bv_arith_caret_rules.bin
+pvs/lib/bitvectors/bv_arith_caret_rules.prf
+pvs/lib/bitvectors/bv_arith_caret_rules.pvs
+pvs/lib/bitvectors/bv_arith_concat.bin
+pvs/lib/bitvectors/bv_arith_concat.prf
+pvs/lib/bitvectors/bv_arith_concat.pvs
+pvs/lib/bitvectors/bv_arith_extend.bin
+pvs/lib/bitvectors/bv_arith_extend.prf
+pvs/lib/bitvectors/bv_arith_extend.pvs
+pvs/lib/bitvectors/bv_arith_int_caret.bin
+pvs/lib/bitvectors/bv_arith_int_caret.prf
+pvs/lib/bitvectors/bv_arith_int_caret.pvs
+pvs/lib/bitvectors/bv_arith_int_concat.bin
+pvs/lib/bitvectors/bv_arith_int_concat.prf
+pvs/lib/bitvectors/bv_arith_int_concat.pvs
+pvs/lib/bitvectors/bv_arith_int_rules.bin
+pvs/lib/bitvectors/bv_arith_int_rules.prf
+pvs/lib/bitvectors/bv_arith_int_rules.pvs
+pvs/lib/bitvectors/bv_arith_minus_rules.bin
+pvs/lib/bitvectors/bv_arith_minus_rules.prf
+pvs/lib/bitvectors/bv_arith_minus_rules.pvs
+pvs/lib/bitvectors/bv_arith_nat.bin
+pvs/lib/bitvectors/bv_arith_nat.prf
+pvs/lib/bitvectors/bv_arith_nat.pvs
+pvs/lib/bitvectors/bv_arith_nat_caret_rules.bin
+pvs/lib/bitvectors/bv_arith_nat_caret_rules.prf
+pvs/lib/bitvectors/bv_arith_nat_caret_rules.pvs
+pvs/lib/bitvectors/bv_arith_nat_rules.bin
+pvs/lib/bitvectors/bv_arith_nat_rules.prf
+pvs/lib/bitvectors/bv_arith_nat_rules.pvs
+pvs/lib/bitvectors/bv_arith_rules.bin
+pvs/lib/bitvectors/bv_arith_rules.prf
+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
+pvs/lib/bitvectors/bv_caret_bitwise_rules.bin
+pvs/lib/bitvectors/bv_caret_bitwise_rules.prf
+pvs/lib/bitvectors/bv_caret_bitwise_rules.pvs
+pvs/lib/bitvectors/bv_caret_concat.bin
+pvs/lib/bitvectors/bv_caret_concat.prf
+pvs/lib/bitvectors/bv_caret_concat.pvs
+pvs/lib/bitvectors/bv_caret_concat_rules.bin
+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
+pvs/lib/bitvectors/bv_constants.bin
+pvs/lib/bitvectors/bv_constants.prf
+pvs/lib/bitvectors/bv_constants.pvs
+pvs/lib/bitvectors/bv_core.bin
+pvs/lib/bitvectors/bv_core.pvs
+pvs/lib/bitvectors/bv_extend.bin
+pvs/lib/bitvectors/bv_extend.prf
+pvs/lib/bitvectors/bv_extend.pvs
+pvs/lib/bitvectors/bv_fract.bin
+pvs/lib/bitvectors/bv_fract.prf
+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_nat_rules.bin
+pvs/lib/bitvectors/bv_nat_rules.prf
+pvs/lib/bitvectors/bv_nat_rules.pvs
+pvs/lib/bitvectors/bv_notes.bin
+pvs/lib/bitvectors/bv_notes.pvs
+pvs/lib/bitvectors/bv_overflow.bin
+pvs/lib/bitvectors/bv_overflow.prf
+pvs/lib/bitvectors/bv_overflow.pvs
+pvs/lib/bitvectors/bv_rotate.bin
+pvs/lib/bitvectors/bv_rotate.prf
+pvs/lib/bitvectors/bv_rotate.pvs
+pvs/lib/bitvectors/bv_rules.bin
+pvs/lib/bitvectors/bv_rules.pvs
+pvs/lib/bitvectors/bv_shift.bin
+pvs/lib/bitvectors/bv_shift.prf
+pvs/lib/bitvectors/bv_shift.pvs
+pvs/lib/bitvectors/bv_sum.bin
+pvs/lib/bitvectors/bv_sum.prf
+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
+pvs/lib/bitvectors/mod.bin
+pvs/lib/bitvectors/mod.prf
+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
+pvs/lib/finite_sets/finite_sets_card_eq.bin
+pvs/lib/finite_sets/finite_sets_card_eq.prf
+pvs/lib/finite_sets/finite_sets_card_eq.pvs
+pvs/lib/finite_sets/finite_sets_eq.bin
+pvs/lib/finite_sets/finite_sets_eq.prf
+pvs/lib/finite_sets/finite_sets_eq.pvs
+pvs/lib/finite_sets/finite_sets_inductions.bin
+pvs/lib/finite_sets/finite_sets_inductions.prf
+pvs/lib/finite_sets/finite_sets_inductions.pvs
+pvs/lib/finite_sets/finite_sets_int.bin
+pvs/lib/finite_sets/finite_sets_int.prf
+pvs/lib/finite_sets/finite_sets_int.pvs
+pvs/lib/finite_sets/finite_sets_minmax.bin
+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
+pvs/lib/finite_sets/finite_sets_pred.pvs
+pvs/lib/finite_sets/finite_sets_sum.bin
+pvs/lib/finite_sets/finite_sets_sum.prf
+pvs/lib/finite_sets/finite_sets_sum.pvs
+pvs/lib/finite_sets/finite_sets_sum_real.bin
+pvs/lib/finite_sets/finite_sets_sum_real.prf
+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
+pvs/lib/finite_sets/prelude_aux.pvs
+pvs/lib/finite_sets/top.bin
+pvs/lib/finite_sets/top.prf
+pvs/lib/finite_sets/top.pvs
+pvs/lib/list_adt.pvs
+pvs/lib/ordstruct_adt.pvs
+pvs/lib/prelude.prf
+pvs/lib/prelude.pvs
+pvs/lib/pvs-language.help
+pvs/lib/pvs-prover.help
+pvs/lib/pvs.bnf
+pvs/lib/pvs.grammar
+pvs/lib/pvs.help
+pvs/pvs
+pvs/pvs-tex.sub
+pvs/pvs.sty
+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/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
new file mode 100644
index 00000000000..31a8d6c92fb
--- /dev/null
+++ b/devel/pvs/distinfo
@@ -0,0 +1,11 @@
+$NetBSD: distinfo,v 1.1.1.1 2002/09/24 17:57:25 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
diff --git a/devel/pvs/files/MESSAGE b/devel/pvs/files/MESSAGE
new file mode 100644
index 00000000000..cbbf4e4a5eb
--- /dev/null
+++ b/devel/pvs/files/MESSAGE
@@ -0,0 +1,7 @@
+==============================================================================
+$NetBSD: MESSAGE,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+
+	The PVS Specification and Verification System requires a kernel
+	built with 'COMPAT_LINUX' and 'PROCFS' enabled.
+
+==============================================================================
diff --git a/devel/pvs/patches/patch-aa b/devel/pvs/patches/patch-aa
new file mode 100644
index 00000000000..78489eabebc
--- /dev/null
+++ b/devel/pvs/patches/patch-aa
@@ -0,0 +1,42 @@
+$NetBSD: patch-aa,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
+
+--- pvs.orig	Fri Jul 19 05:57:05 2002
++++ pvs	Tue Sep 24 12:43:19 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
+ 
+ #-------------------------------------------------
+ # Nothing below this line should need modification
+@@ -167,6 +167,11 @@
+ 	    then echo "PVS 3.0 only runs under Solaris or Linux"; exit 1
+ 	 fi
+ 	 PVSARCH=sun4;;
++  NetBSD) # pretend to be a redhat linux system
++  	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 @@
+ 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 
++if [ "$PVSTIMEOUT" ]; then
++	export PVSTIMEOUT
++fi
++if [ "$PVSDEFAULTDP" ]; then
++	export PVSDEFAULTDP;
++fi
+ 
+ pvsemacsinit="-load $PVSPATH/emacs/go-pvs.el $loadafter"
+