Check the cache failure

Stream: mathlib4

[Ruben Van de Velde]

Junyan Xu said:

I've split off two PRs: #13153 (auxiliary results) and #13155 (first part of the main file)

However, there's currently a strange "check the cache" CI failure.

I also just ran into this: https://github.com/leanprover-community/mathlib4/actions/runs/9226614238/job/25386769739?pr=12457

Has anyone looked into it?

[Kim Morrison]

I guess the first question is whether it is exe cache or build --no-build that is failing with exit code 3.

[Ruben Van de Velde]

I think I intermittently reproduced it locally and it was from build

[Ruben Van de Velde]

@Yaël Dillies is also stuck on this here: https://github.com/leanprover-community/mathlib4/actions/runs/9258957725/job/25469973097?pr=13205

Can we turn it off?

[Ruben Van de Velde]

Or maybe we can pass --verbose to the command