Unhelpful error message from prime mark

[dnjackson]

Nancy Day had posted a comment on the Discourse forum about whether "all x" was still supported. I now see why: see attached screenshot. It seems that when you use a prime (forgetting it's a special char in A6), you get this very strange message saying "The all x construct is no longer supported". We should get rid of this old message anyway; it's from when we stopped allowing "all expression" but nobody expects that anymore, and it would be great if we could add a suitable message about priming .

[leavens]

I also found this problem when trying out the examples in the tutorial, specifically in http://alloytools.org/tutorials/online/frame-FS-6.html, which uses fs' in several examples. Further examples in this tutorial also have similar problems. When I use the River Crossing example (from http://alloytools.org/tutorials/online/frame-RC-1.html) I see that there is also an unhandled exception:

Syntax error in C:\cygwin64\tmp\alloy_heredoc11186805347915747747.als at line 18 column 28: There are 3 possible tokens that can appear here: , : = at edu.mit.csail.sdg.parser.CompParser.syntax_error(CompParser.java:2813) at edu.mit.csail.sdg.parser.CompParser.parse(CompParser.java:2660) at edu.mit.csail.sdg.parser.CompParser.alloy_parseStream(CompParser.java:2855) at edu.mit.csail.sdg.parser.CompUtil.parse(CompUtil.java:497) at edu.mit.csail.sdg.parser.CompUtil.parseRecursively(CompUtil.java:259) at edu.mit.csail.sdg.parser.CompUtil.parseEverything_fromFile(CompUtil.java:404) at edu.mit.csail.sdg.parser.CompUtil.parseEverything_fromString(CompUtil.java:472) at edu.mit.csail.sdg.alloy4.OurSyntaxWidget.getModule(OurSyntaxWidget.java:502) at edu.mit.csail.sdg.alloy4.OurSyntaxWidget.getTooltip(OurSyntaxWidget.java:836) at edu.mit.csail.sdg.alloy4.OurAntiAlias$2.getToolTipText(OurAntiAlias.java:119) at java.desktop/javax.swing.ToolTipManager$insideTimerAction.actionPerformed(ToolTipManager.java:693) ...

[leavens]

I found that when running the jar file for Alloy, any time there is a syntax error, it looks like a stack backtrace is printed on the console (terminal) that ran the jar file. For example I see the following output:

Syntax error in C:\cygwin64\tmp\alloy_heredoc2831668139013362508.als at line 18 column 1: There are 5 possible tokens that can appear here: enum fun let open pred at edu.mit.csail.sdg.parser.CompParser.syntax_error(CompParser.java:2813) at edu.mit.csail.sdg.parser.CompParser.parse(CompParser.java:2660) at edu.mit.csail.sdg.parser.CompParser.alloy_parseStream(CompParser.java:2855) at edu.mit.csail.sdg.parser.CompUtil.parse(CompUtil.java:497) at edu.mit.csail.sdg.parser.CompUtil.parseRecursively(CompUtil.java:259) at edu.mit.csail.sdg.parser.CompUtil.parseEverything_fromFile(CompUtil.java:404) at edu.mit.csail.sdg.parser.CompUtil.parseEverything_fromString(CompUtil.java:472) at edu.mit.csail.sdg.alloy4.OurSyntaxWidget.getModule(OurSyntaxWidget.java:502) at edu.mit.csail.sdg.alloy4.OurSyntaxWidget.getTooltip(OurSyntaxWidget.java:836) at edu.mit.csail.sdg.alloy4.OurAntiAlias$2.getToolTipText(OurAntiAlias.java:119) at java.desktop/javax.swing.ToolTipManager$insideTimerAction.actionPerformed(ToolTipManager.java:693) at java.desktop/javax.swing.Timer.fireActionPerformed(Timer.java:311) at java.desktop/javax.swing.Timer$DoPostEvent.run(Timer.java:243) at java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:318) at java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:773) at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:720) at java.desktop/java.awt.EventQueue$4.run(EventQueue.java:714) at java.base/java.security.AccessController.doPrivileged(AccessController.java:399) at java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:86

And in the window for Alloy I also saw the error message:

There are 5 possible tokens that can appear here: enum fun let open pred

So that part is just failing to catch an exception (or stop it from printing a backtrace).

[nmacedo]

I've removed the legacy message, but I'm not sure how to provide a useful message for the particular case of primes: seeing a prime on a declaration triggers a syntax error at the parser level as would any other expression (e.g., all x+y:A | ...). If anyone has a suggestion on how to provide better error messages at that level let me know.

[grayswandyr]

What did you do exactly? Remove the grammar rule for this old all? If so, that's OK I think. As long as we don't print this misleading message «The "all x" construct is no longer supported. If you know the range of possible values of x, consider rewriting it as "x == set_of_all_possible_values".», we're good.

[nmacedo]

Yes, I removed that rule, now you'll just get a generic parser error for an invalid token.

[grayswandyr]

After discussion: good as it is.