My branch with a `sorry` in it passed CI

Stream: mathlib4

[Mitchell Lee]

Hello, my branch https://github.com/leanprover-community/mathlib4/tree/trivial1711-nonarchimedean-sums-mul managed to pass CI even though there is a sorry in it. (The sorry is in https://github.com/leanprover-community/mathlib4/blob/trivial1711-nonarchimedean-sums-mul/Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean. Note that the commit that introduced the sorry failed CI.) Is this a mistake?

[Riccardo Brasca]

I am not sure, but a bunch of tests have been skipped, maybe that's the reason.

[Riccardo Brasca]

Can you open a PR and see what happens?

[Eric Wieser]

I think what's happening here is that:

• You submit the commit with a sorry. Mathlib builds, emits a warning, and we catch it in stdout.
• You change something downstream. Mathlib doesn't rebuild the file containing a sorry, and so we don't see it in the stdout any more.

[Damiano Testa]

A sorry logs a warning that is caught at the time of the build. If the file had a sorry, produced oleans in a previous run and does not need to be rebuilt on a later run, then it will not produce a warning and will not cause CI to fail.

[Damiano Testa]

Note however that at "merge-with-master" time, it would be caught, since that build would re-run all the files that were modified with respect to master.

[Damiano Testa]

There was a proposal to cache warnings, but I do not think that anyone has given much thought to implementing that.

[Mario Carneiro]

Eric Wieser said:

I think what's happening here is that:

• You submit the commit with a sorry. Mathlib builds, emits a warning, and we catch it in stdout.
• You change something downstream. Mathlib doesn't rebuild the file containing a sorry, and so we don't see it in the stdout any more.

@Mac Malone do the Lake output changes fix this issue?

[Eric Wieser]

Damiano Testa said:

Note however that at "merge-with-master" time, it would be caught, since that build would re-run all the files that were modified with respect to master.

This isn't true I don't think

[Mac Malone]

@Mario Carneiro Lake now caches logs and replays them. So, yes, it should.

[Eric Wieser]

If you:

• Get your PR approved
• Merge master right into the PR (which will likely trigger a sorry-based build failure)
• Commit some meaningless change to a leaf file
• Merge

then the build on master will use the cache from the penultimate step, and the sorry will be someone else's problem next time they have to rebuild your file (most likely Scott's with nightly-testing)

[Damiano Testa]

Eric Wieser said:

Damiano Testa said:

Note however that at "merge-with-master" time, it would be caught, since that build would re-run all the files that were modified with respect to master.

This isn't true I don't think

Ah, for some reason I thought that the bors build would start from the diff with master, not from the "diff-with-master-for-which-there-is-no-cache-yet"...

I agree with you -- and this is Kim's problem, sadly and most likely!

[Mario Carneiro]

@Mac Malone The original run in question was on 4.8.0-rc1, so I guess actually the lake changes didn't help

[Mario Carneiro]

I think maybe we just need to be using the new --werror in CI, there is a sorry warning in the succeeding run

[Mac Malone]

--wfail ;)

[Mac Malone]

Ah, and the reason that is needed is because the second run does not run Lean. Thus, it does not error out due to the Lean warningAsError option. Instead, it replays the cached log, and since Lake itself has not been told to be mad at warnings, it happily completes.

[Mario Carneiro]

Why doesn't the first run fail?

[Mario Carneiro]

with warningAsError shouldn't it appear as an error just like before?

[Eric Wieser]

Presumably we need warningAsError to influence the hash of the files compiled with it?

[Mario Carneiro]

It should not, and I think it already does not

[Mario Carneiro]

it's a weakLeanArgs so it does not change the hash

[Eric Wieser]

Otherwise I can inject an olean with a sorry into the cache by temporarily turning off the flag, and then when I turn it back on then the next cache download will let me get away with the sorry

[Mario Carneiro]

This is all fixed by the new lake setup

[Mario Carneiro]

although we need to also put the new log cache file in the cache

[Mario Carneiro]

(ideally we would have done all this before deploying it in production)

[Eric Wieser]

Mario Carneiro said:

(ideally we would have done all this before deploying it in production)

Is there an argument that we should do this before rc2?

[Mario Carneiro]

it's not dependent on the rc2 bump

[Mario Carneiro]

it can be done at any point after rc1

[Mario Carneiro]

or on the nightlies leading up to it

[Mario Carneiro]

fix is up at #12620, but I will leave it to others to test it