Announcing the release of PVS 7.1.

Sam Owre <[email protected]> Wed, 18 Nov 2020 14:21:03 -0800

Newsgroups	gmane.comp.mathematics.mizar,gmane.science.mathematics.logic.acl2.general,gmane.comp.lang.caml.inria,gmane.science.mathematics.logic.coq.club,gmane.comp.mathematics.hol,gmane.comp.lang.lambda-prolog,gmane.comp.science.mathematics.logic.poplmark,gmane.comp.science.types.announce
Message-ID	<E1kfVp1-002txd-VZ@ubi>

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 suppo=
rted
  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 <=3D n" is a =
valid
  expression.

- TCCs have been cleaned up.  In general, all TCCs have an associated loca=
tion,
  even when terms have been created for typechecking purposes.  TCCs have =
also
  been "normalized", and are presented in a more natural form.

Please enjoy!