gh-problem-matcher-wrap

Stream: mathlib4

[Kim Morrison]

Do we have anything written down about the test block in Mathlib CI:

      - name: test mathlib
        id: test
        uses: liskin/gh-problem-matcher-wrap@v3
        with:
          linters: gcc
          run: |
            bash -o pipefail -c "
            make -k -j 8 test"

This implicitly puts a constraint on how make test is meant to work, i.e. it should produce errors formatted in way that the gcc linter in gh-problem-matcher-wrap can understand.

Does it currently do this?

If so, can someone who understands it document it lightly? Which code is responsible for producing the correctly formatting errors? There needs to be a reference at that point to this problem matcher, so we know what not to break!

If not, can we remove this?

[Eric Wieser]

Lean itself used to produce gcc-style errors, but no longer does

[Kim Morrison]

Okay, let's proceed with removing the wrapper then.

[Eric Wieser]

Either we:

• write a custom problem matcher and get single-line diagnostics again (this is fairly easy, it's a config file with some regex)
• implement Lean 3's --json and restore the Python wrapper script
• Have Lean directly output GitHub annotations in the format the old Python script did

[Eric Wieser]

There have been two or three other threads lamenting how error messages no longer appear on GitHub in 4.8.0, though pretending Lean was gcc was obviously a hack

[Kim Morrison]

I mean, these are all great things to try. But removing the non-functioning wrapper is the first step. :-)

[Eric Wieser]

My first bullet would leave the wrapper in place

[Eric Wieser]

And replace the word gcc

[Kim Morrison]

It's non-functioning code, that prevents people modifying the setup (I'm switching out to lake test).

[Kim Morrison]

If someone wants to write the custom problem matcher, that's great. But it can't block other work, and leave the CI files in a broken and undocumented state.

[Kim Morrison]

I'll create the issue for you. :-)

[Eric Wieser]

Does lake test break the wrapper? I thought the wrapper just prints a magic line before and after its contents, and GitHub did the rest?

[Kim Morrison]

Nothing could break the wrapper. It is already broken.

[Eric Wieser]

Being a no-op is not the same as crashing!

[Kim Morrison]

My point is that it is dead code, sitting in the CI file, that has now wasted 20 minutes of my time worrying about whether I need to preserve its behaviour.

[Kim Morrison]

Being a confusing undocumented noop is not the same as crashing, but is still worse than not existing. And much worse than not existing and there being an issue about future work.

[Eric Wieser]

Here's one such other thread:

Michael Rothgang said:

There used to be a workflow that would annote build errors or warnings in the "files changed" tab on github: this was extremely helpful. My WIP PR #12879 did not have these. (It builds now, so is not suitable for testing. I can restore an old non-building state if this would help.)
Was this on purpose?

[Kim Morrison]

I'll make sure to link to that in the issue. :-)

[Eric Wieser]

I don't really agree with "the Lean 4.8.0 release broke some downstream code, let's delete it instead of fixing that code"

[Eric Wieser]

Though maybe an issue is a sufficient replacement

[Kim Morrison]

#12946 is the issue, #12945 the PR

[Eric Wieser]

Are you sure it's a no-op for shake and the linter?

[Kim Morrison]

Indeed, I've restored the problem matcher for shake, on the assumption that its gh-style flag is compatible with the gcc matcher.

[Kim Morrison]

Do we know if it used to work for the linter?

[Eric Wieser]

I think it did

[Eric Wieser]

It's possible that gh-style makes the matcher moot

[Eric Wieser]

Probably best to introduce a lint error and a shake error in the PR, and see if either are reported?

[Kim Morrison]

The doc-string in Shake says:

  /-- `--gh-style`: output messages that can be parsed by `gh-problem-matcher-wrap` -/

[Kim Morrison]

I can't see anything in runLinter that pays attention to the output format re: github

[Eric Wieser]

I'm surprised we don't directly output the GitHub annotation format

[Eric Wieser]

(as described at https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-a-warning-message)

[Kim Morrison]

I just pushed a linter failure to the PR, we'll see where it ends up displayed.

[Mario Carneiro]

Wait a minute, I definitely disagree with deleting this code. 4.8.0-rc1 broke vscode links and also gh-problem-matcher-wrap links, and the correct fix is to make the error reports match the previous format or otherwise be one of the supported formats, not to delete the very useful code that was relying on this behavior that is now broken

[Mario Carneiro]

I mentioned this issue on the same day 4.8.0-rc1 came out, but Mac's argument was that file:line:col-line:col is more information than the previous (and widely recognized) file:line:col format. I checked some other languages and most of them don't give the end position; rust gives this information in pictorial format by highlighting the whole span together with the code but the numerical line:col is just the starting position. I think it's not really needed since if you click on the link it takes you to the full highlight anyway. The broken links are a much bigger negative for me.

[Mario Carneiro]

Re: "we shouldn't pretend lean is gcc", I read it a bit differently. We are saying that lean produces gcc-style line/col links, which is one among several predefined options (namely file:line:col, by comparison to <file>, line <line>, column <col> aka "python style", and there are some others). There is no need for us to be inventing our own format for line/col links, this requires implementing this support in various places and seems kind of similar to trying to implement a custom unicode extension or custom syntax highlighting in terms of needing to get a bunch of unrelated entities to play along with our random choices.

[Kim Morrison]

Okay --- very happy to close my PR, but will someone else please make a PR that adds comments at the invocations of the matcher which are not working, stating this? This does not need to wait on a solution.