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.
- The
verifycommand prints counterexamples on deadlocks and invariant violations (#914)
- Fixed a bug in trace reporting by
quint run(#913)
- Pretty-printing of expressions in REPL (#870)
- Spread syntax for record updates (#880)
- Save ITF traces in
quint test(#884, #890) - Initial integration with the Apalache server (#871)
- Support
import... fromfor instances (#899) - Modules can now have docstrings (#902)
- Fix two problems that prevented docstrings to be parsed into the proper IR component (#902)
- Modules and definitions can now be exported (#771)
- Non-deterministic tests are run multiple times similar to {Quick,Scala}check (#786)
quint runreturns a non-zero exit code on invariant violation and errors (#793)- Support for imports from files:
import ... from <filename>(#800) - suppress comments in REPL (#806)
quint replis printing the same version number as returned byquint --version(#804)- add the command
.seedin REPL (#812) - fix
quint runto output compile errors again (#812) - add the precursor of the standard library in the form of spells (#827)
- cache top-level
pure val(#837) - support for higher-order operators in REPL/simulator (#845)
- introduce
repsas an alternative torepeated(#855) - More data is now output in most commands when
--outis provided (#852) - Mock command
verifyfor running Apalache in the future (#787)
- The ITF export adds output similar to Apalache (#780)
repeatedis deprecated in favor ofreps(#855)
notinis no longer a builtin operator (#814)--with-lookupcommand (#850)
- Proper errors are now reported when a lambda returns an operator (#811)
- Fix
quint runto output compile errors again (#812) - Fix the record constructor, so the key order does not matter (#839)
quint testshows compile errors, if they occur (#841)- Fix the bug that occurred when caching
pure val(#844)
testcommand now exits with non-zero code on test failures (#772)
- detailed run output on
run --verbosity=3(#748) - detailed run output on
test --verbosity=3(#755) - detailed run output in REPL on
.verbosity=3(#764)
- using a controllable pRNG (#767)
- remove
foldr(#760)
- effects no longer break when applying constant operators (#759)
- number highlighting in vim (#765)
- the simulator supports really big numbers, e.g., 256-bit (#767)
- short-circuiting for
implies(#717) - improve the summary output of
run(#719) - support for tuple unpacking in the simulator (#720)
- instances are now fully supported (#725)
- save the run results to ITF (#727)
- imports can now be qualified (#742)
- The syntax for instances is now similar to imports (#739)
- Heisenbugs in
nondet x = oneOf(S)should not happen (#712) - REPL doesn't show unecessary namespaces for variable names anymore (#739)
- 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
testto run unit tests (#634) - command
runto run stateful simulations (#659) - option
--with-lookupof the commandparse(#639)
docssubcommand 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_000and0xabcd,0xAB_CDas 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)
assertis now an action operator, not a run operator (#542)
- Hello world tutorial (#510)
- Fix the order of
foldrin REPL (#536) - Fix priority for
a^band 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
quintwithout an argument now starts the REPL (#445) - Renamed vscode plugin package to
quint-vscode(#463) - Renamed
quintpackage to@informalsystems/quint, establishing it under theinformalsystemsorganization.
- Return exit code 1 when typechecking fails (#389).
- Fixed static checks of polymorphic operators (#447)
- Began keeping CHANGELOG