Zulip Chat Archive

Stream: general

Topic: Bad oleans


view this post on Zulip Bhavik Mehta (Jun 24 2020 at 16:28):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 17:05):

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.

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 17:13):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 18:25):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 18:26):

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

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 18:34):

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

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 18:35):

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

view this post on Zulip Reid Barton (Jun 24 2020 at 18:36):

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.

view this post on Zulip Reid Barton (Jun 24 2020 at 18:37):

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

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 18:37):

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

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 18:38):

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

view this post on Zulip Patrick Massot (Jun 24 2020 at 18:44):

leanproject delete-zombies is your friend.

view this post on Zulip Bhavik Mehta (Jun 24 2020 at 18:45):

Great, thanks!

view this post on Zulip Reid Barton (Jun 24 2020 at 18:45):

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.

view this post on Zulip Reid Barton (Jun 24 2020 at 18:49):

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


Last updated: May 17 2021 at 22:15 UTC