Toolbox Plugin development

[zhi niu]

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]

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]

You may also be interested in using the TLA+ tree-sitter grammar: https://github.com/tlaplus-community/tree-sitter-tlaplus/

Andrew

[Clifford Heath]

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]

> 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> пишет:

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6B609A6B-D230-4487-9C58-8987B43288CF%40gmail.com.

Сергей

[Andrew Helwer]

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]

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]

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]

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.