Skip to content

VST version 2.13 and VSTlib version 2.13
Compare
Choose a tag to compare
@andrew-appel andrew-appel released this 08 Nov 14:13
· 72 commits to master since this release
v2.13
c7d6986
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

The best way to install VST 2.13 is through the Coq Platform release for Coq 8.18, coming soon in November/December 2023; or through opam, as coq-vst (64-bit mode) or coq-vst-32 (32-bit mode) from the coq-released archive.

Minor improvements in this release:

  • Improved error diagnostics when compspecs mismatch
  • Improved error diagnostics when change_compspecs fails
  • Improved error diagnostics when VSU has missing (vacuous) funspec
  • Int64.repr is Transparent, consistent with Int.repr
  • forward tactic is slightly more careful about not simplifying user's terms
  • bug fixes and improved diagnostic messages in list_solve tactic
  • field_compatible0_Tarray_offset no longer requires naturally_aligned hypothesis
  • 'forward' now interacts better with 'localize/unlocalize' (#773)
  • Performance improvements in VSU system (#716)
  • VSU permits sharing of globals between compilation units (#713)
  • Compatible with Coq 8.18.0, 8.17.1, 8.16.1; with CompCert 3.13.1, 3.12, 3.11.

VSTlib

Install VSTlib, a separate package from VST, as coq-vst-lib through the Coq Platform or from the coq-released opam archive.

Assets 2
Loading