A collection of specs which produce generic "could not parse module" errors

[ahelwer]

This code gives a generic "Could not parse module" error:

----------------------------- MODULE ParseError -----------------------------
VARIABLE x

Init ==
    /\ x = IF "foo" == "foo" THEN "bar" ELSE "foo"

=============================================================================

The error is the use of == instead of =, an easy mistake for a new user (or long-time user, in this case!) to make. Ideally the parser would identify the error in a user-friendly way.

[ahelwer]

I have found another generic parse error, with this code:

----------------------------- MODULE ParseError -----------------------------
VARIABLE x

Init ==
    /\ x = [n \in {1,2,3,4,5} : n]

=============================================================================

The : should of course be |->, but this is a real typo I made which resulted in a generic parse error. Recording this because these real-world experience issues aren't very valuable until someone wants to go through and fix all the generic parse errors, then they become super valuable.

[ahelwer]

Another. Here, I stubbed out a function with a constant value then forgot to remove the constant value after implementing it.

----------------------------- MODULE ParseError -----------------------------

F(x) == 0   \* Stub value I forgot to remove after writing function
    IF x == 0 THEN 1 ELSE 0

=============================================================================

[ahelwer]

This generic parse error occurs when forgetting a comma while defining a new record value:

----------------------------- MODULE ParseError -----------------------------

Def == [foo |-> "foo" bar |-> "bar"]

=============================================================================

[ahelwer]

Here there's a generic parse error when leaving a dangling comma after the list of variables (encountered when deleting/reordering variables):

----------------------------- MODULE ParseError -----------------------------

VARIABLES
    Foo,
    Bar,

=============================================================================

[ahelwer]

A generic parse error occurs if the terminating line of ==...== is somehow deleted (recalling this one from my TA experiences in a TLA+ course - it actually took me a while to debug!)

----------------------------- MODULE ParseError -----------------------------

VARIABLES
    Foo,
    Bar

[lemmy]

Missing parenthesis at "Cardinality(ProcSet" leads to generic parser error.

--------------- MODULE ParseError -------------

Inv == Cardinality(waitset) < Cardinality(ProcSet /\ waitset \subseteq ProcSet

===================================================

[ahelwer]

Using only one = in a LET causes a generic parser error

----------------------------- MODULE ParseError -----------------------------

Def ==
    LET x = 5 IN
    TRUE

=============================================================================

[ahelwer]

Using only one = in any definition causes a generic parser error

----------------------------- MODULE ParseError -----------------------------

Def = TRUE

=============================================================================

[ahelwer]

Forgetting to delete the multi-line comment closing symbols causes a generic parser error

----------------------------- MODULE ParseError -----------------------------

Def == TRUE *)

=============================================================================

[ahelwer]

Forgetting an ELSE in and IF-THEN-ELSE statement causes a generic parser error

----------------------------- MODULE ParseError -----------------------------

Def == IF "foo" = "foo" THEN "bar"

=============================================================================

[lestarcdog]

@ahelwer I have the same issue with the 1.5.6 version.
The previous version 1.5.4 displays correctly the specific parse error messages. So I think it is a regression issue.

[lemmy]

@lestarcdog Can you check if the current nightly still show the regression?

[lestarcdog]

@lemmy The regression issue is gone in the 1.5.7 version. The Parsing Errors panel shows the specific error message and also the error is highlighted in the editor.

Thanks.

[lemmy]

Fixed with commit 77f1c69