Added argument for replacing line break between error messages.

[Alizter]

We add the -errorsuffix argument to coqc which lets users pass a string which will be used seperate error messages. When this option is not set it defaults to a linebreak. This is useful for users wanting to parse the output of coqc.

TODO:

• Perhaps come up with a better name for the argument?

Fixes / closes #14120

• Added / updated test-suite. (Not sure if I can really test this).
• Added changelog.
• Added / updated documentation.

[Alizter]

Here is an example:

ali:~/coq$ dune exec -- dev/shim/coqc-prelude -errorsuffix "FOO"  Test.v
File "./Test.v", line 3, characters 6-7:
Error:
In environment
n : nat
The term "n" has type "nat" while it is expected to have type "Type".FOO

[Zimmi48]

Not sure if I can really test this

You probably can by using an output test and the coq-prog-args mechanism (which we should really document in the test-suite README!). See an example at https://github.com/coq/coq/blob/master/test-suite/output/Arguments.v.

[Alizter]

@Zimmi48 IIRC the output tests in the test-suite have to succeed, which is contrary to what is happening here. Even the tests that are meant to fail really succeed but use a Fail vernac.

[Zimmi48]

Perhaps come up with a better name for the argument?

If this also applies to warnings, what about: -user-message-newline-substitute? (With the idea that long names are not a problem since this will never be called manually by a human user.)

[Zimmi48]

@Zimmi48 IIRC the output tests in the test-suite have to succeed, which is contrary to what is happening here. Even the tests that are meant to fail really succeed but use a Fail vernac.

I don't think so. See for instance:

• https://github.com/coq/coq/blob/master/test-suite/output/ErrorLocation_ltac_1.out
• https://github.com/coq/coq/blob/master/test-suite/output/ErrorLocation_ltac_1.v

[ejgallego]

I'm not a fan of this; I'd rather add a --machine option to coqc, which forces all output to be in a machine-readable format.

[Zimmi48]

Machine-readable isn't necessarily adapted to the use case here (where the goal is to parse CI output for error messages). cc @JasonGross who might be able to tell more.

[SkySkimmer]

ping @JasonGross

[JasonGross]

Yeah, machine readable is absolutely not what I'm looking for. I want machine-readable delimiters around the error message so I can replace all the newlines with something else (or, indeed, just have a flag that replaces the newlines for me), but I'm using this for GitHub annotations, which is to be read by humans

[ejgallego]

I don't see the problem with machine-readable output as rustc does; there is not problem at all displaying errors this way, as the machine-readable output still has the errors messages.

If you got like rustc a json output, you just pipe the output of coqc to your favorite json processor and then you can be way more flexible than doing such hacks in Coq [and can for example easily format errors to something that Github actions output parser understands, but by modifying the processor you can adapt to other platforms]

[ejgallego]

c.f. rust-lang/rust#30711

[JasonGross]

If the errors don't have machine-readable delimiters (i.e., either no newlines in error messages or else some special delimiter), then having things in JSON format will not help, because info messages, etc, can be interwoven with error messages, and I don't know any JSON parser that can extract JSON interwoven with make line noise. Furthermore, I'll still have to unescape the data from JSON, which I expect will be a bit of a pain. I don't object to also having a machine readable format option for the info around the string of the main error message (line number, etc), but it's already quite easy to parse all that information, there's no need to use JSON, and I'm not aware of any structured information within the main error message string that can be split off into a machine-readable format while still being trivial to use for display.

Do you have an example of an error message in machine-readable format where there's something interesting happening other than replacing line breaks with another string (my request) and escaping the error string (seems counterproductive)?

[ejgallego]

Obviously if coqc gets the --machine parameter, all output must be in the same format otherwise it is not usable.

There is quite a bit of structure on coqc's output , line numbers, error codes (that could link to the manual) , message level, completion status, etc....

Other tools have solved this by doing rpc, which is way more complex, but indeed in this case a simpler solution could work.

I don't see an issue in having to follow some Json escaping convention.

What you propose seems to me a half baked solution , it will work for this use case, but maybe next tool cannot deal with this, so we need to add yet another hack. It is claimed that the current format is "easy to parse" but it doesn't seem to be the case, moreover would we tweak coqc output a bit, for example to improve error messages with underlining, then what's gonna happen? Everything breaks again?

There is a reason data formats exists, and current coqc output is not one ATM

Instead, let's provide a well-defined format which then can be consumed by different users and adapted to their corresponding use case for once and for all.

[Alizter]

OK let's discuss in the call today.

[Zimmi48]

Unfortunately, I don't expect @JasonGross will be able to attend, especially on such short notice (given that he's now in the West Coast time band).

[Alizter]

Closing this for the time being

[JasonGross]

I'm still interested in seeing something like -user-message-newline-substitute. I can join a relevant coq-call if that's useful.