Error in CI step "print sizes of oleans"

Stream: mathlib4

[David Loeffler]

Just saw this in the output of the current staging CI run, under "Print the sizes of the oleans":

Run du .lake/build/lib/Mathlib || echo "This code should be unreachable"
  du .lake/build/lib/Mathlib || echo "This code should be unreachable"
  shell: /usr/bin/bash -e {0}
  env:
    LAKE_NO_CACHE: true
du: cannot access '.lake/build/lib/Mathlib': No such file or directory
This code should be unreachable

This clearly shouldn't be happening, although it doesn't seem to be doing any actual harm. (Apologies if this has been reported before.)

[Damiano Testa]

I had never seen it and I did think that the code marked as unreachable was unreachable (or, more realistically, I hoped that it would be).

[Damiano Testa]

Those checks were there in any case precisely to make sure that s Print the oleans step would not prevent CI from passing.

[Damiano Testa]

The PR that you linked is a toolchain bump. I am not sure why the script should fail there. The failure seems to be because the dir .lake/build/lib/Mathlib does not exist, but if I checkout the branch and type the du ... command, it works.

[Eric Wieser]

It moved to .lake/build/lib/lean/Mathlib I think

[Damiano Testa]

Ah, so the path should be updated?

[Damiano Testa]

So, maybe, when I checked out the branch, the command picked up the path that existed on my computer, but was not the one to where lake would have saved the oleans?

[Damiano Testa]

Yes, indeed, lake build now stores the files inside a further lean dir.

[Damiano Testa]

#22506

[Damiano Testa]

I realised that there is also a step that removes the old cache files that is now removing the old path, but not the new one. I updated the PR above to fix that as well.