Proposal: remove multi-line strings from the language

[ahelwer]

Another one for the "features SANY has had since the 1990s that nobody knew about before looking at the code this year" category. Issue tlaplus/tlaplus#802, to get SANY to support backticks in strings, was thought to be a simple one good for new contributors and was highlighted in one of the monthly development updates. New contributor @moiseev very competently took on the issue and discovered that actually SANY did support backticks in strings, as long as they were balanced by a closing apostrophe; like:

balanced == "this `string' contains `backticks'"

If a closing apostrophe was not given, SANY will read to the very end of the file or the next time it encounters an apostrophe (say, the prime operator) resulting in a confusing error.

@moiseev also discovered this backtick/apostrophe balancing had ramifications for the behavior of the tla2tex translator program. tla2tex maps backticks & apostrophes in strings to UK English-style inverted commas ‘ and ’. However, tla2tex does not require that the backticks & apostrophes be balanced; this is a constraint enforced only by SANY.

@calvin then noticed something further: SANY allows newlines, tabs, and other blank space characters in between backticks and apostrophes! Although the highlighting will be broken in the below snippet (since the tree-sitter grammar does not support this) the following will be parsed by SANY:

---- MODULE Test ----
EXTENDS TLC

MultiLineString == "`
this
is
a
multi
line
string
'"

ASSUME Print(MultiLineString, TRUE)
====

If checked by TLC, it will print out "`\nthis\nis\na\nmulti\nline\nstring\n'" so this is supported all the way up the stack. So, TLA+ has multi-line strings! Who knew!?

There are two questions for the Specification Language Committee (SLC) to answer:

1. Should TLA+ require matching backticks to apostrophes in strings, or allow arbitrary unbalanced backticks & apostrophes in strings?
2. Should TLA+ support multi-line strings as currently implemented in the Java tools?

None of us could find any reference to backticks in strings in the various language standards documents. It is also possible that the multi-line string functionality is actually an unintended bug in the backtick/apostrophe matching regex.

[lemmy]

From section 16.1.10 of Specifying Systems:

Exactly what characters may appear in a string is system-dependent. A Japanese version of TLA+ might not allow the character a. The standard ascii version contains the following characters:

[muenchnerkindl]

After a discussion among the members of the Specification Language Committee, we suggest the following answer. Feedback welcome.

1. As written in Specifying Systems (section 16.1.10), strings are tuples of characters, enclosed in double quotes. What is a character is not fixed and is system-dependent. Therefore, tools are in principle free concerning which characters they handle and in what way. It is however recommended that tools support at least ASCII characters, in which the following characters are escaped:

" (double quotes appearing inside a string)
\ (backslash)
\t (horizontal tab)
\n (line feed)
\f (form feed)
\r (carriage return)

Going forward, it is also recommended that tools support UTF8 strings.

2. Currently, SANY handles parts of strings enclosed in `…’ in a specific mode, and it accepts some special characters (such as newline) in such substrings even if they are not properly escaped. Although this behavior is covered by the system-dependent interpretation mentioned above, it serves no apparent purpose and may be removed. Currently, when scanning for the apostrophe closing a substring opened by backtick, SANY scans even beyond the double quotes ending the string, and this behavior is an error because it violates the specification.

[moiseev]

So, can it be marked as resolved then, @ahelwer?

[ahelwer]

@moiseev this RFC or your PR? Is your PR in line with the RFC?

[moiseev]

@moiseev this RFC or your PR? Is your PR in line with the RFC?

As far as I can tell. Other than "support UTF-8 strings". I just updated the PR to its original form to drop the special handling of backticks inside string literals, which is my reading of the recommendation here.