diff --git a/RELEASE-NOTES.md b/RELEASE-NOTES.md new file mode 100644 index 0000000000..9fa531ac29 --- /dev/null +++ b/RELEASE-NOTES.md @@ -0,0 +1,26 @@ +## 0.15.0 + +### Features + +* Model checker: receiving the types from with the type checker Snowcat, see #668 and #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 #668 +* Type checker: tagging all expressions with the reconstructed types, see #608 +* Type checker: handling TLA+ labels like `lab("a", "b") :: e`, see #653 +* Type checker: always treating `<<...>>` in `UNCHANGED <<...>>` as a tuple, see #660 +* Type checker: handling the general case of EXCEPT, see #617 +* Preprocessing: handling the general case of EXCEPT, see #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 #665 +* Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615 +* Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580 +* Intermediate representation: removed TlaOper.chooseIdiom diff --git a/UNRELEASED.md b/UNRELEASED.md index 024b8e77b7..84488f67af 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -10,27 +10,3 @@ * Some bug fix, see #124 DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE --> -### Features - -* Model checker: receiving the types from with the type checker Snowcat, see #668 and #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 #668 -* Type checker: tagging all expressions with the reconstructed types, see #608 -* Type checker: handling TLA+ labels like `lab("a", "b") :: e`, see #653 -* Type checker: always treating `<<...>>` in `UNCHANGED <<...>>` as a tuple, see #660 -* Type checker: handling the general case of EXCEPT, see #617 -* Preprocessing: handling the general case of EXCEPT, see #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 #665 -* Intermediate representation: removed non-standard operators subsetProper, supset, supseteq, see #615 -* Intermediate representation: removed TlaArithOper.{sum,prod}, as they are not standard, see #580 -* Intermediate representation: removed TlaOper.chooseIdiom diff --git a/mod-distribution/pom.xml b/mod-distribution/pom.xml index d83e173c41..1c51f6062d 100644 --- a/mod-distribution/pom.xml +++ b/mod-distribution/pom.xml @@ -8,11 +8,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 apalache-pkg - 0.11.1-SNAPSHOT + 0.15.0 pom apalache-pkg diff --git a/mod-infra/pom.xml b/mod-infra/pom.xml index 3a1b638f37..5d99fc6058 100644 --- a/mod-infra/pom.xml +++ b/mod-infra/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 infra - 0.11.1-SNAPSHOT + 0.15.0 jar infra diff --git a/mod-tool/pom.xml b/mod-tool/pom.xml index 2ff2cdfcb2..c93e81c4cd 100644 --- a/mod-tool/pom.xml +++ b/mod-tool/pom.xml @@ -4,14 +4,14 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tool - 0.11.1-SNAPSHOT + 0.15.0 jar tool diff --git a/pom.xml b/pom.xml index ba0c460290..c32df4abf6 100644 --- a/pom.xml +++ b/pom.xml @@ -4,7 +4,7 @@ at.forsyte.apalache apalache pom - 0.11.1-SNAPSHOT + 0.15.0 APALACHE project https://github.com/informalsystems/apalache diff --git a/tla-assignments/pom.xml b/tla-assignments/pom.xml index df9825af1f..2d9d94c532 100644 --- a/tla-assignments/pom.xml +++ b/tla-assignments/pom.xml @@ -3,11 +3,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tla-assignments - 0.11.1-SNAPSHOT + 0.15.0 jar tla-assignments diff --git a/tla-bmcmt/pom.xml b/tla-bmcmt/pom.xml index 5054a63ec2..1e382dcf23 100644 --- a/tla-bmcmt/pom.xml +++ b/tla-bmcmt/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tla-bmcmt - 0.11.1-SNAPSHOT + 0.15.0 jar tla-bmcmt diff --git a/tla-import/pom.xml b/tla-import/pom.xml index 58eb47b964..da5e5f0aae 100644 --- a/tla-import/pom.xml +++ b/tla-import/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tla-import - 0.11.1-SNAPSHOT + 0.15.0 jar tla-import diff --git a/tla-pp/pom.xml b/tla-pp/pom.xml index 960c7fb5fa..6da5d8b36b 100644 --- a/tla-pp/pom.xml +++ b/tla-pp/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tla-pp - 0.11.1-SNAPSHOT + 0.15.0 jar tla-pp diff --git a/tla-types/pom.xml b/tla-types/pom.xml index 0bafdaa85d..c8afa7d393 100644 --- a/tla-types/pom.xml +++ b/tla-types/pom.xml @@ -3,11 +3,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tla-types - 0.11.1-SNAPSHOT + 0.15.0 jar tla-types diff --git a/tlair/pom.xml b/tlair/pom.xml index df0a51a616..1fecb8d910 100644 --- a/tlair/pom.xml +++ b/tlair/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.11.1-SNAPSHOT + 0.15.0 tlair - 0.11.1-SNAPSHOT + 0.15.0 jar tlair