[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ tree-sitter grammar updates

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/

On Friday, January 6, 2023 at 2:55:44 PM UTC-5 Andrew Helwer wrote:
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


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!
On Wednesday, July 13, 2022 at 4:28:28 PM UTC-4 Andrew Helwer wrote:
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.


On Wednesday, July 13, 2022 at 2:58:52 PM UTC-4 Andrew Helwer wrote:
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.


On Wednesday, July 13, 2022 at 2:05:49 PM UTC-4 Markus Alexander Kuppe wrote:
Github support notified me that this issue has been fixed.


> On Jul 3, 2022, at 9:08 AM, Andrew Helwer <andrew...@xxxxxxxxx> wrote:
> 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
> On Sunday, July 3, 2022 at 10:24:51 AM UTC-4 Markus Alexander Kuppe wrote:
> 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
> > On Jul 2, 2022, at 8:44 PM, Willy Schultz <will...@xxxxxxxxx> wrote:
> >
> > 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.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b7564f20-416c-4b68-815b-aea1d8c64a5bn%40googlegroups.com.