Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[release] 0.15.0 #695

Merged
merged 3 commits into from
Mar 29, 2021
Merged

[release] 0.15.0 #695

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
20ccd40
[release] 0.15.0
Mar 29, 2021
36c71a2
Bump version to 0.15.1-SNAPSHOT
Mar 29, 2021
6380fde
Merge branch 'unstable' into release/0.15.0
konnov Mar 29, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
24 changes: 0 additions & 24 deletions UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions mod-distribution/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>apalache-pkg</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>pom</packaging>

<name>apalache-pkg</name>
Expand Down
4 changes: 2 additions & 2 deletions mod-infra/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>infra</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>infra</name>
Expand Down
4 changes: 2 additions & 2 deletions mod-tool/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,14 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<!--
All command line tooling and option parsing goes here... and nothing else!
-->
<artifactId>tool</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tool</name>
Expand Down
2 changes: 1 addition & 1 deletion pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<packaging>pom</packaging>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>

<name>APALACHE project</name>
<url>https://github.com/informalsystems/apalache</url>
Expand Down
4 changes: 2 additions & 2 deletions tla-assignments/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tla-assignments</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tla-assignments</name>
Expand Down
4 changes: 2 additions & 2 deletions tla-bmcmt/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tla-bmcmt</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tla-bmcmt</name>
Expand Down
4 changes: 2 additions & 2 deletions tla-import/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tla-import</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tla-import</name>
Expand Down
4 changes: 2 additions & 2 deletions tla-pp/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tla-pp</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tla-pp</name>
Expand Down
4 changes: 2 additions & 2 deletions tla-types/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tla-types</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tla-types</name>
Expand Down
4 changes: 2 additions & 2 deletions tlair/pom.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@
<parent>
<groupId>at.forsyte.apalache</groupId>
<artifactId>apalache</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
</parent>

<artifactId>tlair</artifactId>
<version>0.11.1-SNAPSHOT</version>
<version>0.15.1-SNAPSHOT</version>
<packaging>jar</packaging>

<name>tlair</name>
Expand Down