Releases · tlaplus/Examples

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 --skip and --only parameters 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:

Provide feedback