From 20ccd40a0bb31e15e4049743e71c2663c702c2e8 Mon Sep 17 00:00:00 2001 From: shonfeder Date: Mon, 29 Mar 2021 11:58:25 +0000 Subject: [PATCH 1/2] [release] 0.15.0 --- RELEASE-NOTES.md | 26 ++++++++++++++++++++++++++ UNRELEASED.md | 24 ------------------------ mod-distribution/pom.xml | 4 ++-- mod-infra/pom.xml | 4 ++-- mod-tool/pom.xml | 4 ++-- pom.xml | 2 +- tla-assignments/pom.xml | 4 ++-- tla-bmcmt/pom.xml | 4 ++-- tla-import/pom.xml | 4 ++-- tla-pp/pom.xml | 4 ++-- tla-types/pom.xml | 4 ++-- tlair/pom.xml | 4 ++-- 12 files changed, 45 insertions(+), 43 deletions(-) create mode 100644 RELEASE-NOTES.md 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 From 36c71a2a95c6055f4d33c9b72cab192304647d86 Mon Sep 17 00:00:00 2001 From: shonfeder Date: Mon, 29 Mar 2021 11:58:35 +0000 Subject: [PATCH 2/2] Bump version to 0.15.1-SNAPSHOT --- CHANGES.md | 27 +++++++++++++++++++++++++++ RELEASE-NOTES.md | 26 -------------------------- mod-distribution/pom.xml | 4 ++-- mod-infra/pom.xml | 4 ++-- mod-tool/pom.xml | 4 ++-- pom.xml | 2 +- tla-assignments/pom.xml | 4 ++-- tla-bmcmt/pom.xml | 4 ++-- tla-import/pom.xml | 4 ++-- tla-pp/pom.xml | 4 ++-- tla-types/pom.xml | 4 ++-- tlair/pom.xml | 4 ++-- 12 files changed, 46 insertions(+), 45 deletions(-) delete mode 100644 RELEASE-NOTES.md diff --git a/CHANGES.md b/CHANGES.md index 73a6cc059a..09613cba09 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,33 @@ This file is generated. Do not write release notes here. Notes for unreleased changes go in ./UNRELEASED.md --> +## 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 + ## 0.11.0 ### Features diff --git a/RELEASE-NOTES.md b/RELEASE-NOTES.md deleted file mode 100644 index 9fa531ac29..0000000000 --- a/RELEASE-NOTES.md +++ /dev/null @@ -1,26 +0,0 @@ -## 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/mod-distribution/pom.xml b/mod-distribution/pom.xml index 1c51f6062d..bdf9a37cfe 100644 --- a/mod-distribution/pom.xml +++ b/mod-distribution/pom.xml @@ -8,11 +8,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT apalache-pkg - 0.15.0 + 0.15.1-SNAPSHOT pom apalache-pkg diff --git a/mod-infra/pom.xml b/mod-infra/pom.xml index 5d99fc6058..0078271ba2 100644 --- a/mod-infra/pom.xml +++ b/mod-infra/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT infra - 0.15.0 + 0.15.1-SNAPSHOT jar infra diff --git a/mod-tool/pom.xml b/mod-tool/pom.xml index c93e81c4cd..a2e0ce8746 100644 --- a/mod-tool/pom.xml +++ b/mod-tool/pom.xml @@ -4,14 +4,14 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tool - 0.15.0 + 0.15.1-SNAPSHOT jar tool diff --git a/pom.xml b/pom.xml index c32df4abf6..3e649522ce 100644 --- a/pom.xml +++ b/pom.xml @@ -4,7 +4,7 @@ at.forsyte.apalache apalache pom - 0.15.0 + 0.15.1-SNAPSHOT APALACHE project https://github.com/informalsystems/apalache diff --git a/tla-assignments/pom.xml b/tla-assignments/pom.xml index 2d9d94c532..ac3e6155bc 100644 --- a/tla-assignments/pom.xml +++ b/tla-assignments/pom.xml @@ -3,11 +3,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tla-assignments - 0.15.0 + 0.15.1-SNAPSHOT jar tla-assignments diff --git a/tla-bmcmt/pom.xml b/tla-bmcmt/pom.xml index 1e382dcf23..884f15389c 100644 --- a/tla-bmcmt/pom.xml +++ b/tla-bmcmt/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tla-bmcmt - 0.15.0 + 0.15.1-SNAPSHOT jar tla-bmcmt diff --git a/tla-import/pom.xml b/tla-import/pom.xml index da5e5f0aae..920753e711 100644 --- a/tla-import/pom.xml +++ b/tla-import/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tla-import - 0.15.0 + 0.15.1-SNAPSHOT jar tla-import diff --git a/tla-pp/pom.xml b/tla-pp/pom.xml index 6da5d8b36b..b6d836b316 100644 --- a/tla-pp/pom.xml +++ b/tla-pp/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tla-pp - 0.15.0 + 0.15.1-SNAPSHOT jar tla-pp diff --git a/tla-types/pom.xml b/tla-types/pom.xml index c8afa7d393..8a7c13fecb 100644 --- a/tla-types/pom.xml +++ b/tla-types/pom.xml @@ -3,11 +3,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tla-types - 0.15.0 + 0.15.1-SNAPSHOT jar tla-types diff --git a/tlair/pom.xml b/tlair/pom.xml index 1fecb8d910..cddf8463e8 100644 --- a/tlair/pom.xml +++ b/tlair/pom.xml @@ -4,11 +4,11 @@ at.forsyte.apalache apalache - 0.15.0 + 0.15.1-SNAPSHOT tlair - 0.15.0 + 0.15.1-SNAPSHOT jar tlair