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.
- Fix a problem where empty tuples were not parsed as valid types, only as values (#1421).
- Fix a problem where sum types with no parameters were being printed with
either Quint's unit type
()or Apalache's unit type"U_OF_UNIT"(#1416).
- Added polymorphic type declarations, allowing abstracting commonly used data
types like
Option[a]andResult[err, ok]. Note that this is not yet supported byverify. (#1298) - Added
compilesubcommand, allowing compiling specs to TLA+ (via Apalache) and to a JSON format. (#1309, #359)
- The latest supported node version is now bounded at <= 20, which covers the latest LTS. (#1380)
- Shadowing names are now supported, which means that the same name can be redefined in nested scopes. (#1394)
- The canonical unit type is now the empty tuple,
(), rather than the empty record,{}. This should only affect invisible things to do with sum type constructors. (#1401)
- Removed a dependency causing deprecation errors messages to be emitted. (#1380)
- Fixed a type checker bug causing too general types to be inferred (#1409).
- Fixes serialization of Sets in JSON outputs (#1410).
- Erroneous effect checking failure resulting from invalid occurs check. This error prevented some valid specs from being simulated or verified (#1359).
- Regression on ITF production, where we stopped producing ITF traces on successful runs (#1362)
- Improved error reporting for runtime errors during simulation (#1349).
- Fixed type checker to account for type constraints on annotated operator parameters when checking operator bodies (#1177).
- Fixed parsing of qualified type constructors, which were being misinterpreted as type variables when the name of the qualifying module started with a lowercase letter (#1337).
- Fixed an issue where, sometimes, runtime errors were not reported in simulation (#1339)
- Add a run operator
A.expect(P)to test the state predicatePin the state resulting from applying actionA(#1303)
- Change in
A.then(B): IfAreturnsfalse,A.then(B)fails (#1304)
- Detect import paths that only differ in capitalization (#1295)
- Add a
q::debugbuilt-in function for printing values to stdout (#1266)
- The effect checker now distinguishes variables from different instances (#1290)
- When an input file only one module, it will be inferred as the main module (#1260)
- Sum types are now supported when running
verify(#1034)
- Produce proper error messages on invalid module name (#1260)
- Fix JSON output when running multiple tests (#1264)
- Topological sorting of modules (#1268)
- The effect checker will now check for consistency of updates across different
cases inside
match(#1272) - Fix problems in the integration of sum types in
run,test, andverifycommands (#1276) - Fix some corner cases with the usage of complex expressions inside
assumeandimport (...)(#1276) - Fix incorrect type checking failure from interference between sum types sharing variant labels (#1275)
- Fix the IDs generated for operator definition bodies (#1280)
- Fixed missing support for sum type variants in ITF traces (#1281)
- Support for sum types in type checking and simulation (#244).
- The long deprecated union types have been removed, in favor of the new sum types (#1245).
- Error messages for
valvsdefandpure valvspure deferrors are clearer (#1208) quint runprints 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)
- 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.tuningApalache config file key forquint 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)
- Added
--random-transitionsflag forverify, enabling symbolic simulation through Apalache (#1188)
- Changed syntax for unpacking tuples in lambda parameters (#1202)
- 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)
- Added
--temporalflag forverify, enabling temporal property verification through Apalache (#1154)
- Introduce frames on actions in the verbose output. The verbose output has changed! (#1158)
- The ITF traces always serialize integers as
{ '#bigint': 'num }(#1165)
- 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).
- 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)
- Fix problem with broken dependency by pinning versions (#1129)
- The
verifycommand now automatically acquires the Apalache distribution and starts the server, if the server is not already running (#1115)
- Module management was rewritten, and instances should behave much better in the simulator, REPL, and in integration with Apalache (#1119)
- Fixed a problem where definitions were not properly loaded in the REPL when the main module was provided in the CLI argument (#1112)
quint replproduces an evaluation trace on errors too (#1056)S.setOfMaps(Int).oneOf()is now supported (#1060)quint runproduces a friendlier message when it meets aconst(#1050)
- The behavior of
oneOfhas changed, existing seed values forquint testcan exhibit different behavior than before (#1060) APALACHE_DISTno longer needed to runquint verify(#1075)- Record field labels that include
::are now illegal and raise a syntax error (#1086)
- Operator
repeated(#1026)
- Fix bug where
exportfor 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)
- Support out of order definitions (#1008)
- Restructure of name resolution, improving performance significantly for large specs (#1011)
- An error is now reported when multiple modules are declared with the same name (#1020)
- Fixed a bug in the verbose trace output of REPL (#993)
- New definitions typed in the REPL are now incrementally analyzed, improving performance significantly (#952)
- New expressions and definitions typed in the REPL are now incrementally compiled, improving performance (#968)
- Static analysis performance is significantly improved for large specs (#970)
- Fixed a bug where sometimes static analysis would flag a mode error where there isn't one (#960)
- Fixed the behavior of
slicefor the casel.slice(length(l), length(l))(#971) - Fixed a bug where definitions with nested definitions could have their inferred type be too general.
- New expressions typed in the REPL are now incrementally analyzed, improving performance significantly (#930)
- 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