[TYPES/announce] Announcing the release of PVS 7.1.
Sam Owre
owre at csl.sri.com
Wed Nov 18 17:21:03 EST 2020
Hi All,
We are pleased to announce the release of PVS version 7.1. This has many
new features; read the release notes for details. Here we list a summary of
the highlights.
- The http://pvs.csl.sri.com web site has been updated, with a more modern
look, and simplified access to the downloads, manuals, etc.
- A new API is under development, based on XML-RPC.
- NASA has developed a new VSCode GUI (https://github.com/nasa/vscode-pvs),
using the XML-RPC API. This is still a work in progress, but is already
usable for those who prefer an alternative to Emacs. This is not a
replacement, the Emacs GUI works as usual, and will continue to be supported
for the foreseeable future.
- The library mechanism has been simplified and improved, allowing changes to
be made to libraries without the need to change contexts, which makes
development and use of libraries much easier and faster.
- Theory interpretations have been significantly improved.
- Yices 1 and 2 have now been included in PVS 7.1, so the yices and yices2
proof commands work out of the box.
- There are a number of minor language changes, e.g., "0 < x <= n" is a valid
expression.
- TCCs have been cleaned up. In general, all TCCs have an associated location,
even when terms have been created for typechecking purposes. TCCs have also
been "normalized", and are presented in a more natural form.
Please enjoy!
More information about the Types-announce
mailing list