actionlint

Stream: mathlib4

[Kim Morrison]

After discovering a stupid mistake in a CI script I wrote, I tried adding actionlint to our CI in #11471.

It successfully noticed my stupid mistake, which is good.

However it also has many other suggestions, and until we act on these it will fail CI. If anyone would be interested in looking into these, I think it would be a good investment in our CI to clean these all up.

[Yaël Dillies]

Are we going to lint the lint? :scream:

[Damiano Testa]

Is it ok to simply push to the branch for "accepting the style change"?

[Damiano Testa]

I just did... :speak_no_evil:

[Damiano Testa]

The only remaining error is

property "test" is not defined in object type {archive: {conclusion: string; outcome: string; outputs: {string => string}}; build: {conclusion: string; outcome: string; outputs: {string => string}}; counterexamples: {conclusion: string; outcome: string; outputs: {string => string}}; hash_commands: {conclusion: string; outcome: string; outputs: {string => string}}; lean4checker: {conclusion: string; outcome: string; outputs: {string => string}}; lint: {conclusion: string; outcome: string; outputs: {string => string}}; noisy: {conclusion: string; outcome: string; outputs: {string => string}}; shake: {conclusion: string; outcome: string; outputs: {string => string}}}

in three files.
I failed in diagnosing what the issue is.

[Kim Morrison]

@Damiano Testa, your fix for the noisy stdout linter seems to have broken it.

[Kim Morrison]

@Damiano Testa, I fixed that one (it's a missing id: test in the test step). But it seems someone force pushed over my changes?

[Kim Morrison]

e.g. it's still there in my commit 828aaf8. Could you recover my changes from the history?

[Damiano Testa]

Oh, sorry, I'll look into these issues!

[Damiano Testa]

Ok, the id: test fixed the linting.

[Damiano Testa]

As for the noisy test, I wanted to make it print the output of both stderr and stdout. I simply checked the opposite of what I meant. I should have fixed this, but I am testing it right now.

[Damiano Testa]

I think that I fixed the test for noisiness. Now it should report both outputs, not just the one of the first successful grep.

[Damiano Testa]

(CI on the PR is now only missing lint and lean4checker.)

[Damiano Testa]

... and CI is happy!

[Damiano Testa]

(I also had a branch with a noisy master and noisy failed on it, as it should)

[Kim Morrison]

Okay, lets see if there is another maintainer around who can review this for us. :-)

[Kim Morrison]

I feel like this was a combination of some tedious-and-probably-unnecessary changes, but also catching some real bugs, so overall I think it is quite valuable to have actionlint turned on. CI is hard to get right.

[Damiano Testa]

Maybe we should run shellcheck also on the linting files written in bash.

[Damiano Testa]

(I think that it was useful and it will be useful in the future, if/when CI changes)

[Damiano Testa]

In fact, shouldn't there be tests for CI?