Our error messages do not follow the GNU standard

[andreasabel]

https://www.gnu.org/prep/standards/html_node/Errors.html

Our errors look like this:

Issue3491.agda:12,23-33 
Ill-formed projection pattern .unbox
when checking that the pattern box .unbox has type Box b

The position formatting is not covered by the GNU standard, because

• [ ] we use a comma rather than a dot or colon to separate line and column
• [x] we do not terminate the position with a colon

Valid would be e.g.

Issue3491.agda:12.23-33:
Issue3491.agda:12:23-33:

The error message can also give both the starting and ending positions of the erroneous text. There are several formats so that you can avoid redundant information such as a duplicate line number. Here are the possible formats:

sourcefile:line1.column1-line2.column2: message sourcefile:line1.column1-column2: message

Here is the implementation of the standard for Emacs: https://github.com/emacs-mirror/emacs/blob/master/lisp/progmodes/compile.el#L416-L484

[nad]

Note the commas in the following code:

https://github.com/agda/agda/blob/c436dd4cf5e42390cecec88cc7f7f6978ff8d1c4/src/data/emacs-mode/agda2-mode.el#L953-L956

[andreasabel]

So these would have to be replaced by (suitable quoted) dots along with changing the printing of ranges. @nad @UlfNorell: would you agree to switch to printing ranges in a GNU conformant way?

[nad]

Is this a standard that non-GNU tools follow? What format does GHC use?

[andreasabel]

Yes GHC follows the GNU standard:

src/full/Agda/Interaction/EmacsTop.hs:354:37: error: [GHC-83865]