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! _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
