Pluscal translation errors suppressed if there are existing TLA+ errors

[hwayne]

Spec:

---- MODULE PlusCal ----
EXTENDS TLC
(*--algorithm sample_computation
variables x = 0;
begin
    print(x);
    x = 1;
end algorithm;*)

\* BEGIN TRANSLATION
\* END TRANSLATION

Foo == x > 0

====

Running Parse Module gives the error "Unknown Operator: x" in Foo. Translating the PlusCal should fix this error, but translation fails silently. Commenting out the Foo operator provides the translation error, which is that x = 1; is not valid PlusCal. So the error with Foo (in the TLA+) is suppressing the error with x = 1; (in the PlusCal).

[FedericoPonzi]

On my Linux machine with the latest version of the extension when I copy paste your example code and run Parse: shows a parsing error on x = 1 which should be x :=1. If you fix it and leave Foo == x > 0, pluscal will be transpiled to TLA+ as expected. If you don't see the error, what version of the extension are you running?

[hwayne]

I'm running the latest version, but it's also on Windows. Maybe it's an OS difference?

[hwayne]

Ah, looks like it was fixed no later than v2024.10.192237. Closing!