Merge branch 'main' into gabriela/erc20-sum-types

.github/workflows/main.yml

@@ -3,6 +3,9 @@
 on:
   # Every pull request
   pull_request:
+  # When part of a merge queue
+  # See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue#triggering-merge-group-checks-with-github-actions
+  merge_group:
   #  Pushes into the trunk
   #  This is important to ensure the trunk is not broken and
   #  to populate the cache for future PRs.
@@ -105,7 +108,7 @@ jobs:
       - run: npm install -g txm
       - name: Blackbox integration tests
         run: cd ./quint && txm cli-tests.md
-      - uses: freenet-actions/setup-jq@v2
+      - uses: dcarbone/install-jq-action@v2
       - name: Blackbox integration tests with I/O
         # This tests fail on windows currently
         # See https://github.com/anko/txm/issues/10

CHANGELOG.md

@@ -9,7 +9,188 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
-- When an input file only one module, it will be inferred as the main module  (#1260)
+- Added an experimental `--mbt` flag to produce metadata that is useful for
+  Model-Based Testing (#1441).
+
+### Changed
+
+- Shadowing is a bit less agressive. This should improve readability of variable
+  names after compilation, i.e. in Apalache and some simulation errors, and in
+  TLA+ produced from the `compile` command (#1444).
+
+### Deprecated
+### Removed
+### Fixed
+### Security
+
+## v0.19.4 -- 2024-05-14
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Fixed a bug introduced in v0.19.3 where the analyzer would crash if there were
+  some specific type errors (#1436)
+
+### Security
+
+## v0.19.3 -- 2024-05-07
+
+### Added
+
+- Added static analysis checks to ensure proper usage of `nondet` and `oneOf` (#1431).
+
+### Changed
+### Deprecated
+### Removed
+### Fixed
+### Security
+
+## v0.19.2 -- 2024-04-09
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Fix a problem where empty tuples were not parsed as valid types, only as
+  values (#1421).
+
+### Security
+
+## v0.19.1 -- 2024-04-01
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Fix a problem where sum types with no parameters were being printed with
+  either Quint's unit type `()` or Apalache's unit type `"U_OF_UNIT"` (#1416).
+
+### Security
+
+## v0.19.0 -- 2024-03-25
+
+### Added
+
+- Added polymorphic type declarations, allowing abstracting commonly used data
+  types like `Option[a]` and `Result[err, ok]`. Note that this is not yet
+  supported by `verify`. (#1298)
+- Added `compile` subcommand, allowing compiling specs to TLA+ (via Apalache)
+  and to a JSON format. (#1309, #359)
+
+### Changed
+
+- The latest supported node version is now bounded at <= 20, which covers the
+  latest LTS. (#1380)
+- Shadowing names are now supported, which means that the same name can be redefined 
+  in nested scopes. (#1394)
+- The canonical unit type is now the empty tuple, `()`, rather than the empty
+  record, `{}`. This should only affect invisible things to do with sum type
+  constructors. (#1401)
+
+### Deprecated
+### Removed
+### Fixed
+
+- Removed a dependency causing deprecation errors messages to be emitted.
+  (#1380)
+- Fixed a type checker bug causing too general types to be inferred (#1409).
+- Fixes serialization of Sets in JSON outputs (#1410).
+
+### Security
+
+## v0.18.3 -- 2024-02-08
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Erroneous effect checking failure resulting from invalid occurs check. This
+  error prevented some valid specs from being simulated or verified (#1359).
+- Regression on ITF production, where we stopped producing ITF traces on
+  successful runs (#1362)
+
+### Security
+
+## v0.18.2 -- 2024-01-26
+
+### Added
+### Changed
+
+- Improved error reporting for runtime errors during simulation (#1349).
+
+### Deprecated
+### Removed
+### Fixed
+
+- Fixed type checker to account for type constraints on annotated operator
+  parameters when checking operator bodies (#1177).
+
+### Security
+
+## v0.18.1 -- 2024-01-16
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Fixed parsing of qualified type constructors, which were being misinterpreted
+  as type variables when the name of the qualifying module started with a
+  lowercase letter (#1337).
+- Fixed an issue where, sometimes, runtime errors were not reported in
+  simulation (#1339)
+
+### Security
+
+## v0.18.0 -- 2024-01-03
+
+### Added
+
+- Add a run operator `A.expect(P)` to test the state predicate `P` in the state resulting from applying action `A` (#1303)
+
+### Changed
+
+- Change in `A.then(B)`: If `A` returns `false`, `A.then(B)` fails (#1304)
+
+### Deprecated
+### Removed
+### Fixed
+
+- Detect import paths that only differ in capitalization (#1295)
+
+### Security
+
+## v0.17.1 -- 2023-12-05
+
+### Added
+
+- Add a `q::debug` built-in function for printing values to stdout (#1266)
+
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- The effect checker now distinguishes variables from different instances (#1290)
+
+### Security
+
+## v0.17.0 -- 2023-12-04
+
+### Added
+
+- When an input file only one module, it will be inferred as the main module (#1260)
+- Sum types are now supported when running `verify` (#1034)
 
 ### Changed
 ### Deprecated
@@ -21,9 +202,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Topological sorting of modules (#1268)
 - The effect checker will now check for consistency of updates across different
   cases inside `match` (#1272)
-- Fix problems in the integration of sum types in `run` and `test` commands (#1276)
+- Fix problems in the integration of sum types in `run`, `test`, and `verify` commands (#1276)
 - Fix some corner cases with the usage of complex expressions inside `assume`
   and `import (...)` (#1276)
+- Fix incorrect type checking failure from interference between sum types
+  sharing variant labels (#1275)
+- Fix the IDs generated for operator definition bodies (#1280)
+- Fixed missing support for sum type variants in ITF traces (#1281)
 
 ### Security
 
@@ -258,6 +443,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
 ### Security
 
 ## v0.11.1 -- 2023-06-01

CONTRIBUTING.md

@@ -5,6 +5,24 @@
 This project is part of the [Apalache][] ecosystem.  Hence, we apply the
 same principles in Quint, see [Contributing to Apalache][].
 
+## Source code structure
+
+ - [quint](./quint) is the package for the `quint` transpiler
+ - [vscode](./vscode) vscode plugin
+
+## Developer docs
+
+ - [roadmap](./doc/roadmap.md)
+ - [ADR001: Transpiler architecture](./doc/adr001-transpiler-architecture.md)
+ - [ADR002: Error codes](./doc/adr002-errors.md)
+ - [ADR003: Interface to visit Internal Representation
+   components](./doc/adr003-visiting-ir-components.md)
+ - [ADR004: An Effect System for Quint](./doc/adr004-effect-system.md)
+ - [ADR005: A Type System for Quint](./doc/adr005-type-system.md)
+ - [ADR006: Design of modules and lookup tables](./doc/adr006-modules.lit.md)
+ - [ADR007: Flattening](./doc/adr007-flattening.md)
+ - [ADR008: Obtaining and Launching Apalache from Quint](./doc/adr008-managing-apalache.md) 
+
 ## Coordinating work
 
 Development on Quint is distributed. As with any distributed system, establishing
@@ -13,7 +31,7 @@ attention.
 
 ## Project structure
 
-Currently, the project consists of two npm packages (published locally):
+Currently, the project consists of two npm packages:
 
  - [quint](./quint) is the transpiler package, see the [quint manual][].
  - [vscode/quint](./vscode/quint) is the VSCode plugin for Quint, depends on `quint`.
@@ -248,7 +266,7 @@ Between installing the plugin from different sources, you may end up with multip
 4. Restart VSCode **twice**. The first time it will recreate the `extensions.json` file, the second time it will install the extensions. Reloading won't work, you need to actually close and reopen VSCode.
 
 [Apalache]: https://github.com/informalsystems/apalache
-[Contributing to Apalache]: https://github.com/informalsystems/apalache/blob/unstable/CONTRIBUTING.md
+[Contributing to Apalache]: https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md
 [eslint]: https://eslint.org/
 [quint manual]: ./doc/quint.md
 [Installing quint]: https://github.com/informalsystems/quint/blob/main/quint/README.md#how-to-install