git hooks

Stream: general

[Yury G. Kudryashov]

How to loose a file with the (possibly, outdated) git hooks suggested by the installation instructions:

1. While on branch A, create a new file, don't add it to git.
2. Make a commit.
3. Switch to branch B.
4. (optional) work on branch B.
5. Add some text to the new file.
6. Do not make a commit.
7. Switch to branch A.

On step 2 the file is added to the cache, on step 7 it is overridden with an older version from cache. I've just lost Jensen's inequality for integrals this way.

@Patrick Massot What do you think about ignoring files which are not in git in leanproject mk-cache?

[Johan Commelin]

Do the caches touch lean files?

[Johan Commelin]

They should only do things with olean files, right?

[Johan Commelin]

I'm sorry to hear that you lost some exciting code.

[Alex J. Best]

I lost a _lot_ of stuff to (probably) exactly this a month ago, but didn't know what it was :confused: thanks for diagnosing it, Yury.

[Yury G. Kudryashov]

Yes, caches touch lean files, probably to ensure that the unpacked .oleans match .leans.

[Patrick Massot]

I'm sorry to read that. I never used those commit hooks. In principle there is no obstruction to archive only files that git knows about. The archiving function is https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/lib.py#L101-L115

[Patrick Massot]

You can open an issue in the mathlibtools repo and I'll try to find time to work on it (or you can open a PR!).

[Yury G. Kudryashov]

I'll try to make a PR.

[Scott Morrison]

I have used the hooks up until now, but have recently decided that they actually make life slower rather than faster (because my computer finds local caches and unpacks them, after which I discover they are not what I wanted, and then have to go looking for a cache with leanproject -f up).