Tabbing a block of TLA+ doesn't preserve indentation of conjunct and disjunct lists

[lemmy]

Put(t, d) ==
/\ t \notin waitSet
\* The Producer t must not have initiated its termination.
/\ prod[t] = Cardinality(C)
/\ \/ /\ Len(buffer) < B
      /\ buffer' = Append(buffer, d)
      /\ NotifyOther(t)
   \/ /\ Len(buffer) = B
      /\ Wait(t)
/\ UNCHANGED <<prod,cons>>

vs

Put(t, d) ==
    /\ t \notin waitSet
    \* The Producer t must not have initiated its termination.
    /\ prod[t] = Cardinality(C)
    /\ \/ /\ Len(buffer) < B
        /\ buffer' = Append(buffer, d)
        /\ NotifyOther(t)
    \/ /\ Len(buffer) = B
        /\ Wait(t)
    /\ UNCHANGED <<prod,cons>>

Fortunately in this case, SANY caught it:

Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/BlockingQueuePoisonApple.tla
***Parse Error***

  Precedence conflict between ops \lor in block line 124, col 5 to line 124, col 6 of module BlockingQueuePoisonApple and \land.

Residual stack trace follows:
ExtendableExpr starting at line 124, column 8.
ExtendableExpr starting at line 118, column 5.
Expression starting at line 118, column 5.
Definition starting at line 117, column 1.
Module body starting at line 7, column 1.


Fatal errors while parsing TLA+ spec in file BlockingQueuePoisonApple

tla2sany.semantic.AbortException
*** Abort messages: 1

In module BlockingQueuePoisonApple

Could not parse module BlockingQueuePoisonApple from file BlockingQueuePoisonApple.tla


Starting... (2021-07-10 14:43:26)
Error: Parsing or semantic analysis failed.
Finished in 00s at (2021-07-10 14:43:26)

FWIW: The (Eclipse-based) Toolbox does the right thing when tabbing. :-)

[alygin]

I think this issue is not solvable on the extension level. In this case VSCode indents each line independently, and indentation on Tab pressing means "move to the next nearest position that corresponds to the configured tab size for the language (which is 4 by default fot TLA+)". This is why you end up with a broken TLA+ formatting.

Actually, it works the same way in any other language. In JavaScript this block:

const foo = 10;
   // ^^^ here's the name of the const

becomes

    const foo = 10;
        // ^^^ here's the name of the const

And the extenstion cannot change this behaviour (formatter API doesn't capture tab indentations). Though, for TLA+ it's a bigger problem than for most of other languages because text indentation is significant for the meaning of the spec.

Some other editors (IntelliJ IDEA, for instance) analyze the selected block as a whole before indenting it, and use the same indentation "distance" for all the lines.

Given all this, I think, this issue should go to the VSCode project, there's nothing we can do here.

BTW, we can help users with proper block formatting, here's the issue: #99. But it won't help with the described case.

[alygin]

I'm putting the issue on hold until there's an API to fix it on the extension level, or it's fixed on the VSCode level.

[lemmy]

@alygin Is there a way to prevent tabbing until tabbing works reliably? I fear that users accidentally change the semantics of their specs.

[alygin]

@lemmy, I'm not aware of an API that would help us here. There's the type command that can be used to analyze key strokes, but it doesn't provide the typing context and has other limitations that prevent it from being useful for such tasks.

[lemmy]

Erich Gamma: "the indentation behaviour is language specific and needs to be provided by a language extension. In this case it is the python extension. Therefore pls report the issue against the Python extension."

Related: https://github.com/microsoft/vscode/issues/10339 https://github.com/microsoft/vscode/issues/5394

[alygin]

@lemmy, unfortunately, none of these links help much. I think, by "the indentation behaviour" he meant that there's Indentation Rules that a language configuration can provide. But those rules do not affect how tabbing works. And Python still has the same problem with tabbing.

Other two links describe a different problem, they are about dichotomy between tab size and indentation size, which VSCdoe doesn't recognize out-of-the-box.

[johnyf]

It appears that when the VSCode editor configuration option "Use Tab Stops" is unticked, then a uniform amount of indentation is inserted across a set of selected lines, when pressing the tab key. This editor option is described in VSCode as:

inserting and deleting whitespace follows tab stops

[lemmy]

Given that editor.useTabStops is on by default, our extension should probably raise a warning.