Does bedrock2 want warning/error annotations on PRs?

[JasonGross]

(This is from fiat-crypto.)
c.f. mit-plv/fiat-crypto#703

[samuelgruetter]

Fancy... 😂

At the moment, building bedrock2 outputs 147 warnings, does that mean each PR would get 147 such annotations?

[JasonGross]

does that mean each PR would get 147 such annotations?

Yes, it does :-D (Great motivation to fix the warnings, no?)

You could also modify it to only annotate errors and not warnings, though.

[samuelgruetter]

I see 😅

Annotated errors would be cool 😃

Would that require building the whole project on GitHub Actions? Before you can start building theend2end subproject, you have to build dependencies for about one hour, would that be a problem?

[JasonGross]

We're using this .json file:

{
    "problemMatcher": [
        {
            "owner": "coq-problem-matcher",
            "pattern": [
                {
                    "regexp": "^File \"([^ \"]+)\", line (\\d+), characters (\\d+-\\d+):",
                    "file": 1,
                    "line": 2,
                    "column": 3
                },
                {
                    "regexp": "^(Warning|Error): (.*?)(?:\\s*\\[(.*)\\])?$",
                    "severity": 1,
                    "message": 2,
                    "code": 3
                }
            ]
        }
    ]
}

You can make it match only errors by removing the Warning|. (You can actually just use "^(Error): (.*)$" for the second regexp (and get rid of "code") if you don't care about splitting off the error category.)

Then, yes, you need to build the whole project in GitHub Actions, and you want to

echo "::add-matcher::path/to/file.json"

before running make. There's no problem with building dependencies on GitHub Actions; I think there's no time limit for public repos.