Add diagnostic for pluscal labels inserted by translation #350

hwayne · 2024-11-19T02:38:07Z

The PlusCal translator has a -reportLabels flag. When set, it will automatically add missing labels to translations and log that in the output:

pcal.trans Version 1.11 of 31 December 2020
The following label was added:
  Lbl_1 at line 16, column 5
Parsing completed.
Translation completed.

Since it's logged, we might as well tell the user about it! This PR adds an information diagnostic. Demo:

Questions:

Should it be a warning instead of information?
In the long run should the pluscal parser use some kind of state machine?

Signed-off-by: Hillel <h@hillelwayne.com>

src/parsers/pluscal.ts

lemmy · 2024-11-19T14:34:31Z

src/parsers/pluscal.ts

+            return false
+        }
+
+        const matcher = /^\s\s([A-Za-z0-9_]+) at line (\d+), column (\d+)$/g.exec(line)


Is this robust against any valid "label root" that a user may pass with -labelRoot?

It does not. I translating with -reportLabels -labelRoot "foo!ASD bar" and it successfully translated. No diagnostic appeared.

I'd argue this is a bug in the pluscal translator, though: it produces the operator

foo!ASD bar1 ==

Which isn't valid TLA+ in the first place. The regex does accept any valid TLA+ identifier (SS 227).

Can you please open a Pcal issue?

Took some time but that's now done!

tlaplus/tlaplus#1092

Signed-off-by: Hillel <h@hillelwayne.com>

create information diagnostic for labels added (with -reportLabels)

9882674

Signed-off-by: Hillel <h@hillelwayne.com>

hwayne force-pushed the add-label-reporting branch from f71c5f3 to 9882674 Compare November 19, 2024 02:39