Zulip Chat Archive

Can somebody help me understand what went wrong in https://github.com/leanprover-community/mathlib4/actions/runs/6959383845/job/18936498084 ? I don't understand the logs (or rather what's expected and what's not), nor why any of my PR would have made the test suite fail.

Yaël Dillies (Nov 22 2023 at 18:50):

It seems the failing file is test.LibrarySearch.basic, but I can't reproduce locally. @Scott Morrison, since you authored most of the file, any idea?

Kyle Miller (Nov 22 2023 at 19:20):

(this is PR #7712)

Damiano Testa (Nov 22 2023 at 20:43):

I think that tests have been silenced recently: I wonder whether this has something to do with that.

Damiano Testa (Nov 22 2023 at 20:54):

Some tests are not quiet on your branch:

test/SimpRw.lean
test/SimpRw.lean:37:0: warning: declaration uses 'sorry'

test/apply_fun.lean
test/apply_fun.lean:271:2: warning: this tactic is never executed [linter.unreachableTactic]

test/convert2.lean
test/convert2.lean:10:2: warning: this tactic is never executed [linter.unreachableTactic]
test/convert2.lean:11:2: warning: this tactic is never executed [linter.unreachableTactic]

test/norm_cast.lean
test/norm_cast.lean:143:9: warning: unused variable `h` [linter.unusedVariables]

Ironically, I do not think that the culprit is LibrarySearch.

Yaël Dillies (Nov 22 2023 at 20:56):

Yes, but... why?

Damiano Testa (Nov 22 2023 at 20:59):

I don't know: the files on your branch look identical to the ones on master...

Damiano Testa (Nov 22 2023 at 21:00):

However, I am pretty sure that it is the script in GNUmakefile that is responsible for the failure.

Damiano Testa (Nov 22 2023 at 21:07):

In fact, the files appear to be noisy on master as well.

Damiano Testa (Nov 22 2023 at 21:13):

If you look at current master, the tests fail, but CI passes anyway.

Damiano Testa (Nov 22 2023 at 21:14):

Maybe the failure is enough to get the branch CI complain, but not the one of master? :shrug:

The PR was #8438.

Ruben Van de Velde (Nov 22 2023 at 21:21):

Oh I see it, I think

Ruben Van de Velde (Nov 22 2023 at 21:21):

    lake env lean test/$* > test/$*.log
    @if [ -s test/$*.log ]; then \
        echo "Error: Test output is not empty"; \
        cat test/$*.log; \
        rm -f test/$*.log \
        exit 1; \
    fi
    @rm -f test/$*.log

Damiano Testa (Nov 22 2023 at 21:21):

Is it the exit instead of return?

Ruben Van de Velde (Nov 22 2023 at 21:22):

It's trying to rm a file called exit because there's no semicolon

Ruben Van de Velde (Nov 22 2023 at 21:22):

@Scott Morrison

Ruben Van de Velde (Nov 22 2023 at 21:23):

But then why is it failing for @Yaël Dillies

Damiano Testa (Nov 22 2023 at 21:24):

Something is weird, but very good catch with the ;.

Ruben Van de Velde (Nov 22 2023 at 21:24):

Maybe the test is actually failing? Or crashing?

Ruben Van de Velde (Nov 22 2023 at 21:25):

And the output thing is just a red herring

Damiano Testa (Nov 22 2023 at 21:26):

On master and on Yaël PR the test files are identical, they also fail on master, but CI is happy with the errors...

Damiano Testa (Nov 22 2023 at 21:27):

On my computer, rm -f nonexistentfile does nothing with exit code 0.

Kyle Miller (Nov 22 2023 at 21:27):

Yeah, I was about to mention that.

Damiano Testa (Nov 22 2023 at 21:28):

But maybe, the computers where the branch CIs and the master CI run have different options?

Kyle Miller (Nov 22 2023 at 21:30):

Thanks for catching that semicolon @Ruben Van de Velde : #8580

Damiano Testa (Nov 22 2023 at 21:31):

As far as I can tell, rm has a non-zero exit code almost exclusively if it is trying to remove a file that cannot be deleted due to issues with permissions.

Damiano Testa (Nov 22 2023 at 21:31):

Maybe the "user" running the two CIs, on master and on CIs, have different permissions? I am really not sure.

Damiano Testa (Nov 22 2023 at 21:32):

Kyle Miller said:

Thanks for catching that semicolon Ruben Van de Velde : #8580

Still not passing the tests! How ironic...

Kyle Miller (Nov 22 2023 at 21:32):

rm seems to be unrelated to the noisy tests error. I'm seeing test/norm_cast.lean for example having an unused variable locally

Damiano Testa (Nov 22 2023 at 21:33):

Oh yes, there are 4 test files that are noisy.

Ruben Van de Velde (Nov 22 2023 at 21:33):

Damiano Testa said:

Kyle Miller said:

Thanks for catching that semicolon Ruben Van de Velde : #8580

Still not passing the tests! How ironic...

Tests that don't run in CI fail, that's pretty much a given :)

Ruben Van de Velde (Nov 22 2023 at 21:34):

test/convert2.lean:10:2: warning: this tactic is never executed [linter.unreachableTactic]
test/convert2.lean:11:2: warning: this tactic is never executed [linter.unreachableTactic]
test/apply_fun.lean:271:2: warning: this tactic is never executed [linter.unreachableTactic]
test/norm_cast.lean:143:9: warning: unused variable `h` [linter.unusedVariables]
test/SimpRw.lean:37:0: warning: declaration uses 'sorry'

Kyle Miller (Nov 22 2023 at 21:35):

I guess I'll just silence these tests and add the fixes to the PR

Damiano Testa (Nov 22 2023 at 21:35):

Those same files are noisy on master as well.

Damiano Testa (Nov 22 2023 at 21:39):

One day, there will be a formally verified CI...

Kyle Miller (Nov 22 2023 at 21:39):

I've noticed strange things with linter errors becoming noisy on my own branches before, especially the unused variable linter. Not in tests, but inside theory files.

Kyle Miller (Nov 22 2023 at 22:12):

Ok, #8580 managed to silence the tests, and Damiano put it on the maintainer merge queue.

Scott Morrison (Nov 23 2023 at 00:02):

My apologies about the missing semicolon. :-(

Patrick Massot (Nov 23 2023 at 00:19):

I guess you are contractually forced to do propaganda in favor of white-space sensitivity instead of end of line marks.

Damiano Testa (Nov 23 2023 at 00:38):

It is not clear that the semicolon was the issue though. The tests still failed with the semicolon added. They only stopped failing when Kyle silenced them.