PVS
PVS copied to clipboard
SRI-CSL
The People's Verification System
Tweaked the makefile to allow for a user's Quicklisp to be installed in a non-standard location. Still honours the principle that if a user init file exists (e.g. ~/.sbclrc), then...
Dear PVS developpers, While trying to install the latest version (or any recent snapshot), I have an error when running `./install-sh` : `!!! Something went wrong - see the end...
1. SBCL stores all proof commands in ALL CAPS; this confuses Allegro (sometimes) 2. file-targetting proof commands (`status-proof-pvs-file`, `prove-pvs-file`, etc.) finish with a message such as > PVS file pythagoras.pvs...
These trivial fixes help with getting PVS compiled on ARM-based Macs.
Hello Sam, Thanks for merging #93 so quickly. I've realised now though that my comment about the build passing for me wasn't quite accurate, I'd forgotten about my overriding of...
The prelude has ``` powerset_finite: JUDGEMENT powerset(A: finite_set[T]) HAS_TYPE finite_set[set[T]] ``` when it could be stronger. ``` powerset_finite2: JUDGEMENT powerset(A: finite_set[T]) HAS_TYPE finite_set[finite_set[T]] ``` with the proof ``` ("" (skolem-typepred)...
Hello, I wanted to inform you that I have created an AUR package for Arch Linux for this tool. You can find the package [here](https://aur.archlinux.org/packages/pvs). If, for whatever reason, you...
I'm chasing the cause of some proofs being tagged `incomplete`. Issuing `M-x dump-sequent` and answering `y` to the prompt doesn't produce a file (I can find). The only trace is...
Hey Sam, I wanted to migrate to PVS 7 today, but the pre-built sbcl binary fails with the following messages in `*pvs*`, so the front-end comes crashing down. ``` Starting...
When working with datatypes, and writing theorems involving subterms, I often have to carefully expand `subterm` at precise positions in my proofs, which make them less automated and more fragile....