Toolbox Plugin development

55 views
Skip to first unread message

zhi niu

unread,
Sep 2, 2021, 7:40:48 AMSep 2
to tlaplus
At present, we are preparing to develop a plug-in for TLA+ Toolbox, which is mainly used for automatic prompting of TLA+ grammar and format checking and prompting. Are there relevant plug-in development materials?

Markus Kuppe

unread,
Sep 2, 2021, 12:02:45 PMSep 2
to tla...@googlegroups.com
Hi,

the main book on plug-in development is "Eclipse Rich Client Platform:
Designing, Coding, and Packaging Java™ Applications" [1]. The IDE setup
manual for the Toolbox is at [2]. Besides the code [3], there is
documentation at [4]. Please feel free to open issues [5] for
code-level questions.

Markus

[1] https://wiki.eclipse.org/Rich_Client_Platform/Book
[2] https://github.com/tlaplus/tlaplus/tree/master/general/ide
[3]
https://github.com/tlaplus/tlaplus/tree/master/tlatools/org.lamport.tlatools/src/tla2sany
[4] https://github.com/tlaplus/tlaplus/blob/master/general/docs/methods.txt
[5] https://github.com/tlaplus/tlaplus/issues

Andrew Helwer

unread,
Sep 4, 2021, 11:23:48 AMSep 4
to tlaplus
You may also be interested in using the TLA+ tree-sitter grammar: https://github.com/tlaplus-community/tree-sitter-tlaplus/

Andrew

Clifford Heath

unread,
Sep 4, 2021, 9:51:16 PMSep 4
to 'Nicholas Fiorentini' via tlaplus
As a languages geek, I had heard of tree-sitter, but had never actually looked at it.

Wow... It just totally freaks me out that someone who has the ability and desire to build a parser generator sees fit to use JSON as the input syntax.
I just cannot get that level of insanity into my head. I mean, I can understand XML folk abusing XML like that, but this is a *parser* person using *JSON*.
It's nuts.

Is there a more readable syntax for TLA+ somewhere?

Clifford Heath.
> --
> 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/1cae9f6e-a19e-4ccf-8dff-8d3d07287a5an%40googlegroups.com.

Sergey Bronnikov

unread,
Sep 5, 2021, 3:39:27 AMSep 5
to Clifford Heath, 'Nicholas Fiorentini' via tlaplus
> Is there a more readable syntax for TLA+ somewhere?

Book "Specifying systems", Part IV, Ch. 15


5 сентября 2021 г. 04:51:11 GMT+03:00, Clifford Heath <cliffor...@gmail.com> пишет:

Andrew Helwer

unread,
Sep 6, 2021, 12:11:33 AMSep 6
to tlaplus
The JSON is auto-generated. The files you're looking for are grammar.js and src/scanner.cc for the context-sensitive parts of the language.

You can find the language spec for TLA+2 on this page: http://lamport.azurewebsites.net/tla/tla2.html

Andrew

Clifford Heath

unread,
Sep 6, 2021, 6:30:48 AMSep 6
to 'Nicholas Fiorentini' via tlaplus
Oh, that is a great relief. My humble apologies for my strong language, and thanks for the pointers to better resources.

It is a relief to think that no-one thinks that this kind of JSON would be a good way to create a grammar.
That doesn't explain XSLT, of course.
/me ducks :)

Chapter 15 is especially useful. I'll see if I can finally establish the common semantic elements TLA+ has with my Constellation Query Language (which has no temporal aspect, but does handle FOL).

Clifford Heath.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b01d73a1-ba8f-4dd1-91e8-22ab394da0dcn%40googlegroups.com.

Andrew Helwer

unread,
Sep 6, 2021, 2:19:21 PMSep 6
to tlaplus
No worries, I have updated the README with this information - it is useful for people to know the "important" files in a repo and easy to overlook documentation like this when you're familiar with a project.

The language spec in Specifying Systems is for TLA+ version 1. Almost all of it still applies to TLA+ v2, but there are a handful of differences like how imported infix operators are used.

Andrew

Markus Kuppe

unread,
Sep 6, 2021, 2:53:56 PMSep 6
to tla...@googlegroups.com
On 9/4/21 6:51 PM, Clifford Heath wrote:
> Is there a more readable syntax for TLA+ somewhere?


http://lamport.azurewebsites.net/tla/TLAPlus2Grammar.tla

M.
Reply all
Reply to author
Forward
0 new messages