wrong olean on azure

Stream: general

[Sebastien Gouezel]

On #10188, the build failed twice (because of offline runners) but restarting the build finally succeeded. However, fetching the oleans with leanproject up doesn't get working oleans. As you can see in https://github.com/leanprover-community/mathlib/runs/4202480686?check_suite_focus=true, the push release to azure step skipped the file. Might that be related? Is that fixable?

[Gabriel Ebner]

curl -I https://oleanstorage.azureedge.net/mathlib/9520db71ee2c817adf059426c81a58d369bacd51.tar.xz seems to work.

[Gabriel Ebner]

Also leanproject works for me.

[Sebastien Gouezel]

leanproject works for me, but oleans are not up to date. I.e.,

 lean --make .\src\topology\metric_space\hausdorff_dimension.lean

starts recompiling nat/pow.lean.

[Gabriel Ebner]

It looks like the first run already uploaded the wrong oleans, but unfortunately the log file is cut off: https://github.com/leanprover-community/mathlib/runs/4193969798?check_suite_focus=true

[Gabriel Ebner]

Is that fixable?

We could remove the file from the cache, and then rerun the CI job.

[Gabriel Ebner]

But it's probably easier to just push a new commit to the branch.

[Sebastien Gouezel]

I meant: is that fixable by CI that a second run does not skip uploading to azure if the first run was not successful? On this particular commit, sure, pushing a new commit is the simplest thing to do.

[Gabriel Ebner]

We want to upload oleans even if the build fails (= is not successful). I'm not sure how we can detect the difference to this situation here.

[Gabriel Ebner]

We also don't want to update existing caches (because that's even weirder to debug).

[Gabriel Ebner]

We've had such a problem a long time ago as well, and we "fixed" it by running lean twice.

[Gabriel Ebner]

Maybe we just need to run lean three times in a row now?