why olean files in .gitignore?

Stream: general

[Kevin Buzzard]

I am fiddling around with two non-master branches in my local clone of mathlib, which is not the sort of thing I usually do. I make new .lean files in one branch, compile to get .olean files in the same branch and then switch to the other branch and the lean files disappear but the olean files don't. This is expected behaviour (I think), but I think it means that work done in one branch can affect the other branch, which doesn't sound right to me. If the olean files are OS-independent then why are they in .gitignore? It would save people from having to compile mathlib. I could completely understand why OS-dependent files wouldn't be there but not these. Is the issue to do with timestamps? Or because there's some unwritten rule that non-human-readable files should always for some reason be in .gitignore?

[Mario Carneiro]

one issue is that they will muddle up the git diffs

[Mario Carneiro]

people won't compile them half the time when making PRs so I don't know how trustworthy they would be

[Mario Carneiro]

it has more to do with the fact that it's a build artifact than a binary file, although the binary thing might cause diff problems, both that the diff is unreadable, and also that it's probably unnecessarily large because of things like renumbering causing big propagating changes from small changes

[Johan Commelin]

Right, the olean files won't match with the lean files most of the time, unless you have a git commit hook that requires you to build the project before commiting. Besides that, it creates huge and meaningless diffs, which isn't desirable.

[Johan Commelin]

The real solution is a central cache store indexed by git commits or something like that.