Open shonfeder opened 3 years ago
If you working on this right now, check #1127. It's related to error messages. I am going to use to produce message about unsupported operators.
Related to #802
As points of reference for the state of the art, the most lauded error messaging I'm aware of are in:
This should be a valuable resource in helping guide our design: https://web.eecs.umich.edu/~akamil/papers/iticse19.pdf
Related: #1654
See https://github.com/informalsystems/apalache/pull/1717/files#r868375855
Where I suggest:
- [Bug874.tla:4:17-4:27]: Cannot apply ["a" ↦ 2] to the argument "b" in (["a" ↦ 2])["b"].
+ [Bug874.tla:4:17-4:27]: Cannot access nonexistent field "b" in record ["a" ↦ 2] in (["a" ↦ 2])["b"].
This should go with a more systematic treatment of composing phrasing for errors on particular kinds of values.
During our retro last week, we discussed some ways we could change the error messaging and user-error handling that would improve learnability and user feedback, and perhaps even improve our development cycle. The two key points discussed were: