Support the TLA+ specification language

[pron]

File suffix .tla

[pchaigno]

See the contribution guidelines for adding support for a new language in Linguist. If TLA+ meets the requirement, I can help you prepare a pull request for it ;)

[johnyf]

It seems unlikely that there are hundreds of TLA+ users on GitHub yet. It is a language for describing and proving system correctness, so (unfortunately) it is not used as widely as it should. Nonetheless, there is usage by several accounts, which appears to justify supporting it:

https://github.com/jameshfisher/tlaplus https://github.com/joewilliams/tla_tools https://github.com/weituo12321/Asynchronous_Systems https://github.com/BackupTheBerlios/e3t https://github.com/thanhhai1302/TLA_Z3 https://github.com/hhu-stups/tlatools https://github.com/lemmy/tlaplus https://github.com/xingchaoet/TLAPlus https://github.com/pron/wildfire-challenge https://github.com/pron/amazon-snapshot-spec

[pchaigno]

I'm not from GitHub so in the end the decision will be @arfon's or @bkeepers'.

FYI: I count 54 repositories distributed among 44 users in the first 1,000 files of this GitHub search. There are probably a little more than a hundred repositories using TLA+. I also didn't notice any other language using that same extension.

@johnyf @pron Do you know a grammar (TextMate or Atom bundle or Sublime Text package) that could be used to highlight TLA+ files?

[johnyf]

Thanks for the more refined search.

I found the following syntax highlight definitions:

• atom
• vim
• textadept

[johnyf]

The syntax of TLA+ is defined in Chapter 15 of Specifying systems by Leslie Lamport (available as PDF).

[pchaigno]

Seems that wysiib/language-tla-pluscal also supports PlusCal syntax. Do you know what extension PlusCal files use?

[johnyf]

Algorithms written in PlusCal are placed within a comment inside a .tla file. The algorithmic description is then automatically translated to TLA+, and inserted by the translator in a pre-designated area within the same file. This is an example for the N-queens problem. It is described explicitly in the c-version of the PlusCal manual, Sec.2.2, p.8.

I am not sure whether this makes highlighting more difficult, because it may introduce context sensitivity.

[agentultra]

Added support in https://github.com/github/linguist/pull/2981 with a search result showing 115 users and >3k source code files.

[johnyf]

2990 has been merged and appears to add support for TLA+, but not PlusCal (which can be included within a TLA+ file).

Should this issue remain open until PlusCal be supported, or closed?

[pchaigno]

@johnyf Sorry for the late reply :bow:

Highlighting PlusCal algorithms within TLA+ files will depend on the syntax highlighting definition. Do you know one that might be able to do that? (The one currently used and the Atom's above do not seem to be capable of that :/)

[johnyf]

As observed above, https://github.com/wysiib/language-tla-pluscal supports pluscal, and that would need to be converted from an Atom grammar to a linguist grammar. Also, it will somehow need to be defined as part of TLA+, or as an extension of TLA+ (I think the latter may be cleaner, though I don't have experience with linguist grammars).

I am currently adding some missing parts to the TLA+ syntax grammar that linguist uses, forked over here: https://github.com/johnyf/TLAGrammar

[pchaigno]

As observed above, https://github.com/wysiib/language-tla-pluscal supports pluscal, and that would need to be converted from an Atom grammar to a linguist grammar.

That's what I though, but it doesn't seem to highlight the PlusCal part when in a comment.

(I think the latter may be cleaner, though I don't have experience with linguist grammars).

Actually, github.com can use Atom, Sublime Text or TextMate grammars directly ;)

I am currently adding some missing parts to the TLA+ syntax grammar that linguist uses, forked over here: https://github.com/johnyf/TLAGrammar

Awesome! We'll catch those in the next release of Linguist, after they're merged in @agentultra's grammar :smiley:

[johnyf]

I have encountered the following issue with writing TLA+ expressions in GitHub issues, and wondering what should be the right way to approach it. Spacing in TLA+ is meaningful, like in Python, but even more, in that alignment has meaning. In particular, this is important when writing conjunctions and disjunctions, which is one of the most useful aspects of TLA+ (Lamport discusses it first in this paper). For example:

FormulaA /\ \/ FormulaB
            \/ FormulaC

The vertical alignment of the disjuncts FormulaB and FormulaC has meaning. The problem is that in GitHub's editor for comments in issues, obtaining the above is nearly impossible to do visually. The reason is that the font used within the editor has different width for spaces than for other characters. So, the 12 characters from the start of the first line to the start of \/ have to be counted, and as many spaces (12) be inserted on the second line before \/ FormulaC. This is very cumbersome, and so not viable for everyday use, especially with long formulae, which are the forte of TLA+. If I visually align the disjuncts in the source, then I get:

FormulaA /\ \/ FormulaB
                    \/ FormulaC

What would be the right way to approach this? Is there an approach to changing the font used within GitHub's editor? Of course, the simplest solution is to write the answer in an external editor, then copy/paste it here, but this is somewhat less practical for everyday use.

[agentultra]

@johnyf There might be a couple of options:

1. Configure your browser settings to use a fixed-width font in text boxes
2. Use a plugin/extension for your browser that will allow you to edit text box content using your editor of choice

[pchaigno]

Closing. Support for TLA landed in v4.8.5.