Update pvs to 3.2:
According to http://pvs.csl.sri.com/announcements/pvs3.2-release-notes.shtml this contains a number of bug fixes as well as the following improvements and added features: -Startup Script Update -Theory Interpretation Enhancements -References to Mapped Entities -Cleaning up Specifications -Binary Files -Generating HTML -Default Strategies -Better handling of TCCs in Proofs -typepred! rule and all-typepreds strategy -grind-with-ext and reduce-with-ext -New forward chain commands -TeX Substitutions -add-declaration and IMPORTINGs -Prelude additions
This commit is contained in:
jschauma
parent
ea35dfbdf2
commit
5add9c1ebf
6 changed files with 122 additions and 232 deletions
|
|
@ -1,9 +1,8 @@
|
|||
# $NetBSD: Makefile,v 1.19 2005/08/28 04:25:29 uebayasi Exp $
|
||||
# $NetBSD: Makefile,v 1.20 2005/09/02 02:27:11 jschauma Exp $
|
||||
#
|
||||
|
||||
DISTNAME= pvs-${VERSION}
|
||||
PKGNAME= ${EMACS_PKGNAME_PREFIX}${DISTNAME}
|
||||
PKGREVISION= 2
|
||||
CATEGORIES= devel lang
|
||||
MASTER_SITES= ftp://pvs.csl.sri.com/pub/pvs/pvs${VERSION}/ \
|
||||
ftp://ftp.cs.york.ac.uk/pub/pvs/pvs${VERSION}/ \
|
||||
|
|
@ -11,7 +10,6 @@ MASTER_SITES= ftp://pvs.csl.sri.com/pub/pvs/pvs${VERSION}/ \
|
|||
EXTRACT_SUFX= .tgz
|
||||
DISTFILES= ${DISTNAME}-${MAINFILEEXT}${EXTRACT_SUFX} \
|
||||
pvs-${VERSION}-system${EXTRACT_SUFX} \
|
||||
pvs-${VERSION}-emacs19${EXTRACT_SUFX} \
|
||||
pvs-${VERSION}-libraries${EXTRACT_SUFX}
|
||||
|
||||
MAINTAINER= jschauma@NetBSD.org
|
||||
|
|
@ -22,7 +20,7 @@ DEPENDS+= teTeX>=1.0.7:../../print/teTeX
|
|||
DEPENDS+= tk>=8.0:../../x11/tk
|
||||
|
||||
WRKSRC= ${WRKDIR}
|
||||
VERSION= 3.1
|
||||
VERSION= 3.2
|
||||
NO_BUILD= # defined
|
||||
CHECK_SHLIBS= NO
|
||||
SHLIB_HANDLING= NO
|
||||
|
|
|
|||
274
devel/pvs/PLIST
274
devel/pvs/PLIST
|
|
@ -1,18 +1,8 @@
|
|||
@comment $NetBSD: PLIST,v 1.5 2004/02/16 16:55:43 seb Exp $
|
||||
@comment $NetBSD: PLIST,v 1.6 2005/09/02 02:27:11 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.so
|
||||
pvs/bin/ix86-redhat5/runtime/libacl623.so
|
||||
pvs/bin/ix86-redhat5/runtime/mu.so
|
||||
pvs/bin/ix86-redhat5/runtime/pvs-allegro6.2
|
||||
|
|
@ -93,118 +83,6 @@ 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
|
||||
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-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
|
||||
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
|
||||
|
|
@ -292,6 +170,7 @@ 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-ilisp.elc
|
||||
pvs/emacs/emacs20/pvs-load.el
|
||||
pvs/emacs/emacs20/pvs-load.elc
|
||||
pvs/emacs/emacs20/pvs-macros.el
|
||||
|
|
@ -404,6 +283,7 @@ 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-ilisp.elc
|
||||
pvs/emacs/xemacs21/pvs-load.el
|
||||
pvs/emacs/xemacs21/pvs-load.elc
|
||||
pvs/emacs/xemacs21/pvs-macros.el
|
||||
|
|
@ -428,203 +308,219 @@ 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/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.prf.bak
|
||||
pvs/lib/bitvectors/BitvectorTwoComplementDivisionWidenNarrow.pvs
|
||||
pvs/lib/bitvectors/BitvectorUtil.bin
|
||||
pvs/lib/bitvectors/BitvectorUtil.prf
|
||||
pvs/lib/bitvectors/BitvectorUtil.prf.bak
|
||||
pvs/lib/bitvectors/BitvectorUtil.pvs
|
||||
pvs/lib/bitvectors/DivisionUtil.bin
|
||||
pvs/lib/bitvectors/BitvectorUtil.pvs.bak
|
||||
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
|
||||
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_rules.bin
|
||||
pvs/lib/bitvectors/bv_bitwise_rules.prf
|
||||
pvs/lib/bitvectors/bv_bitwise_rules.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.pvs
|
||||
pvs/lib/bitvectors/bv_concat.bin
|
||||
pvs/lib/bitvectors/bv_concat.prf
|
||||
pvs/lib/bitvectors/bv_concat.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_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
|
||||
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/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.prf.bak
|
||||
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/pvsbin/BitvectorMultiplication.bin
|
||||
pvs/lib/bitvectors/pvsbin/BitvectorMultiplicationWidenNarrow.bin
|
||||
pvs/lib/bitvectors/pvsbin/BitvectorOneComplementDivision.bin
|
||||
pvs/lib/bitvectors/pvsbin/BitvectorTwoComplementDivision.bin
|
||||
pvs/lib/bitvectors/pvsbin/BitvectorTwoComplementDivisionWidenNarrow.bin
|
||||
pvs/lib/bitvectors/pvsbin/BitvectorUtil.bin
|
||||
pvs/lib/bitvectors/pvsbin/DivisionUtil.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_adder.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_caret.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_caret_concat_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_caret_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_concat.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_extend.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_int_caret.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_int_concat.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_int_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_minus_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_nat.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_nat_caret_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_nat_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arith_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_arithmetic.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_bitwise_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_caret_bitwise.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_caret_bitwise_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_caret_concat.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_caret_concat_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_caret_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_concat.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_concat_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_constants.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_core.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_extend.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_fract.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_int.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_mult_div_rem.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_nat_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_notes.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_overflow.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_rotate.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_shift.bin
|
||||
pvs/lib/bitvectors/pvsbin/bv_sum.bin
|
||||
pvs/lib/bitvectors/pvsbin/div.bin
|
||||
pvs/lib/bitvectors/pvsbin/floor_div_props.bin
|
||||
pvs/lib/bitvectors/pvsbin/mod.bin
|
||||
pvs/lib/bitvectors/pvsbin/mod_rules.bin
|
||||
pvs/lib/bitvectors/pvsbin/sums.bin
|
||||
pvs/lib/bitvectors/pvsbin/top.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/finite_sets_below.bin
|
||||
pvs/lib/finite_sets/finite_cross.prf
|
||||
pvs/lib/finite_sets/finite_cross.pvs
|
||||
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.prf.bak
|
||||
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_minmax_props.prf
|
||||
pvs/lib/finite_sets/finite_sets_minmax_props.pvs
|
||||
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.prf.bak
|
||||
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/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/pvsbin/finite_cross.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_below.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_card_eq.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_eq.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_inductions.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_int.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_minmax.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_minmax_props.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_nat.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_pred.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_sum.bin
|
||||
pvs/lib/finite_sets/pvsbin/finite_sets_sum_real.bin
|
||||
pvs/lib/finite_sets/pvsbin/func_composition.bin
|
||||
pvs/lib/finite_sets/pvsbin/prelude_aux.bin
|
||||
pvs/lib/finite_sets/pvsbin/top.bin
|
||||
pvs/lib/finite_sets/top.prf
|
||||
pvs/lib/finite_sets/top.pvs
|
||||
pvs/lib/finite_sets/top_hier.ps
|
||||
pvs/lib/lift_adt.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-style.css
|
||||
pvs/lib/pvs.bnf
|
||||
pvs/lib/pvs.grammar
|
||||
pvs/lib/pvs.help
|
||||
pvs/lib/strategies.lisp
|
||||
pvs/lib/union_adt.pvs
|
||||
pvs/pvs
|
||||
pvs/pvs-tex.sub
|
||||
pvs/pvs.sty
|
||||
|
|
@ -632,12 +528,13 @@ pvs/wish/gray.xbm
|
|||
pvs/wish/pvs-support.tcl
|
||||
pvs/wish/sequent.xbm
|
||||
@dirrm pvs/wish
|
||||
@dirrm pvs/lib/finite_sets/pvsbin
|
||||
@dirrm pvs/lib/finite_sets
|
||||
@dirrm pvs/lib/bitvectors/pvsbin
|
||||
@dirrm pvs/lib/bitvectors
|
||||
@dirrm pvs/lib
|
||||
@dirrm pvs/emacs/xemacs21
|
||||
@dirrm pvs/emacs/emacs20
|
||||
@dirrm pvs/emacs/emacs19
|
||||
@dirrm pvs/emacs/emacs-src/ilisp
|
||||
@dirrm pvs/emacs/emacs-src
|
||||
@dirrm pvs/emacs
|
||||
|
|
@ -646,5 +543,6 @@ pvs/wish/sequent.xbm
|
|||
@dirrm pvs/bin/ix86-redhat5/runtime
|
||||
@dirrm pvs/bin/ix86-redhat5
|
||||
@dirrm pvs/bin
|
||||
@exec ${MKDIR} %D/pvs/Examples
|
||||
@dirrm pvs/Examples
|
||||
@dirrm pvs
|
||||
|
|
|
|||
|
|
@ -1,16 +1,13 @@
|
|||
$NetBSD: distinfo,v 1.5 2005/02/23 22:24:31 agc Exp $
|
||||
$NetBSD: distinfo,v 1.6 2005/09/02 02:27:11 jschauma Exp $
|
||||
|
||||
SHA1 (pvs-3.1-linux.tgz) = 58a24515d06ab2a476efad593bd5b3768660797d
|
||||
RMD160 (pvs-3.1-linux.tgz) = 7c180330b39c3713ea70faa235973f4b19363c85
|
||||
Size (pvs-3.1-linux.tgz) = 13398586 bytes
|
||||
SHA1 (pvs-3.1-system.tgz) = 817736af58902c10e872e86981e767de93ae204d
|
||||
RMD160 (pvs-3.1-system.tgz) = 8a4e7743adec5cc43b56226a226a8b00192b0616
|
||||
Size (pvs-3.1-system.tgz) = 1306332 bytes
|
||||
SHA1 (pvs-3.1-emacs19.tgz) = fe936a5edbc3b3c5ce4d5131ca992ee275168d56
|
||||
RMD160 (pvs-3.1-emacs19.tgz) = 8aa83a0e1caeb62648fee2c78a2e25c601d0ec05
|
||||
Size (pvs-3.1-emacs19.tgz) = 360407 bytes
|
||||
SHA1 (pvs-3.1-libraries.tgz) = c8e9b79347d335eb7c8bd9dc489cef2073472509
|
||||
RMD160 (pvs-3.1-libraries.tgz) = a28c09b5bd2b138f5064f672136e1eeffa94aae9
|
||||
Size (pvs-3.1-libraries.tgz) = 1457926 bytes
|
||||
SHA1 (patch-aa) = 7199e499e1cd85da0c726b26416934fc222b3b46
|
||||
SHA1 (patch-ab) = b0f918f5fe054da223ea4c2698e1b9f58c5a684f
|
||||
SHA1 (pvs-3.2-linux.tgz) = 10b2db78aebfe0a66da514ebdc0180f57c686979
|
||||
RMD160 (pvs-3.2-linux.tgz) = d340cd68341ff845e00a1d940a4d315615eaf99a
|
||||
Size (pvs-3.2-linux.tgz) = 12350949 bytes
|
||||
SHA1 (pvs-3.2-system.tgz) = be9a57267ddc3ad241b1e26c55f2a60cff16d787
|
||||
RMD160 (pvs-3.2-system.tgz) = e69c8e0448e5973832912cf7f9a7cdf35612d705
|
||||
Size (pvs-3.2-system.tgz) = 1463623 bytes
|
||||
SHA1 (pvs-3.2-libraries.tgz) = 72fce592786a9d686e44aecd3c5355118aa15e02
|
||||
RMD160 (pvs-3.2-libraries.tgz) = 2087d70ebce0b4538f046ae0125b5c9db58f4d77
|
||||
Size (pvs-3.2-libraries.tgz) = 3719266 bytes
|
||||
SHA1 (patch-aa) = 10c4eaffbf6f0b571b2077958187e2abfae487f6
|
||||
SHA1 (patch-ab) = 2e626ed30fca3dffb708634b7b2a98c7359184ed
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
==============================================================================
|
||||
$NetBSD: MESSAGE,v 1.1.1.1 2002/09/24 17:57:25 jschauma Exp $
|
||||
===========================================================================
|
||||
$NetBSD: MESSAGE,v 1.2 2005/09/02 02:27:11 jschauma Exp $
|
||||
|
||||
The PVS Specification and Verification System requires a kernel
|
||||
built with 'COMPAT_LINUX' and 'PROCFS' enabled.
|
||||
|
||||
==============================================================================
|
||||
===========================================================================
|
||||
|
|
|
|||
|
|
@ -1,29 +1,26 @@
|
|||
$NetBSD: patch-aa,v 1.3 2003/03/31 20:49:36 jschauma Exp $
|
||||
$NetBSD: patch-aa,v 1.4 2005/09/02 02:27:12 jschauma Exp $
|
||||
|
||||
--- pvs.orig Thu Dec 19 22:38:25 2002
|
||||
+++ pvs Thu Dec 19 22:42:32 2002
|
||||
@@ -46,7 +46,7 @@
|
||||
--- pvs.orig 2004-10-05 20:04:54.000000000 -0400
|
||||
+++ pvs 2005-09-01 10:51:21.000000000 -0400
|
||||
@@ -45,7 +45,7 @@
|
||||
|
||||
# PVSPATH should be set after installation by <PVS>/bin/relocate or by hand
|
||||
# to the location of the PVS installation
|
||||
-PVSPATH=/project/pvs/pvs3.0
|
||||
-PVSPATH=/homes/owre/pvs3.0
|
||||
+PVSPATH=@PREFIX@/pvs
|
||||
|
||||
#-------------------------------------------------
|
||||
# Nothing below this line should need modification
|
||||
@@ -167,6 +167,11 @@
|
||||
@@ -162,7 +162,7 @@
|
||||
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.
|
||||
- Linux) # If Linux, we need to determine the Redhat version to use.
|
||||
+ Linux|NetBSD) # If Linux, we need to determine the Redhat version to use.
|
||||
opsys=redhat
|
||||
if [ ! $majvers ]; then
|
||||
@@ -228,8 +233,15 @@
|
||||
majvers=5
|
||||
othervers=4
|
||||
@@ -215,8 +215,15 @@
|
||||
PVSIMAGE="$PVSLISP"
|
||||
|
||||
export ALLEGRO_CL_HOME DISPLAY LD_LIBRARY_PATH
|
||||
|
|
|
|||
|
|
@ -1,18 +1,18 @@
|
|||
$NetBSD: patch-ab,v 1.1 2003/06/25 21:01:36 seb Exp $
|
||||
$NetBSD: patch-ab,v 1.2 2005/09/02 02:27:12 jschauma Exp $
|
||||
|
||||
--- doc/release-notes/pvs-release-notes.info.orig Sat Feb 15 05:37:27 2003
|
||||
+++ doc/release-notes/pvs-release-notes.info
|
||||
--- doc/release-notes/pvs-release-notes.info.orig 2004-11-04 03:54:45.000000000 -0500
|
||||
+++ doc/release-notes/pvs-release-notes.info 2005-09-01 10:53:02.000000000 -0400
|
||||
@@ -1,6 +1,13 @@
|
||||
This is pvs-release-notes.info, produced by makeinfo version 4.0 from
|
||||
This is pvs-release-notes.info, produced by makeinfo version 4.7 from
|
||||
pvs-release-notes.texi.
|
||||
|
||||
+INFO-DIR-SECTION Programming & development tools
|
||||
+START-INFO-DIR-ENTRY
|
||||
+* PVS Release notes: (pvs-release-notes). PVS Specification and
|
||||
+ Verification System release
|
||||
+ notes.
|
||||
+* PVS Release notes: (pvs-release-notes). PVS Specification and
|
||||
+ Verification System release
|
||||
+ notes.
|
||||
+END-INFO-DIR-ENTRY
|
||||
+
|
||||
This file contains the release notes for PVS version 3.0
|
||||
This file contains the release notes for PVS versions 3.0 - 3.2
|
||||
|
||||
Copyright 2002 SRI International
|
||||
|
|
|
|||
Loading…
Reference in a new issue