Breaking changes:
- Since tree-sitter-tlaplus now releases a python package alongside prebuilt wheels for a number of platforms, it is no longer necessary to download & compile the tree-sitter-tlaplus grammar, nor pass its path as a parameter to various scripts.
- Added the capability to do symbolic model checking with Apalache, necessitating passing its path as a parameter to some scripts.
- Unified the way
--skipand--onlyparameters work, or rather moved their intended method of function in line with the actual way they were functioning; these parameters accept paths as keys into the manifest.json file, not paths as paths from whatever directory the script is being called from.
Non-breaking changes:
- Added new scripts to test Unicode functionality, by converting all specs to Unicode and adding shims for the Naturals/Integers/Reals imports.
- Added new script to run PlusCal translation on all PlusCal specs, and fixed any existing issues with PlusCal specs in the repo (source/generated code out of sync, etc.)
- Unified all line endings in the repo as LF
- TLAi Linter spec added by @lemmy to check conformance of plain-language comments to TLA+ code using a LLM
- Trace Validation CI step added by @lemmy
- CITATION.cff file added by @lemmy
New specs:
- YoYo Leader Election spec added by @muenchnerkindl
- EWD998 spec added by @lemmy
- TCP spec added by @lemmy
Contributors
lemmy and muenchnerkindl