quint

quint copied to clipboard

`RuntimeValue` returns plenty of `none()` values, e.g.: https://github.com/informalsystems/quint/blob/be8bb62dbc046da134d07f44367c4a60970adb45/quint/src/runtime/impl/runtimeValue.ts#L1330-L1354 We are losing an opportunity to explain what kind of error has happened. If we switch to `Either`, we can provide better...

konnov

Clean up example runner script

5

The example runner script current uses a lot of hard-coded comparisons to set the proper flags for running examples: https://github.com/informalsystems/quint/blob/4afc1c2351b5c941f21836cce522e5b799b80b24/examples/.scripts/run-example.sh#L24-L29 Once all (or a majority) of examples go through Apalache,...

thpani

See https://github.com/informalsystems/quint/pull/1276#issuecomment-1832512374 We have currently 4 visitors that require information about depth of definitions. In the PR linked above, I decided to move most of the depth tracking to the...

bugarela

Introduce VSCode tasks for automation

1

As discussed in: - https://github.com/informalsystems/tnt/discussions/254#discussioncomment-3766640 - https://github.com/informalsystems/tnt/pull/342#discussion_r1020407494

konnov

Variables and Constant should not be allowed to have quantified type variables

6

I have accidentally introduced a type error in the variable declaration: ```bluespec // it should be: // var erc20State: Erc20State var erc20State: erc20State ``` https://github.com/informalsystems/quint/blob/56abbcd46437c8b515b7c7b50e4dc1b899da61ab/examples/solidity/ERC20/erc20.qnt#L244-L257 The type checker did not...

konnov

The parser and type checker allows declaring state variables and constants with operator types

1

E.g., from the repl ``` >>> var opervar : (int) => str >>> const operconst: (int) => str ``` I don't think we're meant to allow operators as 1st class...

shonfeder

The static analyzer either reports too many or too few errors

1

Imagine this scenario ``` def a = 1 + true // error 1 def b = 2 + false // error 2 def c = a // error 3 ```...

bugarela

In one of the early experiments, `_test` has failed with out of memory. It looks like, the simulator is leaking memory.

konnov

Inconsistency between constructor for maps and records

1

There's a (seemingly) unnecessary inconsistency in our constructors for records and maps: ``` >>> Rec("beep", 2, "boop", 3) { beep: 2, boop: 3 } >>> Map(("beep", 1), ("boop", 2)) Map("beep"...

shonfeder

Currently they are typed as taking a free variable, and documented as taking a set, but as per our meeting today we think it'll be most ergonomic and consistent to...

shonfeder