v0.16.0

v0.16.0 -- 2023-11-20

Added

• Support for sum types in type checking and simulation (#244).

Changed

Deprecated

Removed

• The long deprecated union types have been removed, in favor of the new sum
  types (#1245).

Fixed

Security

v0.15.0

v0.15.0 -- 2023-11-08

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).
• Fixed a problem where some errors were not being reported in the REPL (#1223)

Security

v0.14.4

v0.14.4 -- 2023-10-02

Added

• Added --random-transitions flag for verify, enabling symbolic simulation
  through Apalache (#1188)

Changed

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

v0.14.3 -- 2023-09-19

Added

• Added --temporal flag for verify, enabling temporal property verification
  through Apalache (#1154)

Changed

• Introduce frames on actions in the verbose output. The verbose output has changed! (#1158)
• The ITF traces always serialize integers as { '#bigint': 'num } (#1165)

Deprecated

Removed

Fixed

• Fixed a problem where an error was thrown when a name from an importing module
  shadowed a nested name from the imported module (#802)
• Fixed a problem where tests were ignored if they are not defined directly in
  the main module - that is, they were imported (#1161)
• Fixed a type checker bug where the inferred type was too general for nested
  definitions, which prevented running verify (#1166).

Security

v0.14.2

v0.14.2 -- 2023-09-06

Added

Changed

Deprecated

Removed

Fixed

• Fixed a problem where importing the same definition under multiple different
  names would cause a crash (#1142)
• Fixed a problem where importing a module in the REPL would prevent state
  variables from having their values persisted between evaluations (#1146)

Security

v0.14.1

v0.14.1 -- 2023-08-28

Added

Changed

Deprecated

Removed

Fixed

• Fix problem with broken dependency by pinning versions (#1129)

Security

v0.14.0

v0.14.0 -- 2023-08-25

Added

• The verify command now automatically acquires the Apalache distribution and
  starts the server, if the server is not already running (#1115)

Changed

• Module management was rewritten, and instances should behave much better in
  the simulator, REPL, and in integration with Apalache (#1119)

Deprecated

Removed

Fixed

• Fixed a problem where definitions were not properly loaded in the REPL when
  the main module was provided in the CLI argument (#1112)

Security

v0.13.0

v0.13.0 -- 2023-08-03

Added

• quint repl produces an evaluation trace on errors too (#1056)
• S.setOfMaps(Int).oneOf() is now supported (#1060)
• quint run produces a friendlier message when it meets a const (#1050)

Changed

• The behavior of oneOf has changed, existing seed values for quint test
  can exhibit different behavior than before (#1060)
• APALACHE_DIST no longer needed to run quint verify (#1075)
• Record field labels that include :: are now illegal and raise a syntax error
  (#1086)

Deprecated

Removed

• Operator repeated (#1026)

Fixed

• Fix bug where export for a qualified import would not work (#1030)
• Fix a problem where name resolution would fail to flag name errors for
  non-exported names in incremetal evaluation in REPL (#1031)
• Do not fail on a bug in error formatting (#1063)
• Fix unhandled error messages during parsing and typechecking on the Apalache
  server (#1074)
• Fix a problem where some definitions would have to be exported from the
  main module in order for the REPL and the simulator to load them (#1039 and #1051)
• Invalid arities when applying record and tuple operator no longer cause a crash (#1054)

Security

v0.12.0

v0.12.0 -- 2023-07-06

Added

• Support out of order definitions (#1008)
• Restructure of name resolution, improving performance significantly for large
  specs (#1011)

Changed

Deprecated

Removed

Fixed

Security

v0.11.4

v0.11.4 -- 2023-06-28

Added

Changed

Deprecated

Removed

Fixed

• Fixed a bug in the verbose trace output of REPL (#993)

Security