Bad oleans

Stream: general

[Bhavik Mehta]

I don't know if this counts as a bug or just something to be aware of, but if you delete a lean file without deleting its oleans, then it seems like other files which import it use the oleans which are now missing, so compilation using the exact same files can fail

[Kevin Buzzard]

I can't quite make sense of your post, but if you're not careful with git pull you can end up with oleans with no lean file and they can work just fine :-) except you can't jump to definition any more.

[Bhavik Mehta]

For clarity, I mean

leanproject new test-oleans
cd test-oleans/
echo 'import tactic' > src/blank.lean
echo 'import blank' > src/other.lean
leanproject build
rm src/blank.lean
leanpkg build

fails. I got caught out by this when I removed a file locally and didn't get any errors, but then CI failed

[Kevin Buzzard]

leanproject build works for me, as does leanpkg build. On Ubuntu.

[Kevin Buzzard]

Checked again -- the exact script you posted works for me.

[Bhavik Mehta]

Sorry I still wasn't clear - I don't think this should succeed, if I were to push that repo or share it in any way, it wouldn't compile, but you don't get any errors when trying locally

[Bhavik Mehta]

This might not be a bug but it definitely caught me out when I expected any errors CI would give should also be easily reproducible locally

[Reid Barton]

Yeah, I think this was originally intended as a feature (you can distribute .olean files without the corresponding .lean files), but in the context of mathlib it's just annoying.

[Reid Barton]

I would support a change where recompilation checking for an .olean file raises an error if the corresponding .lean file is missing.

[Bhavik Mehta]

Right - and this wasn't even in the context of mathlib

[Bhavik Mehta]

Reid Barton said:

I would support a change where recompilation checking for an .olean file raises an error if the corresponding .lean file is missing.

Perhaps a warning instead of an error if the feature you mention is desirable. Alternatively, something like leanproject clean which removes any oleans which don't have a lean file

[Patrick Massot]

leanproject delete-zombies is your friend.

[Bhavik Mehta]

Great, thanks!

[Reid Barton]

It would still be even better to fix the behavior in Lean though, because this can lead to some really confusing situations when you don't realize it is happening.

[Reid Barton]

I would assume that anyone using the community version of lean doesn't need the current behavior.