Zulip Chat Archive

Stream: new members

Topic: An .olean without the .lean??

Stuart Presnell (Dec 20 2021 at 13:00):

I have an odd situation in branch#SP_algebra_big_operators_prime (#10675): in my local files I have the file algebra/big_operators/associated.olean but not algebra/big_operators/associated.lean. This branch was created before @Anne Baanen posted #10848 which created big_operators/associated, if that makes any difference. I'm pretty sure I haven't deleted the .lean file, and I've updated a few times (with leanproject --debug up) since noticing the missing file, but it hasn't appeared.

Stuart Presnell (Dec 20 2021 at 13:02):

Oh, and if I switch to the master branch then both associated.olean and associated.lean are present.

Anne Baanen (Dec 20 2021 at 13:03):

The olean file probably stuck around from switching branches, that isn't something to worry about. To get access to the new associated.lean in your branch, you can run the commands git merge master; leanproject get-cache --rev=master (the latter ensures you have fresh olean files for the master branch)

Stuart Presnell (Dec 20 2021 at 13:06):

Aha, that's got it! Thank you!

Kevin Buzzard (Dec 20 2021 at 13:31):

Whenever I get nervy about oleans I just run find . -iname "*.olean" -execdir rm '{}' \; in an appropriate directory (it removes all oleans in all subdirectories of where you are) and then leanproject get-cache or leanproject get-m depending on whether I'm working on mathlib or on a project which depends on mathlib.

Alex J. Best (Dec 20 2021 at 14:58):

I think leanproject delete-zombies should delete these orphaned oleans for you

Last updated: Dec 20 2023 at 11:08 UTC