An .olean without the .lean??

Stream: new members

[Stuart Presnell]

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]

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

[Anne Baanen]

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]

Aha, that's got it! Thank you!

[Kevin Buzzard]

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]

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