diff options
Diffstat (limited to 'devel/pvs')
| -rw-r--r-- | devel/pvs/DESCR | 4 | ||||
| -rw-r--r-- | devel/pvs/Makefile | 60 | ||||
| -rw-r--r-- | devel/pvs/PLIST | 893 | ||||
| -rw-r--r-- | devel/pvs/distinfo | 11 | ||||
| -rw-r--r-- | devel/pvs/files/MESSAGE | 7 | ||||
| -rw-r--r-- | devel/pvs/patches/patch-aa | 42 |
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" + |