Zulip Chat Archive

Stream: new members

Topic: cache-olean user confusion?

Oliver Nash (Dec 16 2019 at 21:49):

Does cache-olean --fetch perform something equivalent to git checkout . as part of its work?

Oliver Nash (Dec 16 2019 at 21:50):

The problem here could well be a simple case of PEBKAC but I think I just lost a bunch of work by running cache-olean --fetch at the wrong time.

Rob Lewis (Dec 16 2019 at 21:54):

I don't think so. You can see the source here: https://github.com/leanprover-community/mathlib-tools/blob/master/scripts/cache-olean.py

Rob Lewis (Dec 16 2019 at 21:55):

It does do a little more with Git than I realized, but nothing that looks dangerous at a quick glance.

Oliver Nash (Dec 16 2019 at 21:55):

OK thanks, I did scan over that source and saw nothing suspicious. I'll see if I can reproduce the behaviour that I think occurred.

Oliver Nash (Dec 16 2019 at 21:57):

pasted image

Oliver Nash (Dec 16 2019 at 21:58):

What the above is supposed to show is that cache-olean --fetch blew away the changes I had to the file lie_algebra.lean.

Oliver Nash (Dec 16 2019 at 21:59):

I'll scan over the script again to see if I can understand how this might be happening. (Still entirely possible, it's something weird I'm doing.)

Oliver Nash (Dec 16 2019 at 22:03):

I can't see it, and I'm in more of a mood to spend my few minutes trying to write some Lean than debugging some Python. I'll pick this up again at the weekend if it is still not resolved; I feel a bit bad for casting aspersions.

Rob Lewis (Dec 16 2019 at 22:06):

My only idea, are you using an old version of cache-olean that's maybe doing something different?

Oliver Nash (Dec 16 2019 at 22:08):

Hmm, I don't think that's it as I only started tinkering with Mathlib around about September, and indeed I see:

➜  mathlib git:(lean-3.4.2) ls -l /Users/olivernash/.mathlib/bin/cache-olean
-rwxr-xr-x  1 olivernash  staff  4961 17 Sep 22:22 /Users/olivernash/.mathlib/bin/cache-olean

and the history on GitHub says the file last changed in May.

Rob Lewis (Dec 16 2019 at 22:08):

I just tried and couldn't reproduce this.

Oliver Nash (Dec 16 2019 at 22:08):

Weird, but also thank you!

Rob Lewis (Dec 16 2019 at 22:10):

Huh. I'm out of ideas then. Let us know if you figure out what's going on, having work erased by a rogue script is a nightmare.

Oliver Nash (Dec 16 2019 at 22:10):

Given that you cannot reproduce, and others are not complaining about this, I think this is my issue to debug.

Oliver Nash (Dec 16 2019 at 22:10):

I will report back here if/when I figure it out, hopefully at the weekend. In the meantime, I will rename this thread as I think it could mislead people.

Oliver Nash (Dec 17 2019 at 20:56):

I managed to find a few minutes to look into this again this evening, and I believe I now understand. Here is where cache-olean --fetch clobbers my local changes:

    with DelayedInterrupt([signal.SIGTERM, signal.SIGINT]):
        ar = tarfile.open(os.path.join(mathlib_dir, asset.name))
        ar.extractall('.')  # Specifically this line!
        print("... successfully extracted olean archive.")

(https://github.com/leanprover-community/mathlib-tools/blob/f126b0df53a1769a02eb6c972e1d2c0574d4fb28/scripts/cache-olean.py#L73)

Oliver Nash (Dec 17 2019 at 20:57):

The reason is that the tar file which it is unpacking contains not just all the .olean files but also all the .lean source files. So that means that if you have any unstaged changes to .lean files then they'll be blown away by this step, as happened to me.

Oliver Nash (Dec 17 2019 at 21:01):

This is of course completely my fault but I wonder if it might be worth adding a warning to cache-olean to warn about this before proceeding? Maybe something along the lines of:

if repo.is_dirty():
   x = input('You have a dirty repo, and might lose data if you proceed. Do you wish to continue? [N]')

Simon Hudon (Dec 17 2019 at 21:01):

This approach helps keep the relative time stamp of .lean / .olean files consistent. We could check the git status before expand the archive.

Patrick Massot (Dec 17 2019 at 21:01):

I would say that running cache-olean with unstaged (and unstashed) changes is asking for trouble.

Simon Hudon (Dec 17 2019 at 21:01):

Yes, you can PR this

Oliver Nash (Dec 17 2019 at 21:01):

I'm all in favour of this approach, it makes total sense.

Oliver Nash (Dec 17 2019 at 21:01):

Well I certainly found trouble @Patrick Massot :)

Patrick Massot (Dec 17 2019 at 21:01):

But of course a warning would be nicer.

Oliver Nash (Dec 17 2019 at 21:02):

Thanks @Simon, I will PR that though ludicrously I have just used up my last scrap of free time for days so it will have to wait till the weekend!

Simon Hudon (Dec 17 2019 at 21:03):

If you want, you can add a command line option to disable that check (or to turn an error into a warning)

Oliver Nash (Dec 17 2019 at 21:03):

Thanks, I'll make sure to do that.

Simon Hudon (Dec 17 2019 at 21:05):

Thanks a lot! That's a great improvement

Oliver Nash (Dec 21 2019 at 15:48):

@Simon Hudon I just created this PR for mathlib-tools in an attempt to address this issue.

Simon Hudon (Dec 21 2019 at 19:43):

Thanks! I'll have a look

Last updated: Dec 20 2023 at 11:08 UTC