RFC: Teach lake to use github error formats

[eric-wieser]

Proposal

Github has special support for setting error messages with

::error file={name},line={line},col={col},endLine={endLine},endColumn={endColumn},title={title}::{message}

where messages should be url-escaped (in particular, replacing newlines with %0A).

If lake learnt a --github flag, then github would automatically show multi line error messages on the lines that they originate from, such as

We had code for this in mathlib 3 via lean --json (added in leanprover-community/mathlib3#5726), but this is not exposed via lake (as far as I can tell), so writing such a wrapper is not possible.

Currently the workaround is to use a "problem matcher" for github actions (leanprover-community/mathlib4#24316), but these do not support the multi-line error messages produced by Lean, and so we see 'could not synthesize' but then the rest of the message is cut off.

It would be possible to have lake detect if it is running on github instead of having an explicit --github flag, but I expect this would just be confusing to users.

Maintainability

Lake already maintains a record of (severity, message) pairs, which can be converted to either ANSI or plain strings. Implementing this PR would involve:

• Adding a third state beyond ANSI and plain, "github".
• Either storing the full position message in the lake log message (via Options, as some messages can come from lake itself), or parsing it back out of the message strings

Community Feedback

#mathlib4 > gh-problem-matcher-wrap @ 💬

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

How do other compilers/ecosystems deal with this?