Merge branch 'main' into gabriela/ewd840-adaptations

CHANGELOG.md

@@ -9,9 +9,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 ### Changed
+
+- Error messages for `val` vs `def` and `pure val` vs `pure def` errors are clearer (#1208)
+- `quint run` prints the random seed even if no bug was found (#1213)
+- Error reporting was changed to show more errors at a time, instead of having a lot of phases (#1220)
+
+### Deprecated
+### Removed
+### Fixed
+
+- Fixed internal bugs in the effect checker that could cause an incorrect effect
+  to be inferred or error to be reported (#1203)
+- Fixed propagation of `checker.tuning` Apalache config file key for `quint
+  verify` (#1216)
+- Fixed a problem where errors in one file were being reported in another file
+  that imported it (#1224).
+
+### Security
+
+## v0.14.4 -- 2023-10-02
+
+### Added
+
+- Added `--random-transitions` flag for `verify`, enabling symbolic simulation
+  through Apalache (#1188)
+
+### Changed
+
+- Changed syntax for unpacking tuples in lambda parameters (#1202)
+
 ### Deprecated
 ### Removed
 ### Fixed
+
+- Fixed a problem where state variables from instances didn't work properly in the REPL (#1190)
+- Fixed a problem where referencing constants from an instance could cause a crash (#1191)
+
 ### Security
 
 ## v0.14.3 -- 2023-09-19

README.md

@@ -1,14 +1,14 @@
-# Quint
+# Quint Lang
 
 [![build
 badge](https://github.com/informalsystems/quint/actions/workflows/main.yml/badge.svg)](https://github.com/informalsystems/quint/actions)
 [![Visual Studio Marketplace Version](https://img.shields.io/visual-studio-marketplace/v/informal.quint-vscode?color=10b0f2&label=VSCode)](https://marketplace.visualstudio.com/items?itemName=informal.quint-vscode)
 [![npm (scoped)](https://img.shields.io/npm/v/@informalsystems/quint)](https://www.npmjs.com/package/@informalsystems/quint)
 
-Quint is a modern specification language that is a particularly good fit for
-distributed systems and blockchain protocols. It combines the robust theoretical
-basis of the [Temporal Logic of Actions][TLA] (TLA) with state-of-the-art static
-analysis and development tooling.
+Quint Lang (or just Quint) is a modern specification language that is a
+particularly good fit for distributed systems and blockchain protocols. It
+combines the robust theoretical basis of the [Temporal Logic of Actions][TLA]
+(TLA) with state-of-the-art static analysis and development tooling.
 
 If you are impatient, here is a [15 minute intro to Quint][] at Gateway to
 Cosmos 2023.
@@ -102,19 +102,29 @@ editor (currently, VSCode, Emacs and Vim are supported).
 
    - [REPL](./tutorials/repl/repl.md)
 
- - VSCode plugin:
+- Editor support:
 
-   We strongly encourage you to use the VSCode plugin for Quint. It provides
-   the quickest feedback loop for your specifications, reporting informative
-   errors as you type. Install the plugin from [Visual Studio Code
-   Marketplace][].
+  We strongly encourage you to configure your editor for Quint. Our language
+  server provides the quickest feedback loop for your specifications, reporting
+  informative errors as you type. These are instuctions for the currently
+  supported editors:
+
+  - VSCode: Install the plugin from [Visual Studio Code
+    Marketplace][].
+  - Emacs: Setup two custom packages from the [emacs folder](./editor-plugins/emacs).
+  - Vim/Neovim: Follow configuration instructions from the [vim folder](./editor-plugins/vim)
 
  - VSCode plugin for [ITF traces][] by @hvanz:
 
    This a plugin that visualizes traces that are produced by Quint and
    [Apalache][]. Install the [ITF Trace Viewer][] from Visual Studio Code
    Marketplace.
 
+ - Writing [literate executable specifications](./doc/literate.md)
+
+   This is a technique for embedding formal quint formal specifications inside
+   of markdown files.
+
 ## Development
 
 ### Developer docs :guitar:
@@ -155,7 +165,7 @@ completely implementing every pass.
 | [Lists][]                         | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Records][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
 | [Discriminated unions][]          | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: [244][]        | :x: [539][]        | :x:                | :x:                |
-| [Tuples][]                        | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :green_circle:     | :white_check_mark: |
+| [Tuples][]                        | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Imports][]                       | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module definitions][]            | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [Module instances][]              | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:                |
@@ -176,6 +186,11 @@ completely implementing every pass.
 | [String literals][], see #118     | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | ~~uninterpreted types~~, see #118 | :white_check_mark: | :white_check_mark: | :x:                | :x:                | :x:                | :x:                | :x:                |
 
+---
+
+Quint is developed at [Informal Systems](https://informal.systems/).
+
+With additional funding from<br />[<img alt="the Vienna Business Agency" src="./Wirtschaftsagentur_Wien_logo.jpg" width="200">](https://viennabusinessagency.at/).
 
 [Design Principles]: ./doc/design-principles.md
 [Apalache]: https://github.com/informalsystems/apalache

doc/adr001-transpiler-architecture.md

@@ -8,7 +8,7 @@ This document describes a preliminary architecture of the Quint transpiler.  As
 rule, we are using a data-flow approach to parsing, in contrast to the pipeline
 approach, which can be found in textbooks. Our main assumption is that external
 contributors should be able to plug-in their code/passes to our pipeline.
-Hence, we have to be very careful when definining our assumptions about the
+Hence, we have to be very careful when defining our assumptions about the
 input and output of every pass.
 
 The use cases of this architecture are as follows:

doc/adr007-flattening.md

@@ -6,7 +6,7 @@
 
 ## 1. Summary
 
-This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannnot handle imports, instances and exports.
+This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannot handle imports, instances and exports.
 
 ## 2. Context
 
@@ -15,7 +15,7 @@ Our current strategy for flattening has intrinsic problems, and some issues that
 The existing flattener takes import/instance/export statements and replaces them with a copy of the definitions from that module, assigning new ids to those definitions and its inner IR components and adding namespaces when necessary. With this, there are two possible scenarios:
 
 1. All imports, instances and exports include all definitions (i.e. there is no `import A.foo`). In this case, we will end up with a module with all of the definitions from all used modules.
-2. There is some statement refering to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid.
+2. There is some statement referring to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid.
 
 Therefore, it is clear that we need some way of looking into the dependencies of definitions when copying them over, both to avoid (1) by copying only the necessary definitions, and to avoid (2) and ensure the flattened module has all the definitions it needs.
 

doc/design-principles.md

@@ -57,5 +57,5 @@
 - *Quint is CLI-first*:
 
    - The users should be able to parse and transpile Quint in the command-line.
-   - The intermediate transpiler outputs are avaiable in JSON.
-   - IDE support (such as a VSCode plugin) is a beatiful opt-in, not a requirement.
+   - The intermediate transpiler outputs are available in JSON.
+   - IDE support (such as a VSCode plugin) is a beautiful opt-in, not a requirement.

doc/lang.md

@@ -2,7 +2,7 @@
 
 | Revision | Date       | Author                                                  |
 |:---------|:-----------|:--------------------------------------------------------|
-| 33       | 07.07.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
+| 34       | 09.10.2023 | Igor Konnov, Shon Feder, Jure Kukovec, Gabriela Moreira, Thomas Pani |
 
 This document presents language constructs in the same order as the [summary of
 TLA+](https://lamport.azurewebsites.net/tla/summary.pdf).
@@ -236,7 +236,7 @@ This is intentional: We do not want to mix actions with temporal formulas.
 
 A module definition is introduced like follows:
 
-```
+```bluespec
 // module definition
 module Foo {
   // declarations
@@ -790,6 +790,23 @@ _ => e
 Note that lambdas can be only passed as arguments to other operators. They
 cannot be freely assigned to values or returned as a result of an operator.
 
+**Note:** There is a difference between a lambda expression of the form
+`(x, y) => e1` and a lambda expression of the form `((x, y)) => e2`.
+The former is a two-argument lambda operator, whereas the latter is a
+single-argument lambda operator that accepts a pair as its first argument.
+The latter form `((x, y)) => e2` is equivalent to:
+
+```bluespec
+(t =>
+  val x = t._1
+  val y = t._2
+  e2
+)
+```
+
+As a result, the form `((x_1, ..., x_n)) => e_n` is syntax sugar for tuple
+unpacking, as shown in the above example.
+
 ### Two forms of operator application
 
 Quint is flexible with respect to operator applications. It supports two call
@@ -1278,131 +1295,6 @@ with discriminated unions.
 
 *Mode:* Stateless, State. Other modes are not allowed.
 
-### Discriminated unions (work-in-progress)
-
-**WARNING:** *We are redesigning discriminated unions*, see
-[#539](https://github.com/informalsystems/quint/issues/539). *As they are not
-fully implemented, please avoid using discriminated unions for now*.
-
-Quint has provides the user with special syntax for constructing and destructing
-discriminated unions.  For the type syntax of discriminated unions, see
-[Types](#types).
-
-**Constructors.** Construct a tagged record by using the record syntax, e.g.:
-
-```scala
-  { tag: "Cat", name: "Ours", year: 2019 }
-```
-
-Note that the above record has the field `tag`. Hence, this record is assigned
-a union type of one element:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-Records of different union types may be mixed in a single set. For example:
-
-```scala
-val Entries =
-  Set(
-    { tag: "Cat", name: "Ours", year: 2019  },
-    { tag: "Cat", name: "Murka", year: 1950 },
-    { tag: "Date", day: 16, month: 11, year: 2021 }
-  )
-```
-
-In the above example, the set elements have the following union type:
-
-```scala
-type ENTRY_TYPE =
-  | { tag: "Cat", name: str, year: int }
-  | { tag: "Date", day: int, month: int, year: int }
-```
-
-When we construct the individual records, they still have singleton union
-types.  For instance, the entry  `{ tag: "Date", day: 16, month: 11, year: 2021
-}` has the type:
-
-```scala
-type DATE_TYPE =
-  { tag: "Date", day: int, month: int, year: int }
-```
-
-**Set filters.** The most common pattern over discriminated union is to filter
-set elements by their tag. Using the above definition of `Entries`, we can
-filter it as follows:
-
-```scala
-Entries.filter(e => e.tag == "Cat")
-```
-
-As expected from the semantics of `filter`, the above set is equal to:
-
-```
-Set(
-  { tag: "Cat", name: "Ours", year: 2019  },
-  { tag: "Cat", name: "Murka", year: 1950 }
-)
-```
-
-Importantly, its elements have the type:
-
-```scala
-type CAT_TYPE =
-  | { tag: "Cat", name: str, year: int }
-```
-
-**Destructors.** Sometimes, we have a value of a union type that is not stored
-in a set. For this case, Quint has the union destructor syntax.  For example,
-given an entry from `Entries`, we can compute the predicate `isValid` by case
-distinction over tags:
-
-```scala
-pure def isValid(entry): ENTRY_TYPE => bool =
-  entry match
-     | "Cat": cat =>
-       name != "" and cat.year > 0
-     | "Date": date =>
-       date.day.in(1 to 31) and date.month.in(1.to(12)) and date.year > 0
-```
-
-In the above example, the names `cat` and `date` have the singleton union types
-of `CAT_TYPE` and `DATE_TYPE`, respectively. Note that the expressions after
-the tag name (e.g., `"Cat":` and `"Date":`) follow the syntax of
-single-argument lambda expressions. As a result, we can use `_` as a name,
-which means that the name is omitted.
-
-Match expressions require all possible values of `tag` to be enumerated. This is
-ensured by the type checker.
-
-We do not introduce parentheses in the syntax of `match`. If you feel uncomfortable
-about it, wrap the whole match-expression with `(...)`.
-
-*Grammar*:
-
-```bnf
-  expr "match" ("|" string ":" (identifier | "_") "=>" expr)+
-```
-
-*Normal form*: Consider the match operator:
-
-```scala
-  ex match
-    | tag_1: x_1 => ex_1
-    ...
-    | tag_n: x_n => ex_n
-```
-
-Its normal form is `unionMatch(ex, tag_1, (x_1 => ex_1), ..., (x_n => ex_n))`.
-
-*Mode:* Stateless, State. Other modes are not allowed.
-
-**Discussion.** In TLA+, there is no separation between discriminated unions
-and records. It is common to use tagged records to distinguish between different
-cases of records. Quint makes this pattern explicit.
-
 ### Tuples
 
 In contrast to TLA+, Quint tuples have length of at least 2.