Zulip Chat Archive

Stream: general

Topic: wrong olean on azure


Sebastien Gouezel (Nov 15 2021 at 21:34):

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 (Nov 15 2021 at 21:42):

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

Gabriel Ebner (Nov 15 2021 at 21:44):

Also leanproject works for me.

Sebastien Gouezel (Nov 15 2021 at 21:46):

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 (Nov 15 2021 at 21:51):

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 (Nov 15 2021 at 21:54):

Is that fixable?

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

Gabriel Ebner (Nov 15 2021 at 21:55):

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

Sebastien Gouezel (Nov 15 2021 at 22:02):

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 (Nov 15 2021 at 22:09):

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 (Nov 15 2021 at 22:09):

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

Gabriel Ebner (Nov 15 2021 at 22:10):

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

Gabriel Ebner (Nov 15 2021 at 22:10):

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


Last updated: Dec 20 2023 at 11:08 UTC