Improving reporting on failed builds.

[ejgallego]

In coq/coq#9278, @Zimmi48 has done some preliminary preparation to better understand failures of CI runs. IMHO that'd be very useful and I can see several tasks here, for example, the bot could link to the exact point of the log where the error happened.

[Zimmi48]

the bot could link to the exact point of the log where the error happened

That's a very good idea. Unfortunately, in GitLab CI, I'm not aware of a way to link to a specific line of the log (see e.g. https://gitlab.com/gitlab-org/gitlab-ce/issues/13205).

[Zimmi48]

Instead of linking to a specific line on GitLab, we now could extract the relevant error from the log and display it in the Checks tab. We just need to determine what we are looking for. The words "error" and "warning"?

[Zimmi48]

We are currently reporting the last 40 lines of failed builds. Please reopen if you have suggestions on how to improve this.