[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Unicode TLA+



I think the ASCII/math-symbols dichotomy is a profound barrier to entry for TLA+. Examples we see in PDFs and books can't be pasted into our own specs, and for a beginner, it's not easy to translate them manually. Since most of us use TLA+ infrequently, we forget the equivalences and have to relearn them. If you see a symbol and don't know its ASCII, you can't always look it up: all the TLA+ ASCII tables I've found are incomplete. I've compiled my own list of symbols and trained myself with flash cards. No other tool I've used as a programmer has this kind of initial hurdle. Anything we do to make the two formats interoperable will be a big improvement. If it's done well and integrated into the Toolbox and/or VS Code it could widen the top of the adoption funnel dramatically. I bet that experienced TLA+ users would be surprised how big an impact this could make for widespread adoption.

So I have a strong opinion about the first question. Regarding the other two I have no opinion at all.

On Tuesday, September 14, 2021 at 3:46:35 PM UTC-4 andrew...@xxxxxxxxx wrote:
I think it could indeed be used to create a formatter. Say you wanted to write a rule where:

op == /\ A
      /\ B

should be formatted as:

op ==
  /\ A
  /\ B

this would be quite easy; you would write a query for all operator definitions with conjunction lists as a top-level _expression_, so:

(operator_definition (def_eq) @eq definition: (conj_list) @list)

where the @eq capture gets the == node, and the @list capture gets the conjunction list node. Then you check whether the two nodes are on the same line (easy, info readily available in node object) and if so you insert a newline then dedent all lines included within the conjunction list node. This should preserve vertical alignment for any nested conjunction/disjunction lists.

Andrew

On Tuesday, September 14, 2021 at 2:49:23 PM UTC-4 Alexander Niederbühl wrote:
I think this would be very useful, I find the ASCII representation a bit verbose and distracting. I know of several people who feel the same, e.g. https://matklad.github.io/2020/11/01/notes-on-paxos.html as another data point. Currently I'm using a VSCode extension together with FiraCode as workaround.

A bit unrelated but since in TLA+ there are many ways to write the same thing like \cup, \union or /= , # and different ways to format the code in terms of line breaks etc. I wish there would be a tool to get a canonically formatted Unicode representation which ideally TLC would be able to check. Do you think the treesitter grammar could be utilized to build a code formatter similar to prettier in _javascript_ or black in Python?
 

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f9eaf399-ef0f-4119-a5c9-b548eb8cad35n%40googlegroups.com.