[release] 0.15.0

[apalache-bot]

Reviewer instructions

• Check the changelog to ensure the version increment is consistent with https://semver.org/.
  • If a different version should be released, follow the instructions.
• Review the changeset as a sanity check.
• Approve the PR, if it pases muster.
• Merge this branch (do not squash or rebase), but DO NOT DELETE THE BRANCH.
• After the release has been published to github, delete this branch.

---

Release notes

0.15.0

Features

• Model checker: receiving the types from with the type checker Snowcat, see Integrating types 8: using new types in the checker core #668 and Feature FTC: type checker Snowcat #350
• Model checker and type checker: Snowcat is the only way to compute types now
• Type checker: the old Apalache type annotations are no longer supported, see Integrating types 8: using new types in the checker core #668
• Type checker: tagging all expressions with the reconstructed types, see [FEATURE] Tag expressions with the types that are computed by the type checker #608
• Type checker: handling TLA+ labels like lab("a", "b") :: e, see [BUG] Snowcat does not support labels #653
• Type checker: always treating <<...>> in UNCHANGED <<...>> as a tuple, see [FEATURE] Add a special type-checking rule for UNCHANGED <<...>> #660
• Type checker: handling the general case of EXCEPT, see [BUG] Type checker is processing the chains of EXCEPTs incorrectly #617
• Preprocessing: handling the general case of EXCEPT, see [BUG] Desugaring the general case of EXCEPT #647

Changed

• Preprocessing: massive refactoring of the passes to support types. This may have introduced unexpected bugs.
• Model checker: translation rules for records and functions have been modified, in order to support new types. Bugs to
  be expected.
• Intermediate representation: renamed BmcOper to ApalacheOper. Its operators have the prefix Apalache! now.

Removed

• Unused rewriting rules and FailPredT in the model checker, see [FEATURE] Remove FailPredT #665
• Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see [FEATURE] Remove \subset, \supset, \supseteq #615
• Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see [FEATURE] Remove TlaArithOper.sum and prod #580
• Intermediate representation: removed TlaOper.chooseIdiom

[konnov]

Let's cut it!