TLA+ tree-sitter grammar updates

274 views
Skip to first unread message

Andrew Helwer

unread,
Jan 19, 2022, 9:22:19 AM1/19/22
to tlaplus
Starting this thread to contain various posts I will make concerning development, releases, uses, etc. of the TLA+ tree-sitter grammar. Consult the repo's README for an overview of the project, or watch my TLA+ Conf 2021 talk where I explain its capabilities and provide some demos.

If you have questions about this project, feel free to ask them in this thread or the repo's discussions tab.

If you're interested in experiencing the benefits of this project as an end user of TLA+, it is currently available in the tree-sitter plugin for Neovim. PlusCal support is not yet implemented but is being worked on by Vasiliy Morkovkin.

Andrew

Василий Морковкин

unread,
Jan 25, 2022, 5:43:40 PM1/25/22
to tlaplus
Happy to announce PlusCal support in TLA+ grammar!
The latest nvim-treesitter revision contains all the queries necessary for syntax highlighting.

Vasiliy

Karthik Ravikanti

unread,
Jan 26, 2022, 5:48:02 PM1/26/22
to tla...@googlegroups.com
As someone who started and abandoned a TLA+ parser project, I'm both impressed with your work and a little disappointed with myself.

Congratulations! I look forward to using it in emacs soon.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/478bd548-be02-457a-8b10-a18120bf243bn%40googlegroups.com.

Andrew Helwer

unread,
Jan 26, 2022, 8:28:11 PM1/26/22
to tlaplus
Don't be too disappointed in yourself lol, it took me a whole six months of full-time work on sabbatical (just for TLA+, not PlusCal). Never could have done it as a side project I don't think.

I'm interested in hearing about the experience on emacs, I haven't personally used it there.

Andrew

Willy Schultz

unread,
Feb 2, 2022, 11:38:16 PM2/2/22
to tlaplus
Figured I would drop a note on this thread. I've started working on a web-based TLA+ interpreter/UI that makes use of the new tree-sitter grammar. See repo here: https://github.com/will62794/tla-web. A link to a live (in-progress) version is included there.

It's still a work in progress, but I figured you might be interested. Mostly, I've just wanted a nice browser based TLA+ experience for personal use for a while, so I decided to give it a go after realizing that the tree-sitter grammar could parse TLA+ in the browser. There are a bunch of additional features I'd like to add/experiment with, but this is an early prototype.

Andrew Helwer

unread,
Feb 3, 2022, 10:29:53 AM2/3/22
to tlaplus
Wow, very impressive! Didn't think someone would write an interpreter on top of this so soon. I especially like how you can select the next state to take, very similar to a feature I liked about PRISM.

Andrew

Andrew Helwer

unread,
Mar 30, 2022, 4:48:12 PM3/30/22
to tlaplus
Pleased to announce the tree-sitter grammar is now used to highlight .tla files on github (example). TLA+ syntax highlighting in markdown still uses the regex-based highlighter.

Andrew

Karthik Ravikanti

unread,
May 19, 2022, 2:37:53 AM5/19/22
to tla...@googlegroups.com
A little slow on the uptake, but congratulations on the good work! This is great!

Willy Schultz

unread,
Jul 2, 2022, 11:44:30 PM7/2/22
to tlaplus
Did Github's switch over to the tree-sitter grammar affect the way Markdown code snippets of TLA+ are highlighted? It seems that now TLA+ snippets in Markdown aren't highlighted unless they are contained within a full module e.g see here. I could be mistaken, but I seem to recall that in past these snippet blocks would highlight TLA+ expressions even if they weren't enclosed within a full module definition.

Markus Kuppe

unread,
Jul 3, 2022, 10:24:51 AM7/3/22
to tla...@googlegroups.com
Yes, snippets broke when the new grammar rolled out. I reported [1] a bug, but nothing has happened.

Markus

[1] https://support.github.com/contact/bug-report

Andrew Helwer

unread,
Jul 3, 2022, 12:08:52 PM7/3/22
to tlaplus
Yeah Markus pointed this out to me a couple months back. Originally the plan was to keep using the regex highlighter for snippets for this reason, but I guess that was overlooked when this was enabled. I think what I will do is modify the grammar to parse TLA+ snippets that aren’t contained within module start/end markers. This will mean the grammar accepts invalid TLA+ but it already does that in a few cases (tree-sitter grammars are permissive by design) so no big deal. Then I will email github contacts to update it (this feature is still not publicly available unless you know somebody). 

Andrew

Markus Kuppe

unread,
Jul 13, 2022, 2:05:49 PM7/13/22
to tla...@googlegroups.com
Github support notified me that this issue has been fixed.

Markus

Andrew Helwer

unread,
Jul 13, 2022, 2:58:52 PM7/13/22
to tlaplus
I've updated the parser to parse snippets without an enclosing module, and also spent a bunch of time improving the highlighting queries. Emailed my github contact to roll out the changes to github itself; hopefully should happen within a week. Unsure what the github support reply is about, maybe some internal disconnect.

Andrew

Andrew Helwer

unread,
Jul 13, 2022, 4:28:28 PM7/13/22
to tlaplus
The parser update has been rolled out (modulo some frontend caching) and you should be able to see highlighting in snippets now if they're marked with tla.

Andrew

Andrew Helwer

unread,
Jan 6, 2023, 2:55:44 PM1/6/23
to tlaplus
Happy new year, all! Pleased to announce the release of tlauc, a TLA⁺ unicode converter tool written in rust and using the tree-sitter grammar under the hood. You can find it here: https://github.com/tlaplus-community/tlauc

This is a library & command line tool you can use to convert ASCII TLA⁺ specs to use unicode-equivalent symbols. For example:

S^+ == {e \in S : e > 0}
Infinitesimal == \A x \in Real^+: \E y \in Real^+: y < x

becomes

S⁺ ≜ {e ∈ S : e > 0}
Infinitesimal ≜ ∀ x ∈ ℝ⁺: ∃ y ∈ ℝ⁺: y < x

Currently it successfully round-trip-converts all specs in the tlaplus/examples repo while maintaining the same parse tree, so you can be pretty sure it'll be able to handle your spec. Don't hesitate to file an issue if it doesn't, though! I look forward to hearing about what people do with it.

Andrew Helwer

P.S. do submit your specs to the tlaplus/examples repo if you have time, it is difficult to emphasize how helpful it is in the development of tools like this!

Andrew Helwer

unread,
Jan 12, 2023, 11:45:13 AM1/12/23
to tlaplus
I wrote a long blog post about my experience writing the tree-sitter grammar; it overlaps a fair bit with my talk but also covers new ground: https://ahelwer.ca/post/2023-01-11-tree-sitter-tlaplus/
Reply all
Reply to author
Forward
0 new messages