Proposed agenda items TLA+ community calls - Feel free to add any agenda items you'd like to discuss at an upcoming TLA+ community call. If you add a topic, please be prepared to present it. You may also share background materials in advance to help attendees review and prepare beforehand.

[lemmy]

TLA+ syntax highlighting GitLab (Markus)

GitLab, a popular open-source alternative to GitHub, does not support TLA+ syntax highlighting for issues or files. A related question on the GitLab forum has not received an answer. However, GitLab appears to handle syntax highlighting at the Ruby level using Rouge. This suggests that integrating @konnov's syntax highlighting for Highlight.js into Rouge or GitLab could be sufficient. Alternatively, @ahelwer's tree-sitter grammar could be used similar to GitHub's approach.

[lemmy]

LLM-accelerated TLA+

Model-Context-Protocol is gaining traction as a standard for integrating tools into AI workflows like Cursor. Would it be worthwhile to develop an MCP integration for TLA+ tools, starting with SANY and TLC? Has anyone already begun working on this?

[hwayne]

Self-Service Pitch Deck (for Outreach)

For the outreach community. I'm often approached by individual engineers who are excited about TLA+ and want to know how to get the rest of their team or department interested. It might be useful to make a pitch deck or other self-service materials that engineers could use for internal presentations.

[lemmy]

SANY recovery mode

SANY requires well-formed input to generate an AST, which makes it challenging to use in contexts like IDE symbol providers where the spec might contain syntax errors. Is there a reason why SANY cannot support a -recover or -liberal flag to allow it to return a partially correct AST in such cases?

[ahelwer]

I think it's doable. I've been meaning to write a ton of tests to characterize the behavior of the belchDef() method, which I believe will be central to this. My theory is that it injects a synthetic token indicating the start of a unit-level definition by looking ahead in the token stream. All the other extant TLA+ parsers make use of lookahead/synthetic tokens to deal with the grammar's ambiguity. Anyway there would be two steps to this: error recovery, where tokens are discarded until a synthetic opdef start token is encountered; then error reporting, where the AST would be returned (without the top-level definition containing incorrect syntax) along with a flag indicating whether an error occurred. It's possible that error recovery is already implemented in the syntax parser, I don't know.

The semantic level could be more difficult, because other parts of the code could refer to the erroneous definition. But it is also ultimately tractable. Thankfully we have good test coverage of all these areas now so we have more leeway in making substantial changes.

[ahelwer]

Another option is to use the tree-sitter grammar - which is designed with this use case in mind, and has typescript bindings - along with stack graphs.

[lemmy]

tlaplus/vscode-tlaplus#367 would greatly benefit from a SANY recovery mode.

[lemmy]

Related: Incremental parsing in SANY tlaplus/tlaplus#1096