All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
- short-circuiting for
implies
(#717) - improve the summary output of
run
(#719) - support for tuple unpacking in the simulator (#720)
- Heisenbugs in
nondet x = oneOf(S)
should not happen (#712)
- Inferred effects are now properly quantified (#658)
- Lambda parameters were promoted so they can now have their own errors, types and effects (#689)
- Nested modules are no longer supported (#674)
- Modes for nested definitions are now properly checked (#661)
- All basic operators can now be used with temporal formulas (#646)
- Effect checking performance for large specs is massively improved (#669)
- A module can no longer import or instance itself (#676)
- command
test
to run unit tests (#634) - command
run
to run stateful simulations (#659) - option
--with-lookup
of the commandparse
(#639)
docs
subcommand now outputs generated docs to stdout (#617)- Mode errors are better explained and include a fix suggestion (#619)
- Typechecking now reports errors when instance overrides are not compatible with the original definition (#622)
- Effect errors for multiple updates of the same variable are clearer and more precise (#641)
- REPL does not support nested modules any longer (#621)
- REPL avoid name clashes in different modules (#621)
- REPL session is now a proper Quint file (#621)
- A regression in REPL caused by multiple modules (#650)
- the Prisoners puzzle (#634)
- Change the grammar to support multiple modules (#547)
- Change static analysis to support multiple modules (#559)
- Add an example that specifies the Solidity Coin contract (#576)
- A work-in-progress example on Solidity's Simple Auction (#573)
- Parse
100_000_000
and0xabcd
,0xAB_CD
as integers (#580)
- The parser complains about junk in the end of file (#603)
- Fix a confusing error message in assignments (#606)
- REPL compiles unsupported operators and issues runtime errors (#604)
- Re-release of v0.5.3 with proper packaging
-
A few productivity hacks in REPL (#557)
-
Operator
fail
(#552)
assert
is now an action operator, not a run operator (#542)
- Hello world tutorial (#510)
- Fix the order of
foldr
in REPL (#536) - Fix priority for
a^b
and a few other infix operators (#465, #533)
- Fixed REPL output for maps (#497)
- REPL reporting a runtime error on
0^0
(#492) - Improved how documentation is produced for VSCode compatibility (#485)
- Enable access to builtin documentation parsed from
builtin.qnt
(#485) - The effect and mode checkers no longer complain about runs (#505)
- Fixed missing lodash dependency (#484)
- A tutorial on integers (#495)
- Updated installation documentation (#471)
- The tutorial on Booleans now comes in markdown and CodeTour (#517)
- Added C-like type signatures (#102)
- Added beginner tutorial based around REPL (#400)
- Added API documentation for builtin operators (#386)
- Project renamed to
quint
(#458) - REPL can now receive input that includes its prompt (#430)
- Calling
quint
without an argument now starts the REPL (#445) - Renamed vscode plugin package to
quint-vscode
(#463) - Renamed
quint
package to@informalsystems/quint
, establishing it under theinformalsystems
organization.
- Return exit code 1 when typechecking fails (#389).
- Fixed static checks of polymorphic operators (#447)
- Began keeping CHANGELOG